awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
n : ℕ
y : ℝ
⊢ ‖G (↑n : ℝ)⁻¹ y‖ = G (↑n : ℝ)⁻¹ y

Tactic:
abs_eq_self.mpr (hg.monotoneOn univ |>.slope_nonneg trivial trivial)

Premises used: Iff.mpr, MonotoneOn.slope_nonneg, trivial, Set.univ, Monotone.monotoneOn, abs_eq_self
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
n : ℕ
y : ℝ
⊢ ‖G (↑n : ℝ)⁻¹ y‖ = G (↑n : ℝ)⁻¹ y

Tactic:
exact abs_eq_self.mpr (hg.monotoneOn univ |>.slope_nonneg trivial trivial)

Premises used: Iff.mpr, MonotoneOn.slope_nonneg, trivial, Set.univ, Monotone.monotoneOn, abs_eq_self
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
⊢ liminf
      (fun (n : ℕ) ↦
        ENNReal.ofReal
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
            G (↑n : ℝ)⁻¹ x))
      atTop ≤
    ENNReal.ofReal (g b - g a)

Tactic:
Filter.liminf_le_of_frequently_le'
          (Filter.Frequently.of_forall fun n ↦ ENNReal.ofReal_le_ofReal ?_)

Premises used: Filter.Frequently.of_forall, Filter.liminf_le_of_frequently_le', ENNReal.ofReal_le_ofReal
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
refine :
  ∀ (n : ℕ),
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
        G (↑n : ℝ)⁻¹ x) ≤
      g b - g a
⊢ liminf
      (fun (n : ℕ) ↦
        ENNReal.ofReal
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
            G (↑n : ℝ)⁻¹ x))
      atTop ≤
    ENNReal.ofReal (g b - g a)

Tactic:
refine Filter.liminf_le_of_frequently_le'
          (Filter.Frequently.of_forall fun n ↦ ENNReal.ofReal_le_ofReal ?_)

Premises used: Filter.Frequently.of_forall, Filter.liminf_le_of_frequently_le', ENNReal.ofReal_le_ofReal
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
n : ℕ
rw : ∫ (x : ℝ) in a..b, G (↑n : ℝ)⁻¹ x ≤ g b - g a
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) ≤
    g b - g a

Tactic:
rw [integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le hab]

Premises used: intervalIntegral.integral_of_le, MeasureTheory.integral_Icc_eq_integral_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
n : ℕ
⊢ LE.le (α := ℝ) 0 (↑n : ℝ)⁻¹

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
n : ℕ
h : g b = g (b + (↑n : ℝ)⁻¹)
⊢ ∫ (x : ℝ) in a..b, G (↑n : ℝ)⁻¹ x ≤ g b - g a

Tactic:
convert!
          hg.monotoneOn (Icc a (b + (n : ℝ)⁻¹)) |>.intervalIntegral_slope_le hab (by simp) using 2

Premises used: MonotoneOn.intervalIntegral_slope_le, Nat.cast, Inv.inv, Set.Icc, HAdd.hAdd, Monotone.monotoneOn
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
n : ℕ
⊢ g b = g (b + (↑n : ℝ)⁻¹)

Tactic:
simp [g]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
⊢ ENNReal.ofReal (g b - g a) = ENNReal.ofReal (f b - f a)

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
G : (c x : ℝ) → ℝ := fun (c x : ℝ) ↦ slope g x (x + c)
G_integrable :
  ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
_ :
  Eq (α := ENNReal)
    (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, enorm (E := ℝ) ((fun (n : ℕ) (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) n x)) atTop)
    (liminf
      (fun (n : ℕ) ↦
        ENNReal.ofReal
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
            G (↑n : ℝ)⁻¹ x))
      atTop)
_₁ :
  liminf
      (fun (n : ℕ) ↦
        ENNReal.ofReal
          (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
            G (↑n : ℝ)⁻¹ x))
      atTop ≤
    ENNReal.ofReal (g b - g a)
_₂ : ENNReal.ofReal (g b - g a) = ENNReal.ofReal (f b - f a)
⊢ liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, enorm (E := ℝ) ((fun (n : ℕ) (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) n x)) atTop ≤
    ENNReal.ofReal (f b - f a)

Tactic:
calc
      _ = liminf (fun (n : ℕ) ↦ ENNReal.ofReal (∫ (x : ℝ) in Icc a b, (G (n : ℝ)⁻¹) x)) atTop := by
        apply Filter.liminf_congr
        filter_upwards with n
        rw [← MeasureTheory.ofReal_integral_norm_eq_lintegral_enorm (G_integrable n)]
        congr with y
        exact abs_eq_self.mpr (hg.monotoneOn univ |>.slope_nonneg trivial trivial)
      _ ≤ ENNReal.ofReal (g b - g a) := by
        refine Filter.liminf_le_of_frequently_le'
          (Filter.Frequently.of_forall fun n ↦ ENNReal.ofReal_le_ofReal ?_)
        rw [integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le hab]
        convert!
          hg.monotoneOn (Icc a (b + (n : ℝ)⁻¹)) |>.intervalIntegral_slope_le hab (by simp) using 2
        simp [g]
      _ = ENNReal.ofReal (f b - f a) := by grind

Premises used: Filter.liminf, ENNReal.ofReal, HSub.hSub, MeasureTheory.Measure.restrict, Nat.cast, Filter.atTop, Inv.inv, Set.Icc, MeasureTheory.MeasureSpace.volume, MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
inr :
  ∀ (h : ∀ {a b : ℝ} (hf : MonotoneOn f (uIcc a b)) (hab : a ≤ b), IntervalIntegrable (deriv f) volume a b)
    (hab : ¬a ≤ b), IntervalIntegrable (deriv f) volume a b
wlog : ∀ {a b : ℝ} (hf : MonotoneOn f (uIcc a b)) (hab : a ≤ b), IntervalIntegrable (deriv f) volume a b
⊢ IntervalIntegrable (deriv f) volume a b

Tactic:
wlog hab : a ≤ b generalizing a b with h
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
h : ∀ {a b : ℝ} (hf : MonotoneOn f (uIcc a b)) (hab : a ≤ b), IntervalIntegrable (deriv f) volume a b
hab : ¬a ≤ b
linarith : a < b → b - a + (a - b) = 0
⊢ b ≤ a

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
h : ∀ {a b : ℝ} (hf : MonotoneOn f (uIcc a b)) (hab : a ≤ b), IntervalIntegrable (deriv f) volume a b
hab : ¬a ≤ b
⊢ IntervalIntegrable (deriv f) volume a b

Tactic:
exact h (uIcc_comm a b ▸ hf) (by linarith) |>.symm

Premises used: IntervalIntegrable.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
hab : a ≤ b
⊢ MonotoneOn f (Icc a b)

Tactic:
rw [uIcc_of_le hab] at hf

Premises used: Set.uIcc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
hab : a ≤ b
hf₁ : MonotoneOn f (Icc a b)
⊢ a ≤ b

Tactic:
rw [uIcc_of_le hab] at hf

Premises used: Set.uIcc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
obtain :
  ∀ (G : ℕ → ℝ → ℝ)
    (hGf : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x)))
    (hG :
      ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b)))
    (hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)),
    IntervalIntegrable (deriv f) volume a b
⊢ IntervalIntegrable (deriv f) volume a b

Tactic:
obtain ⟨G, hGf, hG, hG'⟩ := hf.exists_tendsto_deriv_liminf_lintegral_enorm_le hab

Premises used: MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
⊢ Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤

Tactic:
have hG'₀ : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤ :=
    lt_of_le_of_lt hG' ENNReal.ofReal_lt_top |>.ne_top
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
⊢ @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))

Tactic:
have integrable_f_deriv := integrable_of_tendsto hGf hG hG'₀
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
⊢ IntervalIntegrable (deriv f) volume a b

Tactic:
(intervalIntegrable_iff_integrableOn_Icc_of_le hab).mpr integrable_f_deriv

Premises used: Iff.mpr, intervalIntegrable_iff_integrableOn_Icc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
⊢ IntervalIntegrable (deriv f) volume a b

Tactic:
exact (intervalIntegrable_iff_integrableOn_Icc_of_le hab).mpr integrable_f_deriv

Premises used: Iff.mpr, intervalIntegrable_iff_integrableOn_Icc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
inr :
  ∀ (h : ∀ {a b : ℝ} (hf : MonotoneOn f (uIcc a b)) (hab : a ≤ b), ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a))
    (hab : ¬a ≤ b), ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
wlog : ∀ {a b : ℝ} (hf : MonotoneOn f (uIcc a b)) (hab : a ≤ b), ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)

Tactic:
wlog hab : a ≤ b generalizing a b with h
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
h : ∀ {a b : ℝ} (hf : MonotoneOn f (uIcc a b)) (hab : a ≤ b), ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
hab : ¬a ≤ b
linarith : a < b → b - a + (a - b) = 0
⊢ b ≤ a

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
h : ∀ {a b : ℝ} (hf : MonotoneOn f (uIcc a b)) (hab : a ≤ b), ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
hab : ¬a ≤ b
⊢ ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)

Tactic:
specialize h (uIcc_comm a b ▸ hf) (by linarith)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
hab : ¬a ≤ b
h : ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)
⊢ b ∈ uIcc a b

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
hab : ¬a ≤ b
h : ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)
⊢ a ∈ uIcc a b

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
hab : ¬a ≤ b
h : ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)
linarith : a < b → b - a + (a - b) = 0
⊢ b ≤ a

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
hab : ¬a ≤ b
h : ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)
⊢ f b ≤ f a

Tactic:
have : f b ≤ f a := hf (by simp) (by simp) (by linarith)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
hab : ¬a ≤ b
h : ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)
this : f b ≤ f a
linarith : 0 < f b - f a → f b - f a + (0 - (f b - f a)) = 0
⊢ f b - f a ≤ 0

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
hab : ¬a ≤ b
h : ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)
this : f b ≤ f a
inr : -∫ (x : ℝ) in b..a, deriv f x ∈ Icc (f b - f a) 0
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)

Tactic:
rw [intervalIntegral.integral_symm, uIcc_of_ge (by linarith)]

Premises used: Set.uIcc_of_ge, intervalIntegral.integral_symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
hab : ¬a ≤ b
h : ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)
this : f b ≤ f a
⊢ -∫ (x : ℝ) in b..a, deriv f x ∈ Icc (f b - f a) 0

Tactic:
neg_mem_Icc_iff.mpr ?_

Premises used: Iff.mpr, Set.Mem, Set.neg_mem_Icc_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
hab : ¬a ≤ b
h : ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)
this : f b ≤ f a
inr : ∫ (x : ℝ) in b..a, deriv f x ∈ Icc (-0) (-(f b - f a))
⊢ -∫ (x : ℝ) in b..a, deriv f x ∈ Icc (f b - f a) 0

Tactic:
refine neg_mem_Icc_iff.mpr ?_

Premises used: Iff.mpr, Set.neg_mem_Icc_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
hab : ¬a ≤ b
h : ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)
this : f b ≤ f a
inr : ∫ (x : ℝ) in b..a, deriv f x ∈ Icc 0 (f a - f b)
⊢ ∫ (x : ℝ) in b..a, deriv f x ∈ Icc (-0) (-(f b - f a))

Tactic:
simp only [neg_zero, neg_sub]

Premises used: neg_sub, neg_zero
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
hab : ¬a ≤ b
h : ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)
this : f b ≤ f a
linarith : f a - f b < 0 → f b - f a + (f a - f b - 0) = 0
⊢ 0 ≤ f a - f b

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
hab : ¬a ≤ b
h : ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)
this : f b ≤ f a
inr inr₁ inr₂ inr₃ :
  ∀ (h : ∫ (x : ℝ) in b..a, deriv f x ∈ Icc 0 (f a - f b)) (this : f b ≤ f a),
    ∫ (x : ℝ) in b..a, deriv f x ∈ Icc 0 (f a - f b)
⊢ ∫ (x : ℝ) in b..a, deriv f x ∈ Icc 0 (f a - f b)

Tactic:
rwa [uIcc_of_le (by linarith)] at h

Premises used: Set.uIcc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
obtain :
  ∀ (G : ℕ → ℝ → ℝ)
    (hGf : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x)))
    (hG :
      ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b)))
    (hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)),
    ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)

Tactic:
obtain ⟨G, hGf, hG, hG'⟩ := hf.exists_tendsto_deriv_liminf_lintegral_enorm_le hab

Premises used: MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
⊢ ∀ᵐ (x : ℝ), x ≠ a

Tactic:
simp [ae_iff, measure_singleton]

Premises used: MeasureTheory.NoAtoms.measure_singleton, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
⊢ ∀ᵐ (x : ℝ), x ≠ a

Tactic:
have h₁ : ∀ᵐ x, x ≠ a := by simp [ae_iff, measure_singleton]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
⊢ ∀ᵐ (x : ℝ), x ≠ b

Tactic:
simp [ae_iff, measure_singleton]

Premises used: MeasureTheory.NoAtoms.measure_singleton, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
⊢ ∀ᵐ (x : ℝ), x ≠ b

Tactic:
have h₂ : ∀ᵐ x, x ≠ b := by simp [ae_iff, measure_singleton]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
⊢ Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤

Tactic:
have hG'₀ : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤ :=
    lt_of_le_of_lt hG' ENNReal.ofReal_lt_top |>.ne_top
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
h₁ : ∀ᵐ (x : ℝ), x ≠ a
h₂ : ∀ᵐ (x : ℝ), x ≠ b
hG'₀ : Ne (α := ENNReal) (liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop) ⊤
⊢ @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))

Tactic:
have integrable_f_deriv := integrable_of_tendsto hGf hG hG'₀