-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_simpleFunc_larger_space (hm : m ≤ m0) (f : @SimpleFunc β m F)
    (hf_int : Integrable f μ) :
    ∫ x, f x ∂μ = ∑ x ∈ @SimpleFunc.range β F m f, ENNReal.toReal (μ (f ⁻¹' {x})) • x

Proof state:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable (⇑f) μ
⊢ Integrable (⇑(SimpleFunc.toLargerSpace hm f)) μ

Tactic:
rwa [SimpleFunc.coe_toLargerSpace_eq]

Result:
no goals

Proof state:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int✝ : Integrable (⇑f) μ
hf_int : Integrable (⇑(SimpleFunc.toLargerSpace hm f)) μ
⊢ ∑ x ∈ (SimpleFunc.toLargerSpace hm f).range, (μ (⇑(SimpleFunc.toLargerSpace hm f) ⁻¹' {x})).toReal • x =
    ∑ x ∈ f.range, (μ (⇑(SimpleFunc.toLargerSpace hm f) ⁻¹' {x})).toReal • x

Tactic:
congr 1

Result:
no goals

Proof state:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int✝ : Integrable (⇑f) μ
hf_int : Integrable (⇑(SimpleFunc.toLargerSpace hm f)) μ
⊢ ∫ (x : β), (SimpleFunc.toLargerSpace hm f) x ∂μ =
    ∑ x ∈ f.range, (μ (⇑(SimpleFunc.toLargerSpace hm f) ⁻¹' {x})).toReal • x

Tactic:
rw [SimpleFunc.integral_eq_sum _ hf_int]

Result:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int✝ : Integrable (⇑f) μ
hf_int : Integrable (⇑(SimpleFunc.toLargerSpace hm f)) μ
⊢ ∑ x ∈ (SimpleFunc.toLargerSpace hm f).range, (μ (⇑(SimpleFunc.toLargerSpace hm f) ⁻¹' {x})).toReal • x =
    ∑ x ∈ f.range, (μ (⇑(SimpleFunc.toLargerSpace hm f) ⁻¹' {x})).toReal • x

Proof state:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable (⇑f) μ
⊢ ∫ (x : β), f x ∂μ = ∑ x ∈ f.range, (μ (⇑f ⁻¹' {x})).toReal • x

Tactic:
simp_rw [← f.coe_toLargerSpace_eq hm]

Result:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable (⇑f) μ
⊢ ∫ (x : β), (SimpleFunc.toLargerSpace hm f) x ∂μ =
    ∑ x ∈ f.range, (μ (⇑(SimpleFunc.toLargerSpace hm f) ⁻¹' {x})).toReal • x

Proof state:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable (⇑f) μ
⊢ ∫ (x : β), (SimpleFunc.toLargerSpace hm f) x ∂μ =
    ∑ x ∈ f.range, (μ (⇑(SimpleFunc.toLargerSpace hm f) ⁻¹' {x})).toReal • x

Tactic:
have hf_int : Integrable (f.toLargerSpace hm) μ := by rwa [SimpleFunc.coe_toLargerSpace_eq]

Result:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int✝ : Integrable (⇑f) μ
hf_int : Integrable (⇑(SimpleFunc.toLargerSpace hm f)) μ
⊢ ∫ (x : β), (SimpleFunc.toLargerSpace hm f) x ∂μ =
    ∑ x ∈ f.range, (μ (⇑(SimpleFunc.toLargerSpace hm f) ⁻¹' {x})).toReal • x