α : Type u_1
E : Type u_2
F : Type ?u.1246877
𝕜 : Type ?u.1246880
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
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1249571
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α →ₛ E
hfi : Integrable ↑f
⊢ integral μ f = integral μ (Lp.simpleFunc.toSimpleFunc (Lp.simpleFunc.toLp f (_ : Memℒp (↑f) 1)))
α : Type u_1
E : Type u_2
F : Type ?u.1246877
𝕜 : Type ?u.1246880
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
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1249571
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α →ₛ E
hfi : Integrable ↑f
⊢ integral μ f = ∫ (x : α), ↑f x ∂μ
rw [MeasureTheory.integral_eq f hfi, ← L1.SimpleFunc.toLp_one_eq_toL1,
  L1.SimpleFunc.integral_L1_eq_integral, L1.SimpleFunc.integral_eq_integral]
no goals
α : Type u_1
E : Type u_2
F : Type ?u.1246877
𝕜 : Type ?u.1246880
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
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1249571
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α →ₛ E
hfi : Integrable ↑f
⊢ integral μ f = integral μ (Lp.simpleFunc.toSimpleFunc (Lp.simpleFunc.toLp f (_ : Memℒp (↑f) 1)))
exact SimpleFunc.integral_congr hfi (Lp.simpleFunc.toSimpleFunc_toLp _ _).symm