awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
⊢ Membership.mem (γ := Set E)
    {x_1 : E | (fun (x_2 : E) ↦ ‖HSub.hSub (β := F) (f (x + x_2) - f x) ((L : (a : E) → F) x_2 : F)‖ ≤ ε * ‖x_2‖) x_1} v
have norm_rho : ‖ρ‖ = ρ
Tactic: have norm_rho : ‖ρ‖ = ρ := by rw [hρ, norm_norm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
⊢ Membership.mem (γ := Set E)
    {x_1 : E | (fun (x_2 : E) ↦ ‖HSub.hSub (β := F) (f (x + x_2) - f x) ((L : (a : E) → F) x_2 : F)‖ ≤ ε * ‖x_2‖) x_1} v
have rho_pos : 0 ≤ ρ
Tactic: have rho_pos : 0 ≤ ρ := by simp [hρ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
⊢ Membership.mem (γ := Set E)
    {x_1 : E | (fun (x_2 : E) ↦ ‖HSub.hSub (β := F) (f (x + x_2) - f x) ((L : (a : E) → F) x_2 : F)‖ ≤ ε * ‖x_2‖) x_1} v
have inr : ∀ (y : E) (yq : y ∈ q) (hy : ‖w - y‖ < δ),
  Membership.mem (γ := Set E)
    {x_1 : E | (fun (x_2 : E) ↦ ‖HSub.hSub (β := F) (f (x + x_2) - f x) ((L : (a : E) → F) x_2 : F)‖ ≤ ε * ‖x_2‖) x_1} v
Tactic: obtain ⟨y, yq, hy⟩ : ∃ y ∈ q, ‖w - y‖ < δ := by simpa [← dist_eq_norm] using hq w_mem
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
⊢ Membership.mem (γ := Set E)
    {x_1 : E | (fun (x_2 : E) ↦ ‖HSub.hSub (β := F) (f (x + x_2) - f x) ((L : (a : E) → F) x_2 : F)‖ ≤ ε * ‖x_2‖) x_1} v
have this : ‖y - w‖ < δ
Tactic: have : ‖y - w‖ < δ := by rwa [norm_sub_rev]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ ‖f (x + ρ • w) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)‖ =
    ‖f (x + ρ • w) - f (x + ρ • y) +
          (HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F) - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)) +
        (f (x + ρ • y) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F))‖
have e_a : f (x + ρ • w) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F) =
  f (x + ρ • w) - f (x + ρ • y) +
      (HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F) - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)) +
    (f (x + ρ • y) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F))
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ ‖f (x + ρ • w) - f (x + ρ • y)‖ +
        ‖HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F) - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)‖ +
      ‖f (x + ρ • y) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F)‖ ≤
    (↑C : ℝ) * ‖x + ρ • w - (x + ρ • y)‖ + ρ * (‖L‖ * ‖y - w‖) + δ * ρ
have h₁ : ‖f (x + ρ • w) - f (x + ρ • y)‖ ≤ (↑C : ℝ) * ‖x + ρ • w - (x + ρ • y)‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
h₁ : ‖f (x + ρ • w) - f (x + ρ • y)‖ ≤ (↑C : ℝ) * ‖x + ρ • w - (x + ρ • y)‖
⊢ ‖f (x + ρ • w) - f (x + ρ • y)‖ +
        ‖HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F) - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)‖ +
      ‖f (x + ρ • y) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F)‖ ≤
    (↑C : ℝ) * ‖x + ρ • w - (x + ρ • y)‖ + ρ * (‖L‖ * ‖y - w‖) + δ * ρ
have h₂ : ‖HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F) - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)‖ ≤
  ρ * (‖L‖ * ‖y - w‖)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
h₁ : ‖f (x + ρ • w) - f (x + ρ • y)‖ ≤ (↑C : ℝ) * ‖x + ρ • w - (x + ρ • y)‖
h₂ :
  ‖HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F) - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)‖ ≤
    ρ * (‖L‖ * ‖y - w‖)
⊢ ‖f (x + ρ • w) - f (x + ρ • y)‖ +
        ‖HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F) - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)‖ +
      ‖f (x + ρ • y) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F)‖ ≤
    (↑C : ℝ) * ‖x + ρ • w - (x + ρ • y)‖ + ρ * (‖L‖ * ‖y - w‖) + δ * ρ
have h₃ : ‖f (x + ρ • y) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F)‖ ≤ δ * ρ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ ‖HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F) - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)‖ ≤
    ρ * (‖L‖ * ‖y - w‖)
have h₁ : ρ * ‖HSub.hSub (α := F) (β := F) ((L : (a : E) → F) y : F) ((L : (a : E) → F) w : F)‖ ≤ ρ * (‖L‖ * ‖y - w‖)
Tactic: rw [← smul_sub, norm_smul, norm_rho]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ ρ * ‖HSub.hSub (α := F) (β := F) ((L : (a : E) → F) y : F) ((L : (a : E) → F) w : F)‖ ≤ ρ * (‖L‖ * ‖y - w‖)
have h₁ : ‖HSub.hSub (α := F) (β := F) ((L : (a : E) → F) y : F) ((L : (a : E) → F) w : F)‖ ≤ ‖L‖ * ‖y - w‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
| δ * ρ
have rw : δ * ‖ρ‖
Tactic: rw [← norm_rho]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ ‖f (x + ρ • y) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F)‖ ≤ δ * ρ
have h₂ : ‖f (x + ρ • y) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F)‖ ≤ δ * ‖ρ‖
Tactic: conv_rhs => rw [← norm_rho]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ ‖f (x + ρ • y) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F)‖ ≤ δ * ‖ρ‖
have apply : ‖ρ‖ < r
Tactic: apply hr _ _ _ yq
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ (↑C : ℝ) * ‖x + ρ • w - (x + ρ • y)‖ + ρ * (‖L‖ * ‖y - w‖) + δ * ρ ≤ (↑C : ℝ) * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ
have simp : (↑C : ℝ) * (ρ * ‖w - y‖) + ρ * (‖L‖ * ‖y - w‖) + δ * ρ ≤ (↑C : ℝ) * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ
Tactic: simp only [add_sub_add_left_eq_sub, ← smul_sub, norm_smul, norm_rho]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ (↑C : ℝ) * (ρ * ‖w - y‖) + ρ * (‖L‖ * ‖y - w‖) + δ * ρ ≤ (↑C : ℝ) * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ
have bc : 0 ≤ (↑C : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
bc : 0 ≤ (↑C : ℝ)
bc₁ bc₂ : 0 ≤ ρ
⊢ (↑C : ℝ) * (ρ * ‖w - y‖) + ρ * (‖L‖ * ‖y - w‖) + δ * ρ ≤ (↑C : ℝ) * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ
have bc₃ : 0 ≤ ‖L‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ ((↑C : ℝ) + ‖L‖ + 1) * δ * ρ = ε * ‖v‖
have rw : ε * ρ = ε * ‖v‖
Tactic: rw [hδ, hρ]