awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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)
e_a :
  f z - f y - (z • derivWithin f (Ici x) x - y • derivWithin f (Ici x) x) =
    f z - f x - (z • derivWithin f (Ici x) x - x • derivWithin f (Ici x) x) -
      (f y - f x - (y • derivWithin f (Ici x) x - x • derivWithin f (Ici x) x))
⊢ 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:
simp only [sub_smul]

Premises used: sub_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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 • derivWithin f (Ici x) x - y • derivWithin f (Ici x) x) =
    f z - f x - (z • derivWithin f (Ici x) x - x • derivWithin f (Ici x) x) -
      (f y - f x - (y • derivWithin f (Ici x) x - x • derivWithin f (Ici x) x))

Tactic:
abel
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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 x - (z - x) • derivWithin f (Ici x) x - (f y - f x - (y - x) • 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:
(norm_sub_le _ _)

Premises used: norm_sub_le
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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)
linarith : m ≤ x + r → m - (x + r) + (r - (m - x)) = 0
⊢ x + r < m

Tactic:
linarith [hr.2]

Premises used: And.right
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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
h₂ : ‖y - x‖ ≤ r
⊢ ε / 2 * ‖z - x‖ + ε / 2 * ‖y - x‖ ≤ ε / 2 * r + ε / 2 * r

Tactic:
gcongr
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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
h₂ : 0 ≤ z - x
⊢ ‖z - x‖ ≤ r

Tactic:
rw [Real.norm_of_nonneg]

Premises used: Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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)
linarith : r < z - x → r - (z - x) + (z - (x + r)) = 0
⊢ z - x ≤ r

Tactic:
linarith [hz.1, hz.2]

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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)
linarith : z - x < 0 → z - x - 0 + (x - z) = 0
⊢ 0 ≤ z - x

Tactic:
linarith [hz.1, hz.2]

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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
h₃ : 0 ≤ y - x
⊢ ‖y - x‖ ≤ r

Tactic:
rw [Real.norm_of_nonneg]

Premises used: Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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)
linarith : r < y - x → r - (y - x) + (y - (x + r)) = 0
⊢ y - x ≤ r

Tactic:
linarith [hy.1, hy.2]

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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)
linarith : y - x < 0 → y - x - 0 + (x - y) = 0
⊢ 0 ≤ y - x

Tactic:
linarith [hy.1, hy.2]

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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)
⊢ ε / 2 * r + ε / 2 * r = ε * r

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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
z₃ : ε / 2 * r + ε / 2 * r = ε * r
⊢ ‖f z - f y - (z - y) • derivWithin f (Ici x) x‖ ≤ ε * 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

Premises used: Set.Ici, norm_sub_le, add_le_add, HSub.hSub, derivWithin, HSMul.hSMul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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 * ε
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (H : ‖L₁ - L₂‖ ≤ 4 * ε), ‖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

Premises used: norm_smul, half_pos, LT.lt.le, Real.norm_of_nonneg, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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 ε
suffices : ‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε)
⊢ ‖L₁ - L₂‖ ≤ 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
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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₂)‖ = ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂ - (f (x + r / 2) - f x - (x + r / 2 - x) • L₁)‖

Tactic:
simp [smul_sub]

Premises used: smul_sub
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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₁)‖ ≤
    ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ + ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖

Tactic:
norm_sub_le _ _

Premises used: norm_sub_le
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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
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

Tactic:
apply add_le_add

Premises used: add_le_add
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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)
h₄ : x + r / 2 ∈ Icc x (x + r / 2)
⊢ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ ≤ ε * r

Tactic:
apply le_of_mem_A h₂

Premises used: RightDerivMeasurableAux.le_of_mem_A
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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 ε
⊢ x ∈ Icc x (x + r / 2)

Tactic:
simp [(half_pos hr).le]

Premises used: half_pos, LT.lt.le
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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 ε
⊢ x + r / 2 ∈ Icc x (x + r / 2)

Tactic:
simp [(half_pos hr).le]

Premises used: half_pos, LT.lt.le
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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)
h₄ : x + r / 2 ∈ Icc x (x + r / 2)
⊢ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖ ≤ ε * r

Tactic:
apply le_of_mem_A h₁

Premises used: RightDerivMeasurableAux.le_of_mem_A
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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 = r / 2 * (4 * ε)

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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₃ : ε * r + ε * r = r / 2 * (4 * ε)
⊢ ‖(r / 2) • (L₁ - L₂)‖ ≤ 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

Premises used: HMul.hMul, norm_sub_le, HSub.hSub, HDiv.hDiv, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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
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
⊢ x ∈ D f K

Tactic:
rw [D, mem_iInter]

Premises used: Set.mem_iInter, RightDerivMeasurableAux.D
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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 : ℕ
⊢ 0 < 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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 : ℕ
⊢ 0 < (1 / 2) ^ e

Tactic:
have : (0 : ℝ) < (1 / 2) ^ e := pow_pos (by norm_num) _
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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
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
⊢ 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⟩

Premises used: And.left, RightDerivMeasurableAux.mem_A_of_differentiable
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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)
⊢ 1 / 2 < 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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)
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
⊢ 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)

Premises used: exists_pow_lt_of_lt_one, HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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
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)
⊢ Membership.mem (γ := Set ℝ)
    (⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)) x

Tactic:
simp only [mem_iUnion, mem_iInter, B, mem_inter_iff]

Premises used: Set.mem_inter_iff, Set.mem_iUnion, Set.mem_iInter, RightDerivMeasurableAux.B
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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)

Tactic:
⟨n, fun p hp q hq => ⟨derivWithin f (Ici x) x, hx.2, ⟨?_, ?_⟩⟩⟩

Premises used: Set.Ici, derivWithin, And.right, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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)
refine_2 : ∀ (p : ℕ) (hp : p ≥ n) (q : ℕ) (hq : q ≥ n), x ∈ A f (derivWithin f (Ici x) x) ((1 / 2) ^ q) ((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)

Tactic:
refine ⟨n, fun p hp q hq => ⟨derivWithin f (Ici x) x, hx.2, ⟨?_, ?_⟩⟩⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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
⊢ 0 < 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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
refine_1 : (1 / 2) ^ p ≤ (1 / 2) ^ n
⊢ x ∈ A f (derivWithin f (Ici x) x) ((1 / 2) ^ p) ((1 / 2) ^ e)

Tactic:
refine hR _ ⟨pow_pos (by norm_num) _, lt_of_le_of_lt ?_ hn⟩

Premises used: lt_of_le_of_lt, pow_pos, And.intro
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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
⊢ 0 ≤ 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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
⊢ 1 / 2 ≤ 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
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
⊢ n ≤ p

Tactic:
assumption