awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this_1 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 : ℝ | (fun (x_2 : ℝ) ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
r : ℝ
hr : r ∈ Ioo 0 (m - x)
this : r ∈ Ioc (r / 2) r
y : ℝ
hy : y ∈ Icc x (x + r)
z : ℝ
hz : z ∈ Icc x (x + r)
h₁ : z - x ≤ r
⊢ ‖z - x‖ ≤ r
have h₂ : 0 ≤ z - x
Tactic: rw [Real.norm_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this_1 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 : ℝ | (fun (x_2 : ℝ) ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
r : ℝ
hr : r ∈ Ioo 0 (m - x)
this : r ∈ Ioc (r / 2) r
y : ℝ
hy : y ∈ Icc x (x + r)
z : ℝ
hz : z ∈ Icc x (x + r)
⊢ z - x ≤ r
have linarith : r < z - x → r - (z - x) + (z - (x + r)) = 0
Tactic: linarith [hz.1, hz.2]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this_1 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 : ℝ | (fun (x_2 : ℝ) ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
r : ℝ
hr : r ∈ Ioo 0 (m - x)
this : r ∈ Ioc (r / 2) r
y : ℝ
hy : y ∈ Icc x (x + r)
z : ℝ
hz : z ∈ Icc x (x + r)
⊢ 0 ≤ z - x
have linarith : z - x < 0 → z - x - 0 + (x - z) = 0
Tactic: linarith [hz.1, hz.2]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this_1 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 : ℝ | (fun (x_2 : ℝ) ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
r : ℝ
hr : r ∈ Ioo 0 (m - x)
this : r ∈ Ioc (r / 2) r
y : ℝ
hy : y ∈ Icc x (x + r)
z : ℝ
hz : z ∈ Icc x (x + r)
⊢ ‖y - x‖ ≤ r
have h₂ : y - x ≤ r
Tactic: rw [Real.norm_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this_1 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 : ℝ | (fun (x_2 : ℝ) ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
r : ℝ
hr : r ∈ Ioo 0 (m - x)
this : r ∈ Ioc (r / 2) r
y : ℝ
hy : y ∈ Icc x (x + r)
z : ℝ
hz : z ∈ Icc x (x + r)
h₂ : y - x ≤ r
⊢ ‖y - x‖ ≤ r
have h₃ : 0 ≤ y - x
Tactic: rw [Real.norm_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this_1 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 : ℝ | (fun (x_2 : ℝ) ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
r : ℝ
hr : r ∈ Ioo 0 (m - x)
this : r ∈ Ioc (r / 2) r
y : ℝ
hy : y ∈ Icc x (x + r)
z : ℝ
hz : z ∈ Icc x (x + r)
⊢ y - x ≤ r
have linarith : r < y - x → r - (y - x) + (y - (x + r)) = 0
Tactic: linarith [hy.1, hy.2]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this_1 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 : ℝ | (fun (x_2 : ℝ) ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
r : ℝ
hr : r ∈ Ioo 0 (m - x)
this : r ∈ Ioc (r / 2) r
y : ℝ
hy : y ∈ Icc x (x + r)
z : ℝ
hz : z ∈ Icc x (x + r)
⊢ 0 ≤ y - x
have linarith : y - x < 0 → y - x - 0 + (x - y) = 0
Tactic: linarith [hy.1, hy.2]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this_1 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 : ℝ | (fun (x_2 : ℝ) ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
r : ℝ
hr : r ∈ Ioo 0 (m - x)
this : r ∈ Ioc (r / 2) r
y : ℝ
hy : y ∈ Icc x (x + r)
z : ℝ
hz : z ∈ Icc x (x + r)
⊢ ‖f z - f y - (z - y) • derivWithin f (Ici x) x‖ ≤ ε * r
have z₁ : ‖f z - f y - (z - y) • derivWithin f (Ici x) x‖ =
  ‖f z - f x - (z - x) • derivWithin f (Ici x) x - (f y - f x - (y - x) • derivWithin f (Ici x) x)‖
Tactic: calc
    ‖f z - f y - (z - y) • derivWithin f (Ici x) x‖ =
        ‖f z - f x - (z - x) • derivWithin f (Ici x) x -
            (f y - f x - (y - x) • derivWithin f (Ici x) x)‖ := by
      congr 1; simp only [sub_smul]; abel
    _ ≤
        ‖f z - f x - (z - x) • derivWithin f (Ici x) x‖ +
          ‖f y - f x - (y - x) • derivWithin f (Ici x) x‖ :=
      (norm_sub_le _ _)
    _ ≤ ε / 2 * ‖z - x‖ + ε / 2 * ‖y - x‖ :=
      (add_le_add (hm ⟨hz.1, hz.2.trans_lt (by linarith [hr.2])⟩)
        (hm ⟨hy.1, hy.2.trans_lt (by linarith [hr.2])⟩))
    _ ≤ ε / 2 * r + ε / 2 * r := by
      gcongr
      · rw [Real.norm_of_nonneg] <;> linarith [hz.1, hz.2]
      · rw [Real.norm_of_nonneg] <;> linarith [hy.1, hy.2]
    _ = ε * r := by ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this_1 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 : ℝ | (fun (x_2 : ℝ) ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
r : ℝ
hr : r ∈ Ioo 0 (m - x)
this : r ∈ Ioc (r / 2) r
y : ℝ
hy : y ∈ Icc x (x + r)
z : ℝ
hz : z ∈ Icc x (x + r)
z₁ :
  ‖f z - f y - (z - y) • derivWithin f (Ici x) x‖ =
    ‖f z - f x - (z - x) • derivWithin f (Ici x) x - (f y - f x - (y - x) • derivWithin f (Ici x) x)‖
⊢ ‖f z - f y - (z - y) • derivWithin f (Ici x) x‖ ≤ ε * r
have z₂ : ε / 2 * ‖z - x‖ + ε / 2 * ‖y - x‖ ≤ ε / 2 * r + ε / 2 * r
Tactic: calc
    ‖f z - f y - (z - y) • derivWithin f (Ici x) x‖ =
        ‖f z - f x - (z - x) • derivWithin f (Ici x) x -
            (f y - f x - (y - x) • derivWithin f (Ici x) x)‖ := by
      congr 1; simp only [sub_smul]; abel
    _ ≤
        ‖f z - f x - (z - x) • derivWithin f (Ici x) x‖ +
          ‖f y - f x - (y - x) • derivWithin f (Ici x) x‖ :=
      (norm_sub_le _ _)
    _ ≤ ε / 2 * ‖z - x‖ + ε / 2 * ‖y - x‖ :=
      (add_le_add (hm ⟨hz.1, hz.2.trans_lt (by linarith [hr.2])⟩)
        (hm ⟨hy.1, hy.2.trans_lt (by linarith [hr.2])⟩))
    _ ≤ ε / 2 * r + ε / 2 * r := by
      gcongr
      · rw [Real.norm_of_nonneg] <;> linarith [hz.1, hz.2]
      · rw [Real.norm_of_nonneg] <;> linarith [hy.1, hy.2]
    _ = ε * r := by ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this_1 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 : ℝ | (fun (x_2 : ℝ) ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
r : ℝ
hr : r ∈ Ioo 0 (m - x)
this : r ∈ Ioc (r / 2) r
y : ℝ
hy : y ∈ Icc x (x + r)
z : ℝ
hz : z ∈ Icc x (x + r)
z₁ :
  ‖f z - f y - (z - y) • derivWithin f (Ici x) x‖ =
    ‖f z - f x - (z - x) • derivWithin f (Ici x) x - (f y - f x - (y - x) • derivWithin f (Ici x) x)‖
z₂ : ε / 2 * ‖z - x‖ + ε / 2 * ‖y - x‖ ≤ ε / 2 * r + ε / 2 * r
⊢ ‖f z - f y - (z - y) • derivWithin f (Ici x) x‖ ≤ ε * r
have z₃ : ε / 2 * r + ε / 2 * r = ε * r
Tactic: calc
    ‖f z - f y - (z - y) • derivWithin f (Ici x) x‖ =
        ‖f z - f x - (z - x) • derivWithin f (Ici x) x -
            (f y - f x - (y - x) • derivWithin f (Ici x) x)‖ := by
      congr 1; simp only [sub_smul]; abel
    _ ≤
        ‖f z - f x - (z - x) • derivWithin f (Ici x) x‖ +
          ‖f y - f x - (y - x) • derivWithin f (Ici x) x‖ :=
      (norm_sub_le _ _)
    _ ≤ ε / 2 * ‖z - x‖ + ε / 2 * ‖y - x‖ :=
      (add_le_add (hm ⟨hz.1, hz.2.trans_lt (by linarith [hr.2])⟩)
        (hm ⟨hy.1, hy.2.trans_lt (by linarith [hr.2])⟩))
    _ ≤ ε / 2 * r + ε / 2 * r := by
      gcongr
      · rw [Real.norm_of_nonneg] <;> linarith [hz.1, hz.2]
      · rw [Real.norm_of_nonneg] <;> linarith [hy.1, hy.2]
    _ = ε * r := by ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
H : ‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε)
⊢ ‖L₁ - L₂‖ ≤ 4 * ε
have rwa : ∀ (H : ‖r / 2‖ * ‖L₁ - L₂‖ ≤ r / 2 * (4 * ε)), ‖L₁ - L₂‖ ≤ 4 * ε
Tactic: rwa [norm_smul, Real.norm_of_nonneg (half_pos hr).le, mul_le_mul_iff_right₀ (half_pos hr)] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
H : ‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε)
rwa : ∀ (H : ‖r / 2‖ * ‖L₁ - L₂‖ ≤ r / 2 * (4 * ε)), ‖L₁ - L₂‖ ≤ 4 * ε
⊢ ‖L₁ - L₂‖ ≤ 4 * ε
have rwa₁ : ∀ (H : r / 2 * ‖L₁ - L₂‖ ≤ r / 2 * (4 * ε)), ‖L₁ - L₂‖ ≤ 4 * ε
Tactic: rwa [norm_smul, Real.norm_of_nonneg (half_pos hr).le, mul_le_mul_iff_right₀ (half_pos hr)] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
H : ‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε)
rwa : ∀ (H : ‖r / 2‖ * ‖L₁ - L₂‖ ≤ r / 2 * (4 * ε)), ‖L₁ - L₂‖ ≤ 4 * ε
rwa₁ : ∀ (H : r / 2 * ‖L₁ - L₂‖ ≤ r / 2 * (4 * ε)), ‖L₁ - L₂‖ ≤ 4 * ε
⊢ ‖L₁ - L₂‖ ≤ 4 * ε
have rwa₂ : ∀ (H : ‖L₁ - L₂‖ ≤ 4 * ε), ‖L₁ - L₂‖ ≤ 4 * ε
Tactic: rwa [norm_smul, Real.norm_of_nonneg (half_pos hr).le, mul_le_mul_iff_right₀ (half_pos hr)] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖L₁ - L₂‖ ≤ 4 * ε
have suffices : ‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε)
Tactic: suffices H : ‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε) by
    rwa [norm_smul, Real.norm_of_nonneg (half_pos hr).le, mul_le_mul_iff_right₀ (half_pos hr)] at H
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ + ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖ ≤ ε * r + ε * r
have h₃ : ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ ≤ ε * r
Tactic: apply add_le_add
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
h₃ : ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ ≤ ε * r
⊢ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ + ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖ ≤ ε * r + ε * r
have h₄ : ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖ ≤ ε * r
Tactic: apply add_le_add
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ ≤ ε * r
have h₃ : x ∈ Icc x (x + r / 2)
Tactic: apply le_of_mem_A h₂
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
h₃ : x ∈ Icc x (x + r / 2)
⊢ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ ≤ ε * r
have h₄ : x + r / 2 ∈ Icc x (x + r / 2)
Tactic: apply le_of_mem_A h₂
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖ ≤ ε * r
have h₃ : x ∈ Icc x (x + r / 2)
Tactic: apply le_of_mem_A h₁
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
h₃ : x ∈ Icc x (x + r / 2)
⊢ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖ ≤ ε * r
have h₄ : x + r / 2 ∈ Icc x (x + r / 2)
Tactic: apply le_of_mem_A h₁
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε)
have r₁ : ‖(r / 2) • (L₁ - L₂)‖ = ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂ - (f (x + r / 2) - f x - (x + r / 2 - x) • L₁)‖
Tactic: calc
    ‖(r / 2) • (L₁ - L₂)‖ =
        ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂ -
            (f (x + r / 2) - f x - (x + r / 2 - x) • L₁)‖ := by
      simp [smul_sub]
    _ ≤ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ +
          ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖ :=
      norm_sub_le _ _
    _ ≤ ε * r + ε * r := by
      apply add_le_add
      · apply le_of_mem_A h₂ <;> simp [(half_pos hr).le]
      · apply le_of_mem_A h₁ <;> simp [(half_pos hr).le]
    _ = r / 2 * (4 * ε) := by ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
r₁ : ‖(r / 2) • (L₁ - L₂)‖ = ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂ - (f (x + r / 2) - f x - (x + r / 2 - x) • L₁)‖
⊢ ‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε)
have r₂ : ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ + ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖ ≤ ε * r + ε * r
Tactic: calc
    ‖(r / 2) • (L₁ - L₂)‖ =
        ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂ -
            (f (x + r / 2) - f x - (x + r / 2 - x) • L₁)‖ := by
      simp [smul_sub]
    _ ≤ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ +
          ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖ :=
      norm_sub_le _ _
    _ ≤ ε * r + ε * r := by
      apply add_le_add
      · apply le_of_mem_A h₂ <;> simp [(half_pos hr).le]
      · apply le_of_mem_A h₁ <;> simp [(half_pos hr).le]
    _ = r / 2 * (4 * ε) := by ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
r x : ℝ
hr : 0 < r
ε : ℝ
L₁ L₂ : F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
r₁ : ‖(r / 2) • (L₁ - L₂)‖ = ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂ - (f (x + r / 2) - f x - (x + r / 2 - x) • L₁)‖
r₂ : ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ + ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖ ≤ ε * r + ε * r
⊢ ‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε)
have r₃ : ε * r + ε * r = r / 2 * (4 * ε)
Tactic: calc
    ‖(r / 2) • (L₁ - L₂)‖ =
        ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂ -
            (f (x + r / 2) - f x - (x + r / 2 - x) • L₁)‖ := by
      simp [smul_sub]
    _ ≤ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ +
          ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖ :=
      norm_sub_le _ _
    _ ≤ ε * r + ε * r := by
      apply add_le_add
      · apply le_of_mem_A h₂ <;> simp [(half_pos hr).le]
      · apply le_of_mem_A h₁ <;> simp [(half_pos hr).le]
    _ = r / 2 * (4 * ε) := by ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : Membership.mem (γ := Set ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} x
⊢ x ∈ D f K
have rw : ∀ (i : ℕ),
  Membership.mem (γ := Set ℝ)
    (⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ i)) x
Tactic: rw [D, mem_iInter]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : Membership.mem (γ := Set ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} x
e : ℕ
⊢ Membership.mem (γ := Set ℝ)
    (⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)) x
have this : 0 < (1 / 2) ^ e
Tactic: have : (0 : ℝ) < (1 / 2) ^ e := pow_pos (by norm_num) _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : Membership.mem (γ := Set ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} x
e : ℕ
this : 0 < (1 / 2) ^ e
⊢ Membership.mem (γ := Set ℝ)
    (⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)) x
have rcases : ∀ (R : ℝ) (R_pos : R > 0) (hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)),
  Membership.mem (γ := Set ℝ)
    (⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)) x
Tactic: rcases mem_A_of_differentiable this hx.1 with ⟨R, R_pos, hR⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : Membership.mem (γ := Set ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} x
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)
⊢ Membership.mem (γ := Set ℝ)
    (⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)) x
have obtain : ∀ (n : ℕ) (hn : (1 / 2) ^ n < R),
  Membership.mem (γ := Set ℝ)
    (⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)) x
Tactic: obtain ⟨n, hn⟩ : ∃ n : ℕ, (1 / 2) ^ n < R :=
    exists_pow_lt_of_lt_one R_pos (by norm_num : (1 : ℝ) / 2 < 1)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : Membership.mem (γ := Set ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} x
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
⊢ Membership.mem (γ := Set ℝ)
    (⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)) x
have simp : ∃ (i : ℕ),
  ∀ (i_1 : ℕ) (i_2 : i_1 ≥ i) (i_3 : ℕ) (i : i_3 ≥ i),
    ∃ (i : F) (_ : i ∈ K), x ∈ A f i ((1 / 2) ^ i_1) ((1 / 2) ^ e) ∧ x ∈ A f i ((1 / 2) ^ i_3) ((1 / 2) ^ e)
Tactic: simp only [mem_iUnion, mem_iInter, B, mem_inter_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : Membership.mem (γ := Set ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} x
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
⊢ ∃ (i : ℕ),
    ∀ (i_1 : ℕ) (i_2 : i_1 ≥ i) (i_3 : ℕ) (i : i_3 ≥ i),
      ∃ (i : F) (_ : i ∈ K), x ∈ A f i ((1 / 2) ^ i_1) ((1 / 2) ^ e) ∧ x ∈ A f i ((1 / 2) ^ i_3) ((1 / 2) ^ e)
have refine_1 : ∀ (p : ℕ) (hp : p ≥ n) (q : ℕ) (hq : q ≥ n), x ∈ A f (derivWithin f (Ici x) x) ((1 / 2) ^ p) ((1 / 2) ^ e)
Tactic: refine ⟨n, fun p hp q hq => ⟨derivWithin f (Ici x) x, hx.2, ⟨?_, ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : Membership.mem (γ := Set ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} x
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
refine_1 : ∀ (p : ℕ) (hp : p ≥ n) (q : ℕ) (hq : q ≥ n), x ∈ A f (derivWithin f (Ici x) x) ((1 / 2) ^ p) ((1 / 2) ^ e)
⊢ ∃ (i : ℕ),
    ∀ (i_1 : ℕ) (i_2 : i_1 ≥ i) (i_3 : ℕ) (i : i_3 ≥ i),
      ∃ (i : F) (_ : i ∈ K), x ∈ A f i ((1 / 2) ^ i_1) ((1 / 2) ^ e) ∧ x ∈ A f i ((1 / 2) ^ i_3) ((1 / 2) ^ e)
have refine_2 : ∀ (p : ℕ) (hp : p ≥ n) (q : ℕ) (hq : q ≥ n), x ∈ A f (derivWithin f (Ici x) x) ((1 / 2) ^ q) ((1 / 2) ^ e)
Tactic: refine ⟨n, fun p hp q hq => ⟨derivWithin f (Ici x) x, hx.2, ⟨?_, ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : Membership.mem (γ := Set ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} x
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
p : ℕ
hp : p ≥ n
q : ℕ
hq : q ≥ n
⊢ x ∈ A f (derivWithin f (Ici x) x) ((1 / 2) ^ p) ((1 / 2) ^ e)
have refine_1 : (1 / 2) ^ p ≤ (1 / 2) ^ n
Tactic: refine hR _ ⟨pow_pos (by norm_num) _, lt_of_le_of_lt ?_ hn⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : Membership.mem (γ := Set ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} x
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
p : ℕ
hp : p ≥ n
q : ℕ
hq : q ≥ n
⊢ x ∈ A f (derivWithin f (Ici x) x) ((1 / 2) ^ q) ((1 / 2) ^ e)
have refine_2 : (1 / 2) ^ q ≤ (1 / 2) ^ n
Tactic: refine hR _ ⟨pow_pos (by norm_num) _, lt_of_le_of_lt ?_ hn⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
⊢ D f K ⊆ {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
have P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
Tactic: have P : ∀ {n : ℕ}, (0 : ℝ) < (1 / 2) ^ n := fun {n} => pow_pos (by norm_num) n