α : Type ?u.1706708
E : Type ?u.1706711
F : Type u_2
𝕜 : Type ?u.1706717
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.1709388
β : Type u_1
γ : Type ?u.1709394
inst✝ : NormedAddCommGroup H
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable ↑f
hf : StronglyMeasurable ↑f
⊢ (∫ (x : β), ↑f x ∂μ) = ∫ (x : β), ↑f x ∂Measure.trim μ hm
α : Type ?u.1706708
E : Type ?u.1706711
F : Type u_2
𝕜 : Type ?u.1706717
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.1709388
β : Type u_1
γ : Type ?u.1709394
inst✝ : NormedAddCommGroup H
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable ↑f
⊢ (∫ (x : β), ↑f x ∂μ) = ∫ (x : β), ↑f x ∂Measure.trim μ hm
have hf : StronglyMeasurable[m] f := @SimpleFunc.stronglyMeasurable β F m _ f
α : Type ?u.1706708
E : Type ?u.1706711
F : Type u_2
𝕜 : Type ?u.1706717
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.1709388
β : Type u_1
γ : Type ?u.1709394
inst✝ : NormedAddCommGroup H
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable ↑f
hf : StronglyMeasurable ↑f
hf_int_m : Integrable ↑f
⊢ (∫ (x : β), ↑f x ∂μ) = ∫ (x : β), ↑f x ∂Measure.trim μ hm
α : Type ?u.1706708
E : Type ?u.1706711
F : Type u_2
𝕜 : Type ?u.1706717
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.1709388
β : Type u_1
γ : Type ?u.1709394
inst✝ : NormedAddCommGroup H
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable ↑f
hf : StronglyMeasurable ↑f
⊢ (∫ (x : β), ↑f x ∂μ) = ∫ (x : β), ↑f x ∂Measure.trim μ hm
have hf_int_m := hf_int.trim hm hf
α : Type ?u.1706708
E : Type ?u.1706711
F : Type u_2
𝕜 : Type ?u.1706717
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.1709388
β : Type u_1
γ : Type ?u.1709394
inst✝ : NormedAddCommGroup H
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable ↑f
hf : StronglyMeasurable ↑f
hf_int_m : Integrable ↑f
⊢ ∑ x in SimpleFunc.range f, ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x =
    ∑ x in SimpleFunc.range f, ENNReal.toReal (↑↑(Measure.trim μ hm) (↑f ⁻¹' {x})) • x
α : Type ?u.1706708
E : Type ?u.1706711
F : Type u_2
𝕜 : Type ?u.1706717
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.1709388
β : Type u_1
γ : Type ?u.1709394
inst✝ : NormedAddCommGroup H
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable ↑f
hf : StronglyMeasurable ↑f
hf_int_m : Integrable ↑f
⊢ (∫ (x : β), ↑f x ∂μ) = ∫ (x : β), ↑f x ∂Measure.trim μ hm
rw [integral_simpleFunc_larger_space (le_refl m) f hf_int_m,
  integral_simpleFunc_larger_space hm f hf_int]
case e_f.h
α : Type ?u.1706708
E : Type ?u.1706711
F : Type u_2
𝕜 : Type ?u.1706717
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.1709388
β : Type u_1
γ : Type ?u.1709394
inst✝ : NormedAddCommGroup H
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable ↑f
hf : StronglyMeasurable ↑f
hf_int_m : Integrable ↑f
x : F
⊢ ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x = ENNReal.toReal (↑↑(Measure.trim μ hm) (↑f ⁻¹' {x})) • x
α : Type ?u.1706708
E : Type ?u.1706711
F : Type u_2
𝕜 : Type ?u.1706717
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.1709388
β : Type u_1
γ : Type ?u.1709394
inst✝ : NormedAddCommGroup H
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable ↑f
hf : StronglyMeasurable ↑f
hf_int_m : Integrable ↑f
⊢ ∑ x in SimpleFunc.range f, ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x =
    ∑ x in SimpleFunc.range f, ENNReal.toReal (↑↑(Measure.trim μ hm) (↑f ⁻¹' {x})) • x
congr with x
case e_f.h.e_a.e_a
α : Type ?u.1706708
E : Type ?u.1706711
F : Type u_2
𝕜 : Type ?u.1706717
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.1709388
β : Type u_1
γ : Type ?u.1709394
inst✝ : NormedAddCommGroup H
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable ↑f
hf : StronglyMeasurable ↑f
hf_int_m : Integrable ↑f
x : F
⊢ ↑↑μ (↑f ⁻¹' {x}) = ↑↑(Measure.trim μ hm) (↑f ⁻¹' {x})
case e_f.h
α : Type ?u.1706708
E : Type ?u.1706711
F : Type u_2
𝕜 : Type ?u.1706717
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.1709388
β : Type u_1
γ : Type ?u.1709394
inst✝ : NormedAddCommGroup H
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable ↑f
hf : StronglyMeasurable ↑f
hf_int_m : Integrable ↑f
x : F
⊢ ENNReal.toReal (↑↑μ (↑f ⁻¹' {x})) • x = ENNReal.toReal (↑↑(Measure.trim μ hm) (↑f ⁻¹' {x})) • x
congr 2
no goals
case e_f.h.e_a.e_a
α : Type ?u.1706708
E : Type ?u.1706711
F : Type u_2
𝕜 : Type ?u.1706717
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.1709388
β : Type u_1
γ : Type ?u.1709394
inst✝ : NormedAddCommGroup H
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable ↑f
hf : StronglyMeasurable ↑f
hf_int_m : Integrable ↑f
x : F
⊢ ↑↑μ (↑f ⁻¹' {x}) = ↑↑(Measure.trim μ hm) (↑f ⁻¹' {x})
exact (trim_measurableSet_eq hm (@SimpleFunc.measurableSet_fiber β F m f x)).symm