awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ = ∫⁻ (x : ℝ) in Icc a b, ‖derivWithin f (Icc a b) x‖ₑ
have h₁ : (ae (F := Measure ℝ) (Measure.restrict volume (Icc a b))).EventuallyEq (β := ℝ≥0∞) (fun (a : ℝ) ↦ ‖deriv f a‖ₑ)
  fun (a_1 : ℝ) ↦ ‖derivWithin f (Icc a b) a_1‖ₑ
Tactic: apply lintegral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Icc a b))).EventuallyEq (β := ℝ≥0∞) (fun (a : ℝ) ↦ ‖deriv f a‖ₑ)
    fun (a_1 : ℝ) ↦ ‖derivWithin f (Icc a b) a_1‖ₑ
have h₁ : (ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))).EventuallyEq (β := ℝ≥0∞) (fun (a : ℝ) ↦ ‖deriv f a‖ₑ)
  fun (a_1 : ℝ) ↦ ‖derivWithin f (Icc a b) a_1‖ₑ
Tactic: rw [← restrict_Ioo_eq_restrict_Icc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioo a b))).EventuallyEq (β := ℝ≥0∞) (fun (a : ℝ) ↦ ‖deriv f a‖ₑ)
    fun (a_1 : ℝ) ↦ ‖derivWithin f (Icc a b) a_1‖ₑ
have h₁ : ∀ (x : ℝ) (hx : x ∈ Ioo a b), ‖deriv f x‖ₑ = ‖derivWithin f (Icc a b) x‖ₑ
Tactic: filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
x : ℝ
hx : x ∈ Ioo a b
⊢ ‖deriv f x‖ₑ = ‖derivWithin f (Icc a b) x‖ₑ
have h₁ : ‖deriv f x‖ₑ = ‖deriv f x‖ₑ
Tactic: rw [derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
Goal:
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f (max a (min x b))
⊢ ∃ (G : ℕ → ℝ → ℝ),
    (∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))) ∧
      (∀ (n : ℕ),
          AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))) ∧
        liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
have hg : Monotone g
Tactic: have hg : Monotone g := monotoneOn_univ.mp <| hf.comp (by grind [MonotoneOn]) (by grind [MapsTo])
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
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
⊢ ∃ (G : ℕ → ℝ → ℝ),
    (∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))) ∧
      (∀ (n : ℕ),
          AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))) ∧
        liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
have hfg : EqOn f g (Ioo a b)
Tactic: have hfg : EqOn f g (Ioo a b) := by grind [EqOn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
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 f g (Ioo a b)
⊢ ∃ (G : ℕ → ℝ → ℝ),
    (∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))) ∧
      (∀ (n : ℕ),
          AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))) ∧
        liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
have hfg₁ : EqOn (deriv f) (deriv g) (Ioo a b)
Tactic: replace hfg := hfg.deriv isOpen_Ioo
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
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)
⊢ ∃ (G : ℕ → ℝ → ℝ),
    (∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))) ∧
      (∀ (n : ℕ),
          AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))) ∧
        liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (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 : ℝ
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
⊢ ∃ (G : ℕ → ℝ → ℝ),
    (∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))) ∧
      (∀ (n : ℕ),
          AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))) ∧
        liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (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 : ℝ
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)
n : ℕ
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
have this : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ slope g x (x + (↑n : ℝ)⁻¹)) volume a b
Tactic: have := hg.monotoneOn (Icc a (b + (n : ℝ)⁻¹)) |>.intervalIntegrable_slope hab (by simp)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable (hypothesis)
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 : ℕ → ℝ → ℝ),
    (∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))) ∧
      (∀ (n : ℕ),
          AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))) ∧
        liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
have G_integrable : ∀ (n : ℕ), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (G (↑n : ℝ)⁻¹) (Measure.restrict volume (Icc a b))
Tactic: have G_integrable (n : ℕ) : Integrable (G (↑n)⁻¹) (volume.restrict (Icc a b)) := by
    have := hg.monotoneOn (Icc a (b + (n : ℝ)⁻¹)) |>.intervalIntegrable_slope hab (by simp)
    exact intervalIntegrable_iff_integrableOn_Icc_of_le hab |>.mp this
-- 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))
⊢ ∃ (G : ℕ → ℝ → ℝ),
    (∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))) ∧
      (∀ (n : ℕ),
          AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))) ∧
        liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
have refine_1 : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b),
  Tendsto (fun (n : ℕ) ↦ (fun (n : ℕ) (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) n x) atTop (𝓝 (deriv f x))
Tactic: refine ⟨fun n x ↦ G (n : ℝ)⁻¹ x, ?_, fun n ↦ G_integrable n |>.aestronglyMeasurable, ?_⟩
-- 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))
refine_1 :
  ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b),
    Tendsto (fun (n : ℕ) ↦ (fun (n : ℕ) (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) n x) atTop (𝓝 (deriv f x))
⊢ ∃ (G : ℕ → ℝ → ℝ),
    (∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b), Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (deriv f x))) ∧
      (∀ (n : ℕ),
          AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (G n) (Measure.restrict volume (Icc a b))) ∧
        liminf (fun (n : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
have refine_2 : 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: refine ⟨fun n x ↦ G (n : ℝ)⁻¹ x, ?_, fun n ↦ G_integrable n |>.aestronglyMeasurable, ?_⟩
-- 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))
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Icc a b),
    Tendsto (fun (n : ℕ) ↦ (fun (n : ℕ) (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) n x) atTop (𝓝 (deriv f x))
have refine_1 : ∀ᵐ (x : ℝ), x ∈ Icc a b → Tendsto (fun (n : ℕ) ↦ (fun (n : ℕ) (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) n x) atTop (𝓝 (deriv f x))
Tactic: rw [MeasureTheory.ae_restrict_iff' (by measurability)]
-- 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))
⊢ ∀ᵐ (x : ℝ), x ∈ Icc a b → Tendsto (fun (n : ℕ) ↦ (fun (n : ℕ) (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) n x) atTop (𝓝 (deriv f x))
have h : ∀ (x : ℝ) (hx₁ : DifferentiableAt ℝ g x) (hx₂ : x ≠ a) (hx₃ : x ≠ b) (hx₄ : x ∈ Icc a b),
  Tendsto (fun (n : ℕ) ↦ G (↑n : ℝ)⁻¹ x) atTop (𝓝 (deriv f x))
Tactic: filter_upwards [hg.ae_differentiableAt, h₁, h₂] with x hx₁ hx₂ hx₃ hx₄
-- 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))
x : ℝ
hx₁ : DifferentiableAt ℝ g x
hx₂ : x ≠ a
hx₃ : x ≠ b
hx₄ : x ∈ Icc a b
⊢ Tendsto (fun (n : ℕ) ↦ G (↑n : ℝ)⁻¹ x) atTop (𝓝 (deriv f x))
have h : Tendsto (fun (n : ℕ) ↦ G (↑n : ℝ)⁻¹ x) atTop (𝓝 (deriv g x))
Tactic: rw [hfg (by grind [Icc_diff_both])]
-- 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))
x : ℝ
hx₁ : DifferentiableAt ℝ g x
hx₂ : x ≠ a
hx₃ : x ≠ b
hx₄ : x ∈ Icc a b
⊢ Tendsto (fun (n : ℕ) ↦ x + (↑n : ℝ)⁻¹) atTop (𝓝 x)
have h : x = x + 0
Tactic: convert! tendsto_const_nhds.add (tendsto_inv_atTop_nhds_zero_nat (𝕜 := ℝ))
-- 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)
have h : ∀ᶠ (a_1 : ℕ) in atTop,
  ∫⁻ (x : ℝ) in Icc a b, enorm (E := ℝ) ((fun (n : ℕ) (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) a_1 x) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
        G (↑a_1 : ℝ)⁻¹ x)
Tactic: apply Filter.liminf_congr
-- 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))
⊢ ∀ᶠ (a_1 : ℕ) in atTop,
    ∫⁻ (x : ℝ) in Icc a b, enorm (E := ℝ) ((fun (n : ℕ) (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) a_1 x) =
      ENNReal.ofReal
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
          G (↑a_1 : ℝ)⁻¹ x)
have h : ∀ (n : ℕ),
  ∫⁻ (x : ℝ) in Icc a b, ‖G (↑n : ℝ)⁻¹ x‖ₑ =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
        G (↑n : ℝ)⁻¹ x)
Tactic: filter_upwards with n
-- 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))
n : ℕ
⊢ ∫⁻ (x : ℝ) in Icc a b, ‖G (↑n : ℝ)⁻¹ x‖ₑ =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
        G (↑n : ℝ)⁻¹ x)
have h : ENNReal.ofReal
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
      ‖G (↑n : ℝ)⁻¹ x‖) =
  ENNReal.ofReal
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x)
Tactic: rw [← MeasureTheory.ofReal_integral_norm_eq_lintegral_enorm (G_integrable n)]
-- 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))
n : ℕ
⊢ ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
        ‖G (↑n : ℝ)⁻¹ x‖) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦
        G (↑n : ℝ)⁻¹ x)
have h : ∀ (y : ℝ), ‖G (↑n : ℝ)⁻¹ y‖ = G (↑n : ℝ)⁻¹ y
Tactic: congr with y
-- 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))
⊢ 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)
have refine : ∀ (n : ℕ),
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) ≤
    g b - g a
Tactic: refine Filter.liminf_le_of_frequently_le'
          (Filter.Frequently.of_forall fun n ↦ ENNReal.ofReal_le_ofReal ?_)
-- 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))
n : ℕ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) ≤
    g b - g a
have rw : ∫ (x : ℝ) in a..b, G (↑n : ℝ)⁻¹ x ≤ g b - g a
Tactic: rw [integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le hab]
-- 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))
n : ℕ
⊢ ∫ (x : ℝ) in a..b, G (↑n : ℝ)⁻¹ x ≤ g b - g a
have h : g b = g (b + (↑n : ℝ)⁻¹)
Tactic: convert!
          hg.monotoneOn (Icc a (b + (n : ℝ)⁻¹)) |>.intervalIntegral_slope_le hab (by simp) using 2
-- 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))
⊢ 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 _ : 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)
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 : ℝ
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 : ℕ) ↦ ∫⁻ (x : ℝ) in Icc a b, enorm (E := ℝ) ((fun (n : ℕ) (x : ℝ) ↦ G (↑n : ℝ)⁻¹ x) n x)) atTop ≤
    ENNReal.ofReal (f b - f a)
have _₁ : 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: 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