-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem intervalIntegral_pos_of_pos_on {f : ℝ → ℝ} {a b : ℝ} (hfi : IntervalIntegrable f volume a b)
    (hpos : ∀ x : ℝ, x ∈ Ioo a b → 0 < f x) (hab : a < b) : 0 < ∫ x : ℝ in a..b, f x

Proof state:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
h₀ : 0 ≤ᶠ[ae (volume.restrict (Ι a b))] f
⊢ 0 < ∫ (x : ℝ) in a..b, f x

Tactic:
rw [integral_pos_iff_support_of_nonneg_ae' h₀ hfi]

Result:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
h₀ : 0 ≤ᶠ[ae (volume.restrict (Ι a b))] f
⊢ a < b ∧ 0 < volume (support f ∩ Ioc a b)

Proof state:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
⊢ 0 < ∫ (x : ℝ) in a..b, f x

Tactic:
have h₀ : 0 ≤ᵐ[volume.restrict (uIoc a b)] f := by
  rw [EventuallyLE, uIoc_of_le hab.le]
  refine ae_restrict_of_ae_eq_of_ae_restrict Ioo_ae_eq_Ioc ?_
  rw [ae_restrict_iff' measurableSet_Ioo]
  filter_upwards with x hx using (hpos x hx).le

Result:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
h₀ : 0 ≤ᶠ[ae (volume.restrict (Ι a b))] f
⊢ 0 < ∫ (x : ℝ) in a..b, f x

Proof state:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (Ioo a b), 0 x ≤ f x

Tactic:
rw [ae_restrict_iff' measurableSet_Ioo]

Result:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
⊢ ∀ᵐ (x : ℝ), x ∈ Ioo a b → 0 x ≤ f x

Proof state:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
h₀ : 0 ≤ᶠ[ae (volume.restrict (Ι a b))] f
⊢ a < b ∧ 0 < volume (support f ∩ Ioc a b)

Tactic:
exact ⟨hab, ((Measure.measure_Ioo_pos _).mpr hab).trans_le (measure_mono hsupp)⟩

Result:
no goals

Proof state:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
⊢ 0 < ∫ (x : ℝ) in a..b, f x

Tactic:
have hsupp : Ioo a b ⊆ support f ∩ Ioc a b := fun x hx =>
  ⟨mem_support.mpr (hpos x hx).ne', Ioo_subset_Ioc_self hx⟩

Result:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
⊢ 0 < ∫ (x : ℝ) in a..b, f x

Proof state:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
⊢ 0 ≤ᶠ[ae (volume.restrict (Ι a b))] f

Tactic:
rw [EventuallyLE, uIoc_of_le hab.le]

Result:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (Ioc a b), 0 x ≤ f x

Proof state:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (Ioc a b), 0 x ≤ f x

Tactic:
refine ae_restrict_of_ae_eq_of_ae_restrict Ioo_ae_eq_Ioc ?_

Result:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (Ioo a b), 0 x ≤ f x

Proof state:
f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
⊢ ∀ᵐ (x : ℝ), x ∈ Ioo a b → 0 x ≤ f x

Tactic:
filter_upwards with x hx using (hpos x hx).le

Result:
no goals