case inl
ι : Type ?u.19452276
𝕜 : Type ?u.19452279
E : Type ?u.19452282
F : Type ?u.19452285
A : Type ?u.19452288
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hfi : IntervalIntegrable f μ a b
hab : a ≤ b
hf : 0 ≤ᵐ[Measure.restrict μ (Ioc a b)] f
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = 0 ↔ f =ᵐ[Measure.restrict μ (Ioc a b)] 0

case inr
ι : Type ?u.19452276
𝕜 : Type ?u.19452279
E : Type ?u.19452282
F : Type ?u.19452285
A : Type ?u.19452288
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hfi : IntervalIntegrable f μ a b
hab : b ≤ a
hf : 0 ≤ᵐ[Measure.restrict μ (Ioc b a)] f
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = 0 ↔ f =ᵐ[Measure.restrict μ (Ioc b a)] 0
ι : Type ?u.19452276
𝕜 : Type ?u.19452279
E : Type ?u.19452282
F : Type ?u.19452285
A : Type ?u.19452288
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : 0 ≤ᵐ[Measure.restrict μ (Ioc a b ∪ Ioc b a)] f
hfi : IntervalIntegrable f μ a b
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = 0 ↔ f =ᵐ[Measure.restrict μ (Ioc a b ∪ Ioc b a)] 0
cases' le_total a b with hab hab <;>
  simp only [Ioc_eq_empty hab.not_lt, empty_union, union_empty] at hf ⊢
no goals
case inl
ι : Type ?u.19452276
𝕜 : Type ?u.19452279
E : Type ?u.19452282
F : Type ?u.19452285
A : Type ?u.19452288
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hfi : IntervalIntegrable f μ a b
hab : a ≤ b
hf : 0 ≤ᵐ[Measure.restrict μ (Ioc a b)] f
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = 0 ↔ f =ᵐ[Measure.restrict μ (Ioc a b)] 0
exact integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi
no goals
case inr
ι : Type ?u.19452276
𝕜 : Type ?u.19452279
E : Type ?u.19452282
F : Type ?u.19452285
A : Type ?u.19452288
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f g : ℝ → ℝ
a b : ℝ
μ : MeasureTheory.Measure ℝ
hfi : IntervalIntegrable f μ a b
hab : b ≤ a
hf : 0 ≤ᵐ[Measure.restrict μ (Ioc b a)] f
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = 0 ↔ f =ᵐ[Measure.restrict μ (Ioc b a)] 0
rw [integral_symm, neg_eq_zero, integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi.symm]