-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_pos_iff_support_of_nonneg_ae' (hf : 0 ≤ᵐ[μ.restrict (Ι a b)] f)
    (hfi : IntervalIntegrable f μ a b) :
    (0 < ∫ x in a..b, f x ∂μ) ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b)

Proof state:
case inr
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ 0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b)

Tactic:
suffices (∫ x in a..b, f x ∂μ) ≤ 0 by simp only [this.not_lt, hba.not_lt, false_and]

Result:
case inr
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ ≤ 0

Proof state:
case inr
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc b a))] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ 0 ≤ ∫ (x : ℝ) in Ioc b a, f x ∂μ

Tactic:
exact integral_nonneg_of_ae hf

Result:
no goals

Proof state:
case inl
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hab : a < b
⊢ 0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b)

Tactic:
rw [uIoc_of_le hab.le] at hf

Result:
case inl
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] f
hfi : IntervalIntegrable f μ a b
hab : a < b
⊢ 0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b)

Proof state:
case inl
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] f
hfi : IntervalIntegrable f μ a b
hab : a < b
⊢ 0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b)

Tactic:
simp only [hab, true_and, integral_of_le hab.le,
  setIntegral_pos_iff_support_of_nonneg_ae hf hfi.1]

Result:
no goals

Proof state:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
this : ∫ (x : ℝ) in a..b, f x ∂μ ≤ 0
⊢ 0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b)

Tactic:
simp only [this.not_lt, hba.not_lt, false_and]

Result:
no goals

Proof state:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
⊢ 0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b)

Tactic:
rcases lt_or_le a b with hab | hba

Result:
case inl
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hab : a < b
⊢ 0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b)

case inr
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ 0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b)

Proof state:
case inr
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f x ∂μ ≤ 0

Tactic:
rw [integral_of_ge hba, neg_nonpos]

Result:
case inr
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ 0 ≤ ∫ (x : ℝ) in Ioc b a, f x ∂μ

Proof state:
case inr
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ 0 ≤ ∫ (x : ℝ) in Ioc b a, f x ∂μ

Tactic:
rw [uIoc_comm, uIoc_of_le hba] at hf

Result:
case inr
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc b a))] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ 0 ≤ ∫ (x : ℝ) in Ioc b a, f x ∂μ