awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
⊢ ∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ε
have refine : ∀ (r : ℝ) (hr : r ∈ Ioo 0 R), x ∈ A f (fderiv 𝕜 f x) r ε
Tactic: refine ⟨R, R_pos, fun r hr => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
⊢ x ∈ A f (fderiv 𝕜 f x) r ε
have this : r ∈ Ioc (r / 2) r
Tactic: have : r ∈ Ioc (r / 2) r := right_mem_Ioc.2 <| half_lt_self hr.1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
⊢ x ∈ A f (fderiv 𝕜 f x) r ε
have refine : ∀ (y : E) (hy : y ∈ ball x r) (z : E) (hz : z ∈ ball x r),
  ‖HSub.hSub (β := F) (f z - f y) ((fderiv 𝕜 f x : (a : E) → F) (z - y) : F)‖ < ε * r
Tactic: refine ⟨r, this, fun y hy z hz => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : y ∈ ball x r
z : E
hz : z ∈ ball x r
⊢ ‖HSub.hSub (β := F) (f z - f y) ((fderiv 𝕜 f x : (a : E) → F) (z - y) : F)‖ =
    ‖HSub.hSub (β := F) (f z - f x) ((fderiv 𝕜 f x : (a : E) → F) (z - x) : F) -
        HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖
have simp : ‖f z - f y - HSub.hSub (α := F) (β := F) ((fderiv 𝕜 f x : (a : E) → F) z : F) ((fderiv 𝕜 f x : (a : E) → F) y : F)‖ =
  ‖f z - f x - HSub.hSub (α := F) (β := F) ((fderiv 𝕜 f x : (a : E) → F) z : F) ((fderiv 𝕜 f x : (a : E) → F) x : F) -
      (f y - f x -
        HSub.hSub (α := F) (β := F) ((fderiv 𝕜 f x : (a : E) → F) y : F) ((fderiv 𝕜 f x : (a : E) → F) x : F))‖
Tactic: simp only [map_sub]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : y ∈ ball x r
z : E
hz : z ∈ ball x r
⊢ δ * ‖z - x‖ + δ * ‖y - x‖ ≤ δ * r + δ * r
have rw : ∀ (hy : ‖y - x‖ < r) (z : E) (hz : ‖z - x‖ < r), δ * ‖z - x‖ + δ * ‖y - x‖ ≤ δ * r + δ * r
Tactic: rw [mem_ball_iff_norm] at hz hy
Cleared hypotheses: hy, z, hz
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : ‖y - x‖ < r
z : E
hz : ‖z - x‖ < r
⊢ δ * ‖z - x‖ + δ * ‖y - x‖ ≤ δ * r + δ * r
have h₁ : 0 ≤ δ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : y ∈ ball x r
z : E
hz : z ∈ ball x r
⊢ ε / 2 * r < ε * r
have ha : 0 < r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : y ∈ ball x r
z : E
hz : z ∈ ball x r
ha : 0 < r
⊢ ε / 2 * r < ε * r
have hbc : ε / 2 < ε
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : y ∈ ball x r
z : E
hz : z ∈ ball x r
⊢ ‖HSub.hSub (β := F) (f z - f y) ((fderiv 𝕜 f x : (a : E) → F) (z - y) : F)‖ < ε * r
have z₁ : ‖HSub.hSub (β := F) (f z - f y) ((fderiv 𝕜 f x : (a : E) → F) (z - y) : F)‖ =
  ‖HSub.hSub (β := F) (f z - f x) ((fderiv 𝕜 f x : (a : E) → F) (z - x) : F) -
      HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖
Tactic: calc
    ‖f z - f y - (fderiv 𝕜 f x) (z - y)‖ =
        ‖f z - f x - (fderiv 𝕜 f x) (z - x) - (f y - f x - (fderiv 𝕜 f x) (y - x))‖ := by
      simp only [map_sub]; abel_nf
    _ ≤ ‖f z - f x - (fderiv 𝕜 f x) (z - x)‖ + ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ :=
      norm_sub_le _ _
    _ ≤ δ * ‖z - x‖ + δ * ‖y - x‖ :=
      add_le_add (hR _ (ball_subset_ball hr.2.le hz)) (hR _ (ball_subset_ball hr.2.le hy))
    _ ≤ δ * r + δ * r := by rw [mem_ball_iff_norm] at hz hy; gcongr
    _ = (ε / 2) * r := by ring
    _ < ε * r := by gcongr; exacts [hr.1, half_lt_self hε]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : y ∈ ball x r
z : E
hz : z ∈ ball x r
z₁ :
  ‖HSub.hSub (β := F) (f z - f y) ((fderiv 𝕜 f x : (a : E) → F) (z - y) : F)‖ =
    ‖HSub.hSub (β := F) (f z - f x) ((fderiv 𝕜 f x : (a : E) → F) (z - x) : F) -
        HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖
⊢ ‖HSub.hSub (β := F) (f z - f y) ((fderiv 𝕜 f x : (a : E) → F) (z - y) : F)‖ < ε * r
have z₂ : δ * ‖z - x‖ + δ * ‖y - x‖ ≤ δ * r + δ * r
Tactic: calc
    ‖f z - f y - (fderiv 𝕜 f x) (z - y)‖ =
        ‖f z - f x - (fderiv 𝕜 f x) (z - x) - (f y - f x - (fderiv 𝕜 f x) (y - x))‖ := by
      simp only [map_sub]; abel_nf
    _ ≤ ‖f z - f x - (fderiv 𝕜 f x) (z - x)‖ + ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ :=
      norm_sub_le _ _
    _ ≤ δ * ‖z - x‖ + δ * ‖y - x‖ :=
      add_le_add (hR _ (ball_subset_ball hr.2.le hz)) (hR _ (ball_subset_ball hr.2.le hy))
    _ ≤ δ * r + δ * r := by rw [mem_ball_iff_norm] at hz hy; gcongr
    _ = (ε / 2) * r := by ring
    _ < ε * r := by gcongr; exacts [hr.1, half_lt_self hε]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : y ∈ ball x r
z : E
hz : z ∈ ball x r
z₁ :
  ‖HSub.hSub (β := F) (f z - f y) ((fderiv 𝕜 f x : (a : E) → F) (z - y) : F)‖ =
    ‖HSub.hSub (β := F) (f z - f x) ((fderiv 𝕜 f x : (a : E) → F) (z - x) : F) -
        HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖
z₂ : δ * ‖z - x‖ + δ * ‖y - x‖ ≤ δ * r + δ * r
⊢ ‖HSub.hSub (β := F) (f z - f y) ((fderiv 𝕜 f x : (a : E) → F) (z - y) : F)‖ < ε * r
have z₃ : δ * r + δ * r = ε / 2 * r
Tactic: calc
    ‖f z - f y - (fderiv 𝕜 f x) (z - y)‖ =
        ‖f z - f x - (fderiv 𝕜 f x) (z - x) - (f y - f x - (fderiv 𝕜 f x) (y - x))‖ := by
      simp only [map_sub]; abel_nf
    _ ≤ ‖f z - f x - (fderiv 𝕜 f x) (z - x)‖ + ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ :=
      norm_sub_le _ _
    _ ≤ δ * ‖z - x‖ + δ * ‖y - x‖ :=
      add_le_add (hR _ (ball_subset_ball hr.2.le hz)) (hR _ (ball_subset_ball hr.2.le hy))
    _ ≤ δ * r + δ * r := by rw [mem_ball_iff_norm] at hz hy; gcongr
    _ = (ε / 2) * r := by ring
    _ < ε * r := by gcongr; exacts [hr.1, half_lt_self hε]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
ε : ℝ
hε : 0 < ε
x : E
hx : DifferentiableAt 𝕜 f x
δ : ℝ := ε / 2 / 2
R : ℝ
R_pos : R > 0
hR : ∀ y ∈ ball x R, ‖HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖ ≤ δ * ‖y - x‖
r : ℝ
hr : r ∈ Ioo 0 R
this : r ∈ Ioc (r / 2) r
y : E
hy : y ∈ ball x r
z : E
hz : z ∈ ball x r
z₁ :
  ‖HSub.hSub (β := F) (f z - f y) ((fderiv 𝕜 f x : (a : E) → F) (z - y) : F)‖ =
    ‖HSub.hSub (β := F) (f z - f x) ((fderiv 𝕜 f x : (a : E) → F) (z - x) : F) -
        HSub.hSub (β := F) (f y - f x) ((fderiv 𝕜 f x : (a : E) → F) (y - x) : F)‖
z₂ : δ * ‖z - x‖ + δ * ‖y - x‖ ≤ δ * r + δ * r
z₃ : δ * r + δ * r = ε / 2 * r
⊢ ‖HSub.hSub (β := F) (f z - f y) ((fderiv 𝕜 f x : (a : E) → F) (z - y) : F)‖ < ε * r
have z₄ : ε / 2 * r < ε * r
Tactic: calc
    ‖f z - f y - (fderiv 𝕜 f x) (z - y)‖ =
        ‖f z - f x - (fderiv 𝕜 f x) (z - x) - (f y - f x - (fderiv 𝕜 f x) (y - x))‖ := by
      simp only [map_sub]; abel_nf
    _ ≤ ‖f z - f x - (fderiv 𝕜 f x) (z - x)‖ + ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ :=
      norm_sub_le _ _
    _ ≤ δ * ‖z - x‖ + δ * ‖y - x‖ :=
      add_le_add (hR _ (ball_subset_ball hr.2.le hz)) (hR _ (ball_subset_ball hr.2.le hy))
    _ ≤ δ * r + δ * r := by rw [mem_ball_iff_norm] at hz hy; gcongr
    _ = (ε / 2) * r := by ring
    _ < ε * r := by gcongr; exacts [hr.1, half_lt_self hε]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
⊢ ‖L₁ - L₂‖ ≤ 4 * ‖c‖ * ε
have refine : ∀ (x : E), r / 2 / ‖c‖ ≤ ‖x‖ → ‖x‖ < r / 2 → norm.{u_3} (E := F) ((L₁ - L₂ : (a : E) → F) x : F) ≤ 4 * ‖c‖ * ε * ‖x‖
Tactic: refine opNorm_le_of_shell (half_pos hr) (by positivity) hc ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
y : E
ley : r / 2 / ‖c‖ ≤ ‖y‖
ylt : ‖y‖ < r / 2
⊢ norm.{u_3} (E := F) ((L₁ - L₂ : (a : E) → F) y : F) ≤ 4 * ‖c‖ * ε * ‖y‖
have ley₁ : r ≤ 2 * ‖c‖ * ‖y‖
Tactic: rw [div_div, div_le_iff₀' (by positivity)] at ley
Cleared hypotheses: ley, ylt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
y : E
ley : r ≤ 2 * ‖c‖ * ‖y‖
ylt : ‖y‖ < r / 2
⊢ ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₂ : (a : E) → F) (x + y - x) : F)‖ +
      ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₁ : (a : E) → F) (x + y - x) : F)‖ ≤
    ε * r + ε * r
have h₃ : ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₂ : (a : E) → F) (x + y - x) : F)‖ ≤ ε * r
Tactic: apply add_le_add
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
y : E
ley : r ≤ 2 * ‖c‖ * ‖y‖
ylt : ‖y‖ < r / 2
h₃ : ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₂ : (a : E) → F) (x + y - x) : F)‖ ≤ ε * r
⊢ ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₂ : (a : E) → F) (x + y - x) : F)‖ +
      ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₁ : (a : E) → F) (x + y - x) : F)‖ ≤
    ε * r + ε * r
have h₄ : ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₁ : (a : E) → F) (x + y - x) : F)‖ ≤ ε * r
Tactic: apply add_le_add
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
y : E
ley : r ≤ 2 * ‖c‖ * ‖y‖
ylt : ‖y‖ < r / 2
⊢ ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₂ : (a : E) → F) (x + y - x) : F)‖ ≤ ε * r
have h₃ : x ∈ closedBall x (r / 2)
Tactic: apply le_of_mem_A h₂
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
y : E
ley : r ≤ 2 * ‖c‖ * ‖y‖
ylt : ‖y‖ < r / 2
h₃ : x ∈ closedBall x (r / 2)
⊢ ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₂ : (a : E) → F) (x + y - x) : F)‖ ≤ ε * r
have h₄ : x + y ∈ closedBall x (r / 2)
Tactic: apply le_of_mem_A h₂
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
y : E
ley : r ≤ 2 * ‖c‖ * ‖y‖
ylt : ‖y‖ < r / 2
⊢ ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₁ : (a : E) → F) (x + y - x) : F)‖ ≤ ε * r
have h₃ : x ∈ closedBall x (r / 2)
Tactic: apply le_of_mem_A h₁
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
y : E
ley : r ≤ 2 * ‖c‖ * ‖y‖
ylt : ‖y‖ < r / 2
h₃ : x ∈ closedBall x (r / 2)
⊢ ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₁ : (a : E) → F) (x + y - x) : F)‖ ≤ ε * r
have h₄ : x + y ∈ closedBall x (r / 2)
Tactic: apply le_of_mem_A h₁
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
y : E
ley : r ≤ 2 * ‖c‖ * ‖y‖
ylt : ‖y‖ < r / 2
⊢ 2 * ε * r ≤ 2 * ε * (2 * ‖c‖ * ‖y‖)
have ha : 0 ≤ 2 * ε
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
y : E
ley : r ≤ 2 * ‖c‖ * ‖y‖
ylt : ‖y‖ < r / 2
⊢ norm.{u_3} (E := F) ((L₁ - L₂ : (a : E) → F) y : F) ≤ 4 * ‖c‖ * ε * ‖y‖
have f₁ : norm.{u_3} (E := F) ((L₁ - L₂ : (a : E) → F) y : F) =
  ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₂ : (a : E) → F) (x + y - x) : F) -
      HSub.hSub (β := F) (f (x + y) - f x) ((L₁ : (a : E) → F) (x + y - x) : F)‖
Tactic: calc
    ‖(L₁ - L₂) y‖ = ‖f (x + y) - f x - L₂ (x + y - x) - (f (x + y) - f x - L₁ (x + y - x))‖ := by
      simp
    _ ≤ ‖f (x + y) - f x - L₂ (x + y - x)‖ + ‖f (x + y) - f x - L₁ (x + y - x)‖ := norm_sub_le _ _
    _ ≤ ε * r + ε * r := by
      apply add_le_add
      · apply le_of_mem_A h₂
        · simp only [le_of_lt (half_pos hr), mem_closedBall, dist_self]
        · simp only [dist_eq_norm, add_sub_cancel_left, mem_closedBall, ylt.le]
      · apply le_of_mem_A h₁
        · simp only [le_of_lt (half_pos hr), mem_closedBall, dist_self]
        · simp only [dist_eq_norm, add_sub_cancel_left, mem_closedBall, ylt.le]
    _ = 2 * ε * r := by ring
    _ ≤ 2 * ε * (2 * ‖c‖ * ‖y‖) := by gcongr
    _ = 4 * ‖c‖ * ε * ‖y‖ := by ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
y : E
ley : r ≤ 2 * ‖c‖ * ‖y‖
ylt : ‖y‖ < r / 2
f₁ :
  norm.{u_3} (E := F) ((L₁ - L₂ : (a : E) → F) y : F) =
    ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₂ : (a : E) → F) (x + y - x) : F) -
        HSub.hSub (β := F) (f (x + y) - f x) ((L₁ : (a : E) → F) (x + y - x) : F)‖
⊢ norm.{u_3} (E := F) ((L₁ - L₂ : (a : E) → F) y : F) ≤ 4 * ‖c‖ * ε * ‖y‖
have f₂ : ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₂ : (a : E) → F) (x + y - x) : F)‖ +
    ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₁ : (a : E) → F) (x + y - x) : F)‖ ≤
  ε * r + ε * r
Tactic: calc
    ‖(L₁ - L₂) y‖ = ‖f (x + y) - f x - L₂ (x + y - x) - (f (x + y) - f x - L₁ (x + y - x))‖ := by
      simp
    _ ≤ ‖f (x + y) - f x - L₂ (x + y - x)‖ + ‖f (x + y) - f x - L₁ (x + y - x)‖ := norm_sub_le _ _
    _ ≤ ε * r + ε * r := by
      apply add_le_add
      · apply le_of_mem_A h₂
        · simp only [le_of_lt (half_pos hr), mem_closedBall, dist_self]
        · simp only [dist_eq_norm, add_sub_cancel_left, mem_closedBall, ylt.le]
      · apply le_of_mem_A h₁
        · simp only [le_of_lt (half_pos hr), mem_closedBall, dist_self]
        · simp only [dist_eq_norm, add_sub_cancel_left, mem_closedBall, ylt.le]
    _ = 2 * ε * r := by ring
    _ ≤ 2 * ε * (2 * ‖c‖ * ‖y‖) := by gcongr
    _ = 4 * ‖c‖ * ε * ‖y‖ := by ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
y : E
ley : r ≤ 2 * ‖c‖ * ‖y‖
ylt : ‖y‖ < r / 2
f₁ :
  norm.{u_3} (E := F) ((L₁ - L₂ : (a : E) → F) y : F) =
    ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₂ : (a : E) → F) (x + y - x) : F) -
        HSub.hSub (β := F) (f (x + y) - f x) ((L₁ : (a : E) → F) (x + y - x) : F)‖
f₂ :
  ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₂ : (a : E) → F) (x + y - x) : F)‖ +
      ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₁ : (a : E) → F) (x + y - x) : F)‖ ≤
    ε * r + ε * r
⊢ norm.{u_3} (E := F) ((L₁ - L₂ : (a : E) → F) y : F) ≤ 4 * ‖c‖ * ε * ‖y‖
have f₃ : ε * r + ε * r = 2 * ε * r
Tactic: calc
    ‖(L₁ - L₂) y‖ = ‖f (x + y) - f x - L₂ (x + y - x) - (f (x + y) - f x - L₁ (x + y - x))‖ := by
      simp
    _ ≤ ‖f (x + y) - f x - L₂ (x + y - x)‖ + ‖f (x + y) - f x - L₁ (x + y - x)‖ := norm_sub_le _ _
    _ ≤ ε * r + ε * r := by
      apply add_le_add
      · apply le_of_mem_A h₂
        · simp only [le_of_lt (half_pos hr), mem_closedBall, dist_self]
        · simp only [dist_eq_norm, add_sub_cancel_left, mem_closedBall, ylt.le]
      · apply le_of_mem_A h₁
        · simp only [le_of_lt (half_pos hr), mem_closedBall, dist_self]
        · simp only [dist_eq_norm, add_sub_cancel_left, mem_closedBall, ylt.le]
    _ = 2 * ε * r := by ring
    _ ≤ 2 * ε * (2 * ‖c‖ * ‖y‖) := by gcongr
    _ = 4 * ‖c‖ * ε * ‖y‖ := by ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
y : E
ley : r ≤ 2 * ‖c‖ * ‖y‖
ylt : ‖y‖ < r / 2
f₁ :
  norm.{u_3} (E := F) ((L₁ - L₂ : (a : E) → F) y : F) =
    ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₂ : (a : E) → F) (x + y - x) : F) -
        HSub.hSub (β := F) (f (x + y) - f x) ((L₁ : (a : E) → F) (x + y - x) : F)‖
f₂ :
  ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₂ : (a : E) → F) (x + y - x) : F)‖ +
      ‖HSub.hSub (β := F) (f (x + y) - f x) ((L₁ : (a : E) → F) (x + y - x) : F)‖ ≤
    ε * r + ε * r
f₃ : ε * r + ε * r = 2 * ε * r
⊢ norm.{u_3} (E := F) ((L₁ - L₂ : (a : E) → F) y : F) ≤ 4 * ‖c‖ * ε * ‖y‖
have f₄ : 2 * ε * r ≤ 2 * ε * (2 * ‖c‖ * ‖y‖)
Tactic: calc
    ‖(L₁ - L₂) y‖ = ‖f (x + y) - f x - L₂ (x + y - x) - (f (x + y) - f x - L₁ (x + y - x))‖ := by
      simp
    _ ≤ ‖f (x + y) - f x - L₂ (x + y - x)‖ + ‖f (x + y) - f x - L₁ (x + y - x)‖ := norm_sub_le _ _
    _ ≤ ε * r + ε * r := by
      apply add_le_add
      · apply le_of_mem_A h₂
        · simp only [le_of_lt (half_pos hr), mem_closedBall, dist_self]
        · simp only [dist_eq_norm, add_sub_cancel_left, mem_closedBall, ylt.le]
      · apply le_of_mem_A h₁
        · simp only [le_of_lt (half_pos hr), mem_closedBall, dist_self]
        · simp only [dist_eq_norm, add_sub_cancel_left, mem_closedBall, ylt.le]
    _ = 2 * ε * r := by ring
    _ ≤ 2 * ε * (2 * ‖c‖ * ‖y‖) := by gcongr
    _ = 4 * ‖c‖ * ε * ‖y‖ := by ring