-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_lt_integral_of_continuousOn_of_le_of_exists_lt {f g : ℝ → ℝ} {a b : ℝ}
    (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hgc : ContinuousOn g (Icc a b))
    (hle : ∀ x ∈ Ioc a b, f x ≤ g x) (hlt : ∃ c ∈ Icc a b, f c < g c) :
    (∫ x in a..b, f x) < ∫ x in a..b, g x

Proof state:
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : (volume.restrict (Ioc a b)) {x | f x < g x} = 0
⊢ f =ᶠ[ae (volume.restrict (Ioc a b))] g

Tactic:
simp only [← not_le, ← ae_iff] at hlt

Result:
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc a b), g a ≤ f a
⊢ f =ᶠ[ae (volume.restrict (Ioc a b))] g

Proof state:
case hlt
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : (volume.restrict (Ioc a b)) {x | f x < g x} = 0
h_eq : f =ᶠ[ae (volume.restrict (Icc a b))] g
⊢ ∀ c ∈ Icc a b, g c ≤ f c

Tactic:
exact fun c hc ↦ (Measure.eqOn_Icc_of_ae_eq volume hab.ne h_eq hfc hgc hc).ge

Result:
no goals

Proof state:
case hle
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : ∃ c ∈ Icc a b, f c < g c
⊢ f ≤ᶠ[ae (volume.restrict (Ioc a b))] g

Tactic:
simpa only [measurableSet_Ioc, ae_restrict_eq]
  using (ae_restrict_mem measurableSet_Ioc).mono hle

Result:
no goals

Proof state:
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : ∃ c ∈ Icc a b, f c < g c
⊢ ∫ (x : ℝ) in a..b, f x < ∫ (x : ℝ) in a..b, g x

Tactic:
apply integral_lt_integral_of_ae_le_of_measure_setOf_lt_ne_zero hab.le
  (hfc.intervalIntegrable_of_Icc hab.le) (hgc.intervalIntegrable_of_Icc hab.le)

Result:
case hle
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : ∃ c ∈ Icc a b, f c < g c
⊢ f ≤ᶠ[ae (volume.restrict (Ioc a b))] g

case hlt
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : ∃ c ∈ Icc a b, f c < g c
⊢ (volume.restrict (Ioc a b)) {x | f x < g x} ≠ 0

Proof state:
case hlt
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : (volume.restrict (Ioc a b)) {x | f x < g x} = 0
⊢ ∀ c ∈ Icc a b, g c ≤ f c

Tactic:
have h_eq : f =ᵐ[volume.restrict (Ioc a b)] g := by
  simp only [← not_le, ← ae_iff] at hlt
  exact EventuallyLE.antisymm ((ae_restrict_iff' measurableSet_Ioc).2 <|
    Eventually.of_forall hle) hlt

Result:
case hlt
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : (volume.restrict (Ioc a b)) {x | f x < g x} = 0
h_eq : f =ᶠ[ae (volume.restrict (Ioc a b))] g
⊢ ∀ c ∈ Icc a b, g c ≤ f c

Proof state:
case hlt
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : ∃ c ∈ Icc a b, f c < g c
⊢ (volume.restrict (Ioc a b)) {x | f x < g x} ≠ 0

Tactic:
contrapose! hlt

Result:
case hlt
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : (volume.restrict (Ioc a b)) {x | f x < g x} = 0
⊢ ∀ c ∈ Icc a b, g c ≤ f c

Proof state:
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc a b), g a ≤ f a
⊢ f =ᶠ[ae (volume.restrict (Ioc a b))] g

Tactic:
exact EventuallyLE.antisymm ((ae_restrict_iff' measurableSet_Ioc).2 <|
  Eventually.of_forall hle) hlt

Result:
no goals

Proof state:
case hlt
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : (volume.restrict (Ioc a b)) {x | f x < g x} = 0
h_eq : f =ᶠ[ae (volume.restrict (Ioc a b))] g
⊢ ∀ c ∈ Icc a b, g c ≤ f c

Tactic:
rw [Measure.restrict_congr_set Ioc_ae_eq_Icc] at h_eq

Result:
case hlt
f g : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hgc : ContinuousOn g (Icc a b)
hle : ∀ x ∈ Ioc a b, f x ≤ g x
hlt : (volume.restrict (Ioc a b)) {x | f x < g x} = 0
h_eq : f =ᶠ[ae (volume.restrict (Icc a b))] g
⊢ ∀ c ∈ Icc a b, g c ≤ f c