α : Type u_1
E : Type ?u.1063910
F : Type ?u.1063913
𝕜 : Type ?u.1063916
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.1066607
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
⊢ 0 ≤ if hf : Integrable fun a => f a then ↑L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
α : Type u_1
E : Type ?u.1063910
F : Type ?u.1063913
𝕜 : Type ?u.1063916
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.1066607
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
⊢ 0 ≤ ∫ (a : α), f a ∂μ
simp only [integral, L1.integral]
no goals
α : Type u_1
E : Type ?u.1063910
F : Type ?u.1063913
𝕜 : Type ?u.1063916
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.1066607
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
⊢ 0 ≤ if hf : Integrable fun a => f a then ↑L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
exact setToFun_nonneg (dominatedFinMeasAdditive_weightedSMul μ)
  (fun s _ _ => weightedSMul_nonneg s) hf