Theorem: Measure_theory.Lp_trim_to_Lp.ae_eq (Untitled/Probability/Indep.lean)

State before:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
f : ↥(Lp ℝ p)
⊢ ↑↑(Lp_trim_to_Lp p μ hm f) =ᵐ[μ] ↑↑f
Tactic:
apply lpTrimToLpMeas_ae_eq
State after:
no goals