no goals
α : Type u_1
β : Type ?u.1823472
γ : Type ?u.1823475
δ : Type ?u.1823478
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f
⊢ (∫⁻ (a : α), f a ∂Measure.trim μ hm) = ∫⁻ (a : α), f a ∂μ
rw [lintegral_congr_ae (ae_eq_of_ae_eq_trim hf.ae_eq_mk), lintegral_congr_ae hf.ae_eq_mk,
  lintegral_trim hm hf.measurable_mk]