Do we really need all of lebesgue-integral, fubinis-theorem, tonellis-theorem (all of them introduced here?) I think the first one is well covered by measure-theory while I could understand a tag like fubini-tonelli but I don't think it is really useful.