awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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‖ < δ
rw : ε * ρ = ε * ‖v‖
⊢ ((↑C : ℝ) + ‖L‖ + 1) * δ * ρ = ε * ‖v‖
have rw₁ : ε * ‖v‖ = ε * ‖v‖
Tactic: rw [hδ, 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 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ 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 calc : ‖HSub.hSub (β := F) (f (x + v) - f x) ((L : (a : E) → F) v : F)‖ =
  ‖f (x + ρ • w) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)‖
Tactic: calc ‖f (x + v) - f x - L v‖
      = ‖f (x + ρ • w) - f x - ρ • L w‖ := by simp [hvw]
    _ = ‖(f (x + ρ • w) - f (x + ρ • y)) + (ρ • L y - ρ • L w)
          + (f (x + ρ • y) - f x - ρ • L y)‖ := by congr; abel
    _ ≤ ‖f (x + ρ • w) - f (x + ρ • y)‖ + ‖ρ • L y - ρ • L w‖
          + ‖f (x + ρ • y) - f x - ρ • L y‖ := norm_add₃_le
    _ ≤ C * ‖(x + ρ • w) - (x + ρ • y)‖ + ρ * (‖L‖ * ‖y - w‖) + δ * ρ := by
      gcongr
      · exact hf.norm_sub_le _ _
      · rw [← smul_sub, norm_smul, norm_rho]
        gcongr
        exact L.lipschitz.norm_sub_le _ _
      · conv_rhs => rw [← norm_rho]
        apply hr _ _ _ yq
        simpa [norm_rho, hρ] using hv
    _ ≤ C * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ := by
      simp only [add_sub_add_left_eq_sub, ← smul_sub, norm_smul, norm_rho]; gcongr
    _ = ((C + ‖L‖ + 1) * δ) * ρ := by ring
    _ = ε * ‖v‖ := by rw [hδ, 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 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
calc :
  ‖HSub.hSub (β := F) (f (x + v) - f x) ((L : (a : E) → F) v : F)‖ =
    ‖f (x + ρ • w) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)‖
⊢ 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 calc₁ : ‖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: calc ‖f (x + v) - f x - L v‖
      = ‖f (x + ρ • w) - f x - ρ • L w‖ := by simp [hvw]
    _ = ‖(f (x + ρ • w) - f (x + ρ • y)) + (ρ • L y - ρ • L w)
          + (f (x + ρ • y) - f x - ρ • L y)‖ := by congr; abel
    _ ≤ ‖f (x + ρ • w) - f (x + ρ • y)‖ + ‖ρ • L y - ρ • L w‖
          + ‖f (x + ρ • y) - f x - ρ • L y‖ := norm_add₃_le
    _ ≤ C * ‖(x + ρ • w) - (x + ρ • y)‖ + ρ * (‖L‖ * ‖y - w‖) + δ * ρ := by
      gcongr
      · exact hf.norm_sub_le _ _
      · rw [← smul_sub, norm_smul, norm_rho]
        gcongr
        exact L.lipschitz.norm_sub_le _ _
      · conv_rhs => rw [← norm_rho]
        apply hr _ _ _ yq
        simpa [norm_rho, hρ] using hv
    _ ≤ C * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ := by
      simp only [add_sub_add_left_eq_sub, ← smul_sub, norm_smul, norm_rho]; gcongr
    _ = ((C + ‖L‖ + 1) * δ) * ρ := by ring
    _ = ε * ‖v‖ := by rw [hδ, 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 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
calc :
  ‖HSub.hSub (β := F) (f (x + v) - f x) ((L : (a : E) → F) v : F)‖ =
    ‖f (x + ρ • w) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)‖
calc₁ :
  ‖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))‖
⊢ 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 calc₂ : ‖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‖) + δ * ρ
Tactic: calc ‖f (x + v) - f x - L v‖
      = ‖f (x + ρ • w) - f x - ρ • L w‖ := by simp [hvw]
    _ = ‖(f (x + ρ • w) - f (x + ρ • y)) + (ρ • L y - ρ • L w)
          + (f (x + ρ • y) - f x - ρ • L y)‖ := by congr; abel
    _ ≤ ‖f (x + ρ • w) - f (x + ρ • y)‖ + ‖ρ • L y - ρ • L w‖
          + ‖f (x + ρ • y) - f x - ρ • L y‖ := norm_add₃_le
    _ ≤ C * ‖(x + ρ • w) - (x + ρ • y)‖ + ρ * (‖L‖ * ‖y - w‖) + δ * ρ := by
      gcongr
      · exact hf.norm_sub_le _ _
      · rw [← smul_sub, norm_smul, norm_rho]
        gcongr
        exact L.lipschitz.norm_sub_le _ _
      · conv_rhs => rw [← norm_rho]
        apply hr _ _ _ yq
        simpa [norm_rho, hρ] using hv
    _ ≤ C * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ := by
      simp only [add_sub_add_left_eq_sub, ← smul_sub, norm_smul, norm_rho]; gcongr
    _ = ((C + ‖L‖ + 1) * δ) * ρ := by ring
    _ = ε * ‖v‖ := by rw [hδ, 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 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
calc :
  ‖HSub.hSub (β := F) (f (x + v) - f x) ((L : (a : E) → F) v : F)‖ =
    ‖f (x + ρ • w) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)‖
calc₁ :
  ‖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))‖
calc₂ :
  ‖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‖) + δ * ρ
⊢ 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 calc₃ : (↑C : ℝ) * ‖x + ρ • w - (x + ρ • y)‖ + ρ * (‖L‖ * ‖y - w‖) + δ * ρ ≤ (↑C : ℝ) * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ
Tactic: calc ‖f (x + v) - f x - L v‖
      = ‖f (x + ρ • w) - f x - ρ • L w‖ := by simp [hvw]
    _ = ‖(f (x + ρ • w) - f (x + ρ • y)) + (ρ • L y - ρ • L w)
          + (f (x + ρ • y) - f x - ρ • L y)‖ := by congr; abel
    _ ≤ ‖f (x + ρ • w) - f (x + ρ • y)‖ + ‖ρ • L y - ρ • L w‖
          + ‖f (x + ρ • y) - f x - ρ • L y‖ := norm_add₃_le
    _ ≤ C * ‖(x + ρ • w) - (x + ρ • y)‖ + ρ * (‖L‖ * ‖y - w‖) + δ * ρ := by
      gcongr
      · exact hf.norm_sub_le _ _
      · rw [← smul_sub, norm_smul, norm_rho]
        gcongr
        exact L.lipschitz.norm_sub_le _ _
      · conv_rhs => rw [← norm_rho]
        apply hr _ _ _ yq
        simpa [norm_rho, hρ] using hv
    _ ≤ C * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ := by
      simp only [add_sub_add_left_eq_sub, ← smul_sub, norm_smul, norm_rho]; gcongr
    _ = ((C + ‖L‖ + 1) * δ) * ρ := by ring
    _ = ε * ‖v‖ := by rw [hδ, 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 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
calc :
  ‖HSub.hSub (β := F) (f (x + v) - f x) ((L : (a : E) → F) v : F)‖ =
    ‖f (x + ρ • w) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)‖
calc₁ :
  ‖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))‖
calc₂ :
  ‖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‖) + δ * ρ
calc₃ : (↑C : ℝ) * ‖x + ρ • w - (x + ρ • y)‖ + ρ * (‖L‖ * ‖y - w‖) + δ * ρ ≤ (↑C : ℝ) * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ
⊢ 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 calc₄ : (↑C : ℝ) * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ = ((↑C : ℝ) + ‖L‖ + 1) * δ * ρ
Tactic: calc ‖f (x + v) - f x - L v‖
      = ‖f (x + ρ • w) - f x - ρ • L w‖ := by simp [hvw]
    _ = ‖(f (x + ρ • w) - f (x + ρ • y)) + (ρ • L y - ρ • L w)
          + (f (x + ρ • y) - f x - ρ • L y)‖ := by congr; abel
    _ ≤ ‖f (x + ρ • w) - f (x + ρ • y)‖ + ‖ρ • L y - ρ • L w‖
          + ‖f (x + ρ • y) - f x - ρ • L y‖ := norm_add₃_le
    _ ≤ C * ‖(x + ρ • w) - (x + ρ • y)‖ + ρ * (‖L‖ * ‖y - w‖) + δ * ρ := by
      gcongr
      · exact hf.norm_sub_le _ _
      · rw [← smul_sub, norm_smul, norm_rho]
        gcongr
        exact L.lipschitz.norm_sub_le _ _
      · conv_rhs => rw [← norm_rho]
        apply hr _ _ _ yq
        simpa [norm_rho, hρ] using hv
    _ ≤ C * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ := by
      simp only [add_sub_add_left_eq_sub, ← smul_sub, norm_smul, norm_rho]; gcongr
    _ = ((C + ‖L‖ + 1) * δ) * ρ := by ring
    _ = ε * ‖v‖ := by rw [hδ, 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 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
calc :
  ‖HSub.hSub (β := F) (f (x + v) - f x) ((L : (a : E) → F) v : F)‖ =
    ‖f (x + ρ • w) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)‖
calc₁ :
  ‖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))‖
calc₂ :
  ‖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‖) + δ * ρ
calc₃ : (↑C : ℝ) * ‖x + ρ • w - (x + ρ • y)‖ + ρ * (‖L‖ * ‖y - w‖) + δ * ρ ≤ (↑C : ℝ) * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ
calc₄ : (↑C : ℝ) * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ = ((↑C : ℝ) + ‖L‖ + 1) * δ * ρ
⊢ 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 calc₅ : ((↑C : ℝ) + ‖L‖ + 1) * δ * ρ = ε * ‖v‖
Tactic: calc ‖f (x + v) - f x - L v‖
      = ‖f (x + ρ • w) - f x - ρ • L w‖ := by simp [hvw]
    _ = ‖(f (x + ρ • w) - f (x + ρ • y)) + (ρ • L y - ρ • L w)
          + (f (x + ρ • y) - f x - ρ • L y)‖ := by congr; abel
    _ ≤ ‖f (x + ρ • w) - f (x + ρ • y)‖ + ‖ρ • L y - ρ • L w‖
          + ‖f (x + ρ • y) - f x - ρ • L y‖ := norm_add₃_le
    _ ≤ C * ‖(x + ρ • w) - (x + ρ • y)‖ + ρ * (‖L‖ * ‖y - w‖) + δ * ρ := by
      gcongr
      · exact hf.norm_sub_le _ _
      · rw [← smul_sub, norm_smul, norm_rho]
        gcongr
        exact L.lipschitz.norm_sub_le _ _
      · conv_rhs => rw [← norm_rho]
        apply hr _ _ _ yq
        simpa [norm_rho, hρ] using hv
    _ ≤ C * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ := by
      simp only [add_sub_add_left_eq_sub, ← smul_sub, norm_smul, norm_rho]; gcongr
    _ = ((C + ‖L‖ + 1) * δ) * ρ := by ring
    _ = ε * ‖v‖ := by rw [hδ, hρ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
⊢ ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x
have obtain : ∀ (s : Set E) (s_count : s.Countable) (s_dense : Dense s), ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x
Tactic: obtain ⟨s, s_count, s_dense⟩ : ∃ (s : Set E), s.Countable ∧ Dense s :=
    TopologicalSpace.exists_countable_dense E
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
s : Set E
s_count : s.Countable
s_dense : Dense s
⊢ sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
have rw : Subset.{u_1} (α := Set E) (sphere 0 1) univ
Tactic: rw [s_dense.closure_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
s : Set E
s_count : s.Countable
s_dense : Dense s
⊢ ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x
have hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
Tactic: have hs : sphere 0 1 ⊆ closure s := by rw [s_dense.closure_eq]; exact subset_univ _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzWith C f
s : Set E
s_count : s.Countable
s_dense : Dense s
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x
have h : ∀ (a : E), (∃ (L : StrongDual ℝ E), ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) a v) → DifferentiableAt ℝ f a
Tactic: filter_upwards [hf.ae_exists_fderiv_of_countable s_count]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
s : Set E
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzOnWith C f s
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
have obtain : ∀ (g : E → ℝ) (g_lip : LipschitzWith C g) (hg : EqOn f g s), ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
Tactic: obtain ⟨g, g_lip, hg⟩ : ∃ (g : E → ℝ), LipschitzWith C g ∧ EqOn f g s := hf.extend_real
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
f : E → ℝ
s : Set E
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
hf : LipschitzOnWith C f s
g : E → ℝ
g_lip : LipschitzWith C g
hg : EqOn f g s
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
have h : ∀ (x : E) (hx : DifferentiableAt ℝ g x) (xs : x ∈ s), DifferentiableWithinAt ℝ f s x
Tactic: filter_upwards [g_lip.ae_differentiableAt_of_real] with x hx xs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
ι : Type u_3
inst_6 : Fintype ι
f : E → ι → ℝ
s : Set E
hf : LipschitzOnWith C f s
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
have A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
Tactic: have A : ∀ i : ι, LipschitzWith 1 (fun x : ι → ℝ ↦ x i) := fun i => LipschitzWith.eval i
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
ι : Type u_3
inst_6 : Fintype ι
f : E → ι → ℝ
s : Set E
hf : LipschitzOnWith C f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
i : ι
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ f x i) s x
have hf₁ : LipschitzOnWith (β := ℝ) (1 * C) (fun (x : E) ↦ f x i) s
Tactic: apply ae_differentiableWithinAt_of_mem_of_real
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Rademacher (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
C : ℝ≥0
μ : Measure E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
ι : Type u_3
inst_6 : Fintype ι
f : E → ι → ℝ
s : Set E
hf : LipschitzOnWith C f s
A : ∀ (i : ι), LipschitzWith (β := ℝ) 1 fun (x : ι → ℝ) ↦ x i
⊢ ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
have this : ∀ (i : ι), ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ f x i) s x
Tactic: have : ∀ i : ι, ∀ᵐ x ∂μ, x ∈ s → DifferentiableWithinAt ℝ (fun x : E ↦ f x i) s x := fun i ↦ by
    apply ae_differentiableWithinAt_of_mem_of_real
    exact LipschitzWith.comp_lipschitzOnWith (A i) hf