awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : d ∈ Icc a b
r : ℝ
hr : r > 0
⊢ dist (f d) (f b) ≤ r
have rw : ∀ (hd : a ≤ d ∧ d ≤ b) (r : ℝ) (hr : r > 0), dist (f d) (f b) ≤ r
Tactic: rw [mem_Icc] at hd
Cleared hypotheses: hd, r, hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
⊢ a ≤ d
have linarith : d < a → a - d + (d - a) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
⊢ dist (f d) (f b) ≤ r
have had : a ≤ d
Tactic: have had : a ≤ d := by linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
⊢ dist (f d) (f b) ≤ r
have inl : ∀ (hf : AbsolutelyContinuousOnInterval f a d) (hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a d → HasDerivAt f 0 x) (hab : a ≤ d)
  (hd : a ≤ d ∧ d ≤ d), dist (f d) (f d) ≤ r
Tactic: rcases hd.right.eq_or_lt with rfl | hdb
Cleared hypotheses: b, hf, hf₀, hab, hd
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
inl :
  ∀ (hf : AbsolutelyContinuousOnInterval f a d) (hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a d → HasDerivAt f 0 x) (hab : a ≤ d)
    (hd : a ≤ d ∧ d ≤ d), dist (f d) (f d) ≤ r
⊢ dist (f d) (f b) ≤ r
have inr : ∀ (hdb : d < b), dist (f d) (f b) ≤ r
Tactic: rcases hd.right.eq_or_lt with rfl | hdb
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
⊢ ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
have h : ∀ (a_1 : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ Icc a b → HasDerivAt f 0 x) x} x →
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ Ioo d b → HasDerivAt f 0 x) x} x}
    a_1
Tactic: filter_upwards [hf₀] with x _ _ using by grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
h :
  ∀ (a_1 : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ Icc a b → HasDerivAt f 0 x) x} x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ Ioo d b → HasDerivAt f 0 x) x} x}
      a_1
⊢ ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
have h₁ : ∀ (a_1 : ℝ), (a_1 ∈ Icc a b → HasDerivAt f 0 a_1) → a_1 ∈ Ioo d b → HasDerivAt f 0 a_1
Tactic: filter_upwards [hf₀] with x _ _ using by grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
⊢ dist (f d) (f b) ≤ r
have hf₁ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
Tactic: replace hf₀ : ∀ᵐ x, x ∈ Ioo d b → HasDerivAt f 0 x := by
    filter_upwards [hf₀] with x _ _ using by grind
Cleared hypotheses: hf₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
⊢ 0 < r / (b - d)
have ha : 0 < r
Tactic: apply div_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
ha : 0 < r
⊢ 0 < r / (b - d)
have hb : 0 < b - d
Tactic: apply div_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
⊢ 0 < r
have linarith : r ≤ 0 → 0 - r + (r - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
⊢ 0 < b - d
have linarith : b - d ≤ 0 → d - b + (b - d - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
⊢ dist (f d) (f b) ≤ r
have hfdb' : 0 < r / (b - d)
Tactic: have hfdb' : 0 < r / (b - d) := by apply div_pos <;> linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
⊢ dist (f d) (f b) ≤ r
have inr : ∀ (u : Set (ℝ × ℝ)) (hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d))
  (hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2)
  (hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)), dist (f d) (f b) ≤ r
Tactic: have ⟨u, hu₁, hu₂, hu₃⟩ :=
    exists_dist_slope_lt_pairwiseDisjoint_hasSum hd.right hf₀ hfdb'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
⊢ dist (f d) (f b) ≤ r
have g_nonneg : 0 ≤ g
Tactic: have g_nonneg : 0 ≤ g := by intro; simp [g]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
z : (↑u : Type)
hz : z ∈ s
⊢ g z ≤ r / (b - d) * ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)
have slope_bound : dist (slope f (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2) 0 ≤ r / (b - d)
Tactic: have slope_bound := hu₁ z (by simp) |>.right |>.le
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
z : (↑u : Type)
hz : z ∈ s
slope_bound : dist (slope f (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2) 0 ≤ r / (b - d)
⊢ 0 < (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1
have linarith : (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1 ≤ 0 → (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1 - 0 + ((↑z : ℝ × ℝ).1 - (↑z : ℝ × ℝ).2) = 0
Tactic: linarith [hu₁ z (by simp)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
z : (↑u : Type)
hz : z ∈ s
slope_bound : dist (slope f (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2) 0 ≤ r / (b - d)
⊢ g z ≤ r / (b - d) * ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)
have this : 0 < (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1
Tactic: have : 0 < z.val.2 - z.val.1 := by linarith [hu₁ z (by simp)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
z : (↑u : Type)
hz : z ∈ s
slope_bound : dist (slope f (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2) 0 ≤ r / (b - d)
this : 0 < (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1
⊢ g z ≤ r / (b - d) * ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)
have grw : g z ≤ dist (slope f (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2) 0 * ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)
Tactic: grw [← slope_bound]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
z : (↑u : Type)
hz : z ∈ s
slope_bound : dist (slope f (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2) 0 ≤ r / (b - d)
this : 0 < (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1
⊢ g z ≤ dist (slope f (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2) 0 * ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)
have simp : ‖f (↑z : ℝ × ℝ).1 - f (↑z : ℝ × ℝ).2‖ ≤
  ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) * ‖((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)⁻¹ • (f (↑z : ℝ × ℝ).2 - f (↑z : ℝ × ℝ).1)‖
Tactic: simp only [dist_eq_norm, slope, vsub_eq_sub, sub_zero, ge_iff_le, g, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
z : (↑u : Type)
hz : z ∈ s
slope_bound : dist (slope f (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2) 0 ≤ r / (b - d)
this : 0 < (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1
⊢ ‖f (↑z : ℝ × ℝ).1 - f (↑z : ℝ × ℝ).2‖ ≤
    ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) * ‖((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)⁻¹ • (f (↑z : ℝ × ℝ).2 - f (↑z : ℝ × ℝ).1)‖
have nth_rw : ‖f (↑z : ℝ × ℝ).1 - f (↑z : ℝ × ℝ).2‖ ≤
  ‖(↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1‖ * ‖((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)⁻¹ • (f (↑z : ℝ × ℝ).2 - f (↑z : ℝ × ℝ).1)‖
Tactic: nth_rw 1 [← Real.norm_of_nonneg this.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
z : (↑u : Type)
hz : z ∈ s
slope_bound : dist (slope f (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2) 0 ≤ r / (b - d)
this : 0 < (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1
⊢ ‖f (↑z : ℝ × ℝ).1 - f (↑z : ℝ × ℝ).2‖ ≤
    ‖(↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1‖ * ‖((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)⁻¹ • (f (↑z : ℝ × ℝ).2 - f (↑z : ℝ × ℝ).1)‖
have simp : ‖f (↑z : ℝ × ℝ).1 - f (↑z : ℝ × ℝ).2‖ ≤
  |(↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1| * (|(↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1|⁻¹ * ‖f (↑z : ℝ × ℝ).2 - f (↑z : ℝ × ℝ).1‖)
Tactic: simp only [norm_smul, Real.norm_eq_abs, norm_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
z : (↑u : Type)
hz : z ∈ s
slope_bound : dist (slope f (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2) 0 ≤ r / (b - d)
this : 0 < (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1
⊢ ‖f (↑z : ℝ × ℝ).1 - f (↑z : ℝ × ℝ).2‖ ≤
    |(↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1| * (|(↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1|⁻¹ * ‖f (↑z : ℝ × ℝ).2 - f (↑z : ℝ × ℝ).1‖)
have field_simp : ‖f (↑z : ℝ × ℝ).1 - f (↑z : ℝ × ℝ).2‖ ≤ ‖f (↑z : ℝ × ℝ).2 - f (↑z : ℝ × ℝ).1‖
Tactic: field_simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
z : (↑u : Type)
hz : z ∈ s
slope_bound : dist (slope f (↑z : ℝ × ℝ).1 (↑z : ℝ × ℝ).2) 0 ≤ r / (b - d)
this : 0 < (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1
⊢ ‖f (↑z : ℝ × ℝ).1 - f (↑z : ℝ × ℝ).2‖ ≤ ‖f (↑z : ℝ × ℝ).2 - f (↑z : ℝ × ℝ).1‖
have rw : ‖f (↑z : ℝ × ℝ).2 - f (↑z : ℝ × ℝ).1‖ ≤ ‖f (↑z : ℝ × ℝ).2 - f (↑z : ℝ × ℝ).1‖
Tactic: rw [norm_sub_rev]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (hypothesis)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
⊢ ∑ z ∈ s, g z ≤ r
have this : ∀ (z : (↑u : Type)) (hz : z ∈ s), g z ≤ r / (b - d) * ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)
Tactic: have (z : u) (hz : z ∈ s) : g z ≤ r / (b - d) * (z.val.2 - z.val.1) := by
      have slope_bound := hu₁ z (by simp) |>.right |>.le
      have : 0 < z.val.2 - z.val.1 := by linarith [hu₁ z (by simp)]
      grw [← slope_bound]
      simp only [dist_eq_norm, slope, vsub_eq_sub, sub_zero, ge_iff_le, g, mul_comm]
      nth_rw 1 [← Real.norm_of_nonneg this.le]
      simp only [norm_smul, Real.norm_eq_abs, norm_inv]
      field_simp
      rw [norm_sub_rev]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
this : ∀ (z : (↑u : Type)) (hz : z ∈ s), g z ≤ r / (b - d) * ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)
⊢ ∑ z ∈ s, g z ≤ r
have grw : ∑ i ∈ s, r / (b - d) * ((↑i : ℝ × ℝ).2 - (↑i : ℝ × ℝ).1) ≤ r
Tactic: grw [Finset.sum_le_sum this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun (goal)
Goal:
F_1 : Type u_2
inst : NormedAddCommGroup F_1
inst_1 : NormedSpace ℝ F_1
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint (α := Set ℝ) fun (z : ℝ × ℝ) ↦ Icc z.1 z.2
hu₃ : HasSum (fun (z : (↑u : Type)) ↦ (↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1) (b - d)
g : (z : (↑u : Type)) → ℝ := fun (z : (↑u : Type)) ↦ dist (f (↑z : ℝ × ℝ).1) (f (↑z : ℝ × ℝ).2)
g_nonneg : 0 ≤ g
s : Finset (↑u : Type)
this : ∀ (z : (↑u : Type)) (hz : z ∈ s), g z ≤ r / (b - d) * ((↑z : ℝ × ℝ).2 - (↑z : ℝ × ℝ).1)
⊢ ∑ i ∈ s, r / (b - d) * ((↑i : ℝ × ℝ).2 - (↑i : ℝ × ℝ).1) ≤ r
have rw : r / (b - d) * ∑ i ∈ s, ((↑i : ℝ × ℝ).2 - (↑i : ℝ × ℝ).1) ≤ r
Tactic: rw [← Finset.mul_sum]