α : Type u_2
E : Type u_1
F : Type ?u.949136
𝕜 : Type ?u.949139
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 α
f : α → E
hf : Integrable f
⊢ (if hf_1 : Integrable fun a => ↑↑(Integrable.toL1 f hf) a then
      ↑integralCLM (Integrable.toL1 (fun a => ↑↑(Integrable.toL1 f hf) a) hf_1)
    else 0) =
    if hf : Integrable fun a => f a then ↑integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
α : Type u_2
E : Type u_1
F : Type ?u.949136
𝕜 : Type ?u.949139
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 α
f : α → E
hf : Integrable f
⊢ (∫ (a : α), ↑↑(Integrable.toL1 f hf) a ∂μ) = ∫ (a : α), f a ∂μ
simp only [MeasureTheory.integral, L1.integral]
no goals
α : Type u_2
E : Type u_1
F : Type ?u.949136
𝕜 : Type ?u.949139
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 α
f : α → E
hf : Integrable f
⊢ (if hf_1 : Integrable fun a => ↑↑(Integrable.toL1 f hf) a then
      ↑integralCLM (Integrable.toL1 (fun a => ↑↑(Integrable.toL1 f hf) a) hf_1)
    else 0) =
    if hf : Integrable fun a => f a then ↑integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
exact setToFun_toL1 (dominatedFinMeasAdditive_weightedSMul μ) hf