awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
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)
⊢ 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)
have _₂ : ENNReal.ofReal (g b - g a) = 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
⊢ IntervalIntegrable (deriv f) volume a b
have 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
Tactic: wlog hab : a ≤ b generalizing a b with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
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
⊢ IntervalIntegrable (deriv f) volume a b
have wlog : ∀ {a b : ℝ} (hf : MonotoneOn f (uIcc a b)) (hab : a ≤ b), IntervalIntegrable (deriv f) volume a b
Tactic: wlog hab : a ≤ b generalizing a b with h
Cleared hypotheses: a, b, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
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
⊢ b ≤ a
have linarith : a < b → b - a + (a - b) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
hab : a ≤ b
⊢ IntervalIntegrable (deriv f) volume a b
have hf₁ : MonotoneOn f (Icc a b)
Tactic: rw [uIcc_of_le hab] at hf
Cleared hypotheses: hf, hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
⊢ IntervalIntegrable (deriv f) volume a b
have 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
Tactic: obtain ⟨G, hGf, hG, hG'⟩ := hf.exists_tendsto_deriv_liminf_lintegral_enorm_le hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
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)
⊢ IntervalIntegrable (deriv f) volume a b
have hG'₀ : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
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) ⊤
⊢ IntervalIntegrable (deriv f) volume a b
have integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
Tactic: have integrable_f_deriv := integrable_of_tendsto hGf hG hG'₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
have 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)
Tactic: wlog hab : a ≤ b generalizing a b with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
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)
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
have 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)
Tactic: wlog hab : a ≤ b generalizing a b with h
Cleared hypotheses: a, b, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
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
⊢ b ≤ a
have linarith : a < b → b - a + (a - b) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
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 a..b, deriv f x ∈ uIcc 0 (f b - f a)
have h₁ : ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)
Tactic: specialize h (uIcc_comm a b ▸ hf) (by linarith)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
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 ≤ a
have linarith : a < b → b - a + (a - b) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
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)
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
have this : f b ≤ f a
Tactic: have : f b ≤ f a := hf (by simp) (by simp) (by linarith)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
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
⊢ f b - f a ≤ 0
have linarith : 0 < f b - f a → f b - f a + (0 - (f b - f a)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
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 a..b, deriv f x ∈ uIcc 0 (f b - f a)
have inr : -∫ (x : ℝ) in b..a, deriv f x ∈ Icc (f b - f a) 0
Tactic: rw [intervalIntegral.integral_symm, uIcc_of_ge (by linarith)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
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
have inr : ∫ (x : ℝ) in b..a, deriv f x ∈ Icc (-0) (-(f b - f a))
Tactic: refine neg_mem_Icc_iff.mpr ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
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 (-0) (-(f b - f a))
have inr : ∫ (x : ℝ) in b..a, deriv f x ∈ Icc 0 (f a - f b)
Tactic: simp only [neg_zero, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
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
⊢ 0 ≤ f a - f b
have linarith : f a - f b < 0 → f b - f a + (f a - f b - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
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 0 (f a - f b)
have 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)
Tactic: rwa [uIcc_of_le (by linarith)] at h
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
have hf₁ : MonotoneOn f (Icc a b)
Tactic: rw [uIcc_of_le hab] at hf
Cleared hypotheses: hf, hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
have 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)
Tactic: obtain ⟨G, hGf, hG, hG'⟩ := hf.exists_tendsto_deriv_liminf_lintegral_enorm_le hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
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 : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
have h₁ : ∀ᵐ (x : ℝ), x ≠ a
Tactic: have h₁ : ∀ᵐ x, x ≠ a := by simp [ae_iff, measure_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
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 : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
have h₂ : ∀ᵐ (x : ℝ), x ≠ b
Tactic: have h₂ : ∀ᵐ x, x ≠ b := by simp [ae_iff, measure_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
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
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
have hG'₀ : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
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) ⊤
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
have integrable_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
Tactic: have integrable_f_deriv := integrable_of_tendsto hGf hG hG'₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
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_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
have hGf₁ : ∀ᵐ (x : ℝ), x ∈ Icc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
Tactic: rw [MeasureTheory.ae_restrict_iff' (by simp)] at hGf
Cleared hypotheses: hGf, hG, hG', h₁, h₂, hG'₀, integrable_f_deriv
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ 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_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
have hGf₁ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
Tactic: rw [← uIcc_of_le hab] at hGf hG hG'
Cleared hypotheses: hGf, hG, hG', h₁, h₂, hG'₀, integrable_f_deriv
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ 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_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
hGf₁ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
have hG₁ : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
Tactic: rw [← uIcc_of_le hab] at hGf hG hG'
Cleared hypotheses: hGf, hG, hG', h₁, h₂, hG'₀, integrable_f_deriv
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ 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_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
hGf₁ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG₁ : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
have hG'₁ : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
Tactic: rw [← uIcc_of_le hab] at hGf hG hG'
Cleared hypotheses: hGf, hG, hG', h₁, h₂, hG'₀, integrable_f_deriv
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc 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_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
have this : f a ≤ f b
Tactic: have : f a ≤ f b := hf (by simp [hab]) (by simp [hab]) hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc 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_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
⊢ 0 ≤ f b - f a
have linarith : f b - f a < 0 → f a - f b + (f b - f a - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc 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_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
⊢ ∫ (x : ℝ) in a..b, deriv f x ∈ uIcc 0 (f b - f a)
have rw : LE.le (α := ℝ) 0 (∫ (x : ℝ) in a..b, deriv f x) ∧ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a
Tactic: rw [uIcc_of_le (by linarith), mem_Icc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (goal)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc 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_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
x : ℝ
hx : x ∈ Ioo a b
⊢ 0 ≤ deriv f x
have rw : 0 ≤ derivWithin f (Icc a b) x
Tactic: rw [← derivWithin_of_mem_nhds (Icc_mem_nhds (a := a) (b := b) (by grind) (by grind))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (uIcc a b))
hG' : liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in uIcc 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_f_deriv : @Integrable _ _ _ _ Real.measurableSpace (deriv f) (Measure.restrict volume (Icc a b))
this : f a ≤ f b
⊢ LE.le (α := ℝ) 0 (∫ (x : ℝ) in a..b, deriv f x) ∧ ∫ (x : ℝ) in a..b, deriv f x ≤ f b - f a
have f_deriv_nonneg : ∀ {x : ℝ} (hx : x ∈ Ioo a b), 0 ≤ deriv f x
Tactic: have f_deriv_nonneg {x : ℝ} (hx : x ∈ Ioo a b) : 0 ≤ deriv f x := by
    rw [← derivWithin_of_mem_nhds (Icc_mem_nhds (a := a) (b := b) (by grind) (by grind))]
    exact hf.derivWithin_nonneg