mathlib

b22a7c7e - refactor(measure_theory/integral/bochner): remove superfluous hypothesis (#10181)

refactor(measure_theory/integral/bochner): remove superfluous hypothesis (#10181) * Remove hypothesis from `tendsto_integral_of_dominated_convergence` that was superfluous * This results in simplifying some proofs, and removing some hypotheses from other lemmas * Also remove some `ae_measurable` hypotheses for functions that were also assumed to be `integrable`.