α : Type ?u.1721748
E : Type ?u.1721751
F : Type u_2
𝕜 : Type ?u.1721757
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SMulCommClass ℝ 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
H : Type ?u.1724428
β : Type u_1
γ : Type ?u.1724434
inst✝ : NormedAddCommGroup H
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → F
hf : AEStronglyMeasurable f (Measure.trim μ hm)
⊢ (∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ) = ∫ (a : β), AEStronglyMeasurable.mk f hf a ∂Measure.trim μ hm
α : Type ?u.1721748
E : Type ?u.1721751
F : Type u_2
𝕜 : Type ?u.1721757
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SMulCommClass ℝ 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
H : Type ?u.1724428
β : Type u_1
γ : Type ?u.1724434
inst✝ : NormedAddCommGroup H
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → F
hf : AEStronglyMeasurable f (Measure.trim μ hm)
⊢ (∫ (x : β), f x ∂μ) = ∫ (x : β), f x ∂Measure.trim μ hm
rw [integral_congr_ae (ae_eq_of_ae_eq_trim hf.ae_eq_mk), integral_congr_ae hf.ae_eq_mk]
no goals
α : Type ?u.1721748
E : Type ?u.1721751
F : Type u_2
𝕜 : Type ?u.1721757
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SMulCommClass ℝ 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
H : Type ?u.1724428
β : Type u_1
γ : Type ?u.1724434
inst✝ : NormedAddCommGroup H
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → F
hf : AEStronglyMeasurable f (Measure.trim μ hm)
⊢ (∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ) = ∫ (a : β), AEStronglyMeasurable.mk f hf a ∂Measure.trim μ hm
exact integral_trim hm hf.stronglyMeasurable_mk