no goals
α : Type u_1
E : Type ?u.1114206
F : Type ?u.1114209
𝕜 : Type ?u.1114212
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.1116903
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfi : Integrable f
⊢ (0 < ∫ (x : α), f x ∂μ) ↔ 0 < ↑↑μ (Function.support f)
simp_rw [(integral_nonneg_of_ae hf).lt_iff_ne, pos_iff_ne_zero, Ne.def, @eq_comm ℝ 0,
  integral_eq_zero_iff_of_nonneg_ae hf hfi, Filter.EventuallyEq, ae_iff, Pi.zero_apply,
  Function.support]