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
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
hs : s.Countable
B : Basis (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) ℝ E
I1 :
  ∀ᵐ (x : E) ∂μ,
    ∀ v ∈ s,
      lineDeriv ℝ f x
          (∑ i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1),
            HSMul.hSMul (α := ℝ) (β := E)
              ((((B.repr : (a : E) → (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) v :
                      (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) :
                    (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → ℝ)
                  i :
                ℝ)
              ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i : E)) =
        ∑ i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1),
          HSMul.hSMul (α := ℝ)
            ((((B.repr : (a : E) → (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) v :
                    (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) :
                  (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → ℝ)
                i :
              ℝ)
            (lineDeriv ℝ f x ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i))
I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v
x : E
hx :
  ∀ v ∈ s,
    lineDeriv ℝ f x
        (∑ i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1),
          HSMul.hSMul (α := ℝ) (β := E)
            ((((B.repr : (a : E) → (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) v :
                    (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) :
                  (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → ℝ)
                i :
              ℝ)
            ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i : E)) =
      ∑ i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1),
        HSMul.hSMul (α := ℝ)
          ((((B.repr : (a : E) → (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) v :
                  (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) →₀ ℝ) :
                (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → ℝ)
              i :
            ℝ)
          (lineDeriv ℝ f x ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i))
h'x : ∀ v ∈ s, LineDifferentiableAt ℝ f x v
L : StrongDual ℝ E :=
  ((LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] ℝ) ≃ₗ[ℝ] E →L[ℝ] ℝ) : (a : E →ₗ[ℝ] ℝ) → E →L[ℝ] ℝ)
    ((B.constr ℝ : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1) → ℝ) → E →ₗ[ℝ] ℝ)
        fun (i : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) ↦
        lineDeriv ℝ f x ((B : (a : (↑(Basis.ofVectorSpaceIndex ℝ E) : Type u_1)) → E) i) :
      E →ₗ[ℝ] ℝ)
v : E
hv : v ∈ s
⊢ HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) x v
have J : (L : (a : E) → ℝ) v = lineDeriv ℝ f x v
Tactic: have J : L v = lineDeriv ℝ f x v := by convert! (hx v hv).symm <;> simp [L, B.sum_repr v]
-- 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
⊢ HasFDerivAt f L x
have rw : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝 0, ‖HSub.hSub (β := F) (f (x + x_1) - f x) ((L : (a : E) → F) x_1 : F)‖ ≤ c * ‖x_1‖
Tactic: rw [hasFDerivAt_iff_isLittleO_nhds_zero, isLittleO_iff]
-- 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 < ε
⊢ ∀ᶠ (x_1 : E) in 𝓝 0, ‖HSub.hSub (β := F) (f (x + x_1) - f x) ((L : (a : E) → F) x_1 : F)‖ ≤ ε * ‖x_1‖
have obtain : ∀ (δ : ℝ) (δpos : 0 < δ) (hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε),
  ∀ᶠ (x_1 : E) in 𝓝 0, ‖HSub.hSub (β := F) (f (x + x_1) - f x) ((L : (a : E) → F) x_1 : F)‖ ≤ ε * ‖x_1‖
Tactic: obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ (C + ‖L‖ + 1) * δ = ε :=
    ⟨ε / (C + ‖L‖ + 1), by positivity, mul_div_cancel₀ ε (by positivity)⟩
-- 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) * δ = ε
⊢ Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ s, ball y δ)
have apply : ∀ (z : E) (hz : z ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s),
  Membership.mem (γ := Set E) (⋃ y ∈ s, ball y δ) z
Tactic: apply hs.trans (fun z hz ↦ ?_)
-- 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) * δ = ε
z : E
hz : z ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Membership.mem (γ := Set E) (⋃ y ∈ s, ball y δ) z
have obtain : ∀ (y : E) (ys : y ∈ s) (hy : dist z y < δ), Membership.mem (γ := Set E) (⋃ y ∈ s, ball y δ) z
Tactic: obtain ⟨y, ys, hy⟩ : ∃ y ∈ s, dist z y < δ := Metric.mem_closure_iff.1 hz δ δpos
-- 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 ⊆ s, q.Finite ∧ Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
have this : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ s, ball y δ)
Tactic: have : sphere 0 1 ⊆ ⋃ y ∈ s, ball y δ := by
      apply hs.trans (fun z hz ↦ ?_)
      obtain ⟨y, ys, hy⟩ : ∃ y ∈ s, dist z y < δ := Metric.mem_closure_iff.1 hz δ δpos
      exact mem_biUnion ys hy
-- 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) * δ = ε
⊢ ∀ᶠ (x_1 : E) in 𝓝 0, ‖HSub.hSub (β := F) (f (x + x_1) - f x) ((L : (a : E) → F) x_1 : F)‖ ≤ ε * ‖x_1‖
have obtain : ∀ (q : Set E) (hqs : q ⊆ s) (q_fin : q.Finite) (hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)),
  ∀ᶠ (x_1 : E) in 𝓝 0, ‖HSub.hSub (β := F) (f (x + x_1) - f x) ((L : (a : E) → F) x_1 : F)‖ ≤ ε * ‖x_1‖
Tactic: obtain ⟨q, hqs, q_fin, hq⟩ : ∃ q, q ⊆ s ∧ q.Finite ∧ sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ := by
    have : sphere 0 1 ⊆ ⋃ y ∈ s, ball y δ := by
      apply hs.trans (fun z hz ↦ ?_)
      obtain ⟨y, ys, hy⟩ : ∃ y ∈ s, dist z y < δ := Metric.mem_closure_iff.1 hz δ δpos
      exact mem_biUnion ys hy
    exact (isCompact_sphere 0 1).elim_finite_subcover_image (fun y _hy ↦ isOpen_ball) this
-- 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 δ)
⊢ ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
have apply : ∀ (v : E) (hv : v ∈ q),
  ∀ᶠ (x_1 : ℝ) in 𝓝 0, ‖f (x + x_1 • v) - f x - HSMul.hSMul (β := F) x_1 ((L : (a : E) → F) v : F)‖ ≤ δ * ‖x_1‖
Tactic: apply (Finite.eventually_all q_fin).2 (fun v hv ↦ ?_)
-- 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 δ)
v : E
hv : v ∈ q
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝 0, ‖f (x + x_1 • v) - f x - HSMul.hSMul (β := F) x_1 ((L : (a : E) → F) v : F)‖ ≤ δ * ‖x_1‖
have apply : IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝 0)
  (fun (x_1 : ℝ) ↦ f (x + x_1 • v) - f x - HSMul.hSMul (β := F) x_1 ((L : (a : E) → F) v : F)) fun (x : ℝ) ↦ x
Tactic: apply Asymptotics.IsLittleO.def ?_ δpos
-- 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 δ)
⊢ ∀ᶠ (x_1 : E) in 𝓝 0, ‖HSub.hSub (β := F) (f (x + x_1) - f x) ((L : (a : E) → F) x_1 : F)‖ ≤ ε * ‖x_1‖
have I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
Tactic: have I : ∀ᶠ t in 𝓝 (0 : ℝ), ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖ := by
    apply (Finite.eventually_all q_fin).2 (fun v hv ↦ ?_)
    apply Asymptotics.IsLittleO.def ?_ δpos
    exact hasLineDerivAt_iff_isLittleO_nhds_zero.1 (hL v (hqs hv))
-- 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 : ℝ),
    0 < r ∧
      ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
have rcases : ∀ (r : ℝ) (r_pos : r > 0)
  (hr :
    Subset (α := Set ℝ) (ball 0 r)
      {x_1 : ℝ |
        (fun (t : ℝ) ↦ ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖)
          x_1}),
  ∃ (r : ℝ),
    0 < r ∧
      ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
Tactic: rcases Metric.mem_nhds_iff.1 I with ⟨r, r_pos, hr⟩
-- 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‖
⊢ ∀ᶠ (x_1 : E) in 𝓝 0, ‖HSub.hSub (β := F) (f (x + x_1) - f x) ((L : (a : E) → F) x_1 : F)‖ ≤ ε * ‖x_1‖
have obtain : ∀ (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‖),
  ∀ᶠ (x_1 : E) in 𝓝 0, ‖HSub.hSub (β := F) (f (x + x_1) - f x) ((L : (a : E) → F) x_1 : F)‖ ≤ ε * ‖x_1‖
Tactic: obtain ⟨r, r_pos, hr⟩ : ∃ (r : ℝ), 0 < r ∧ ∀ (t : ℝ), ‖t‖ < r →
      ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖ := by
    rcases Metric.mem_nhds_iff.1 I with ⟨r, r_pos, hr⟩
    exact ⟨r, r_pos, fun t ht v hv ↦ hr (mem_ball_zero_iff.2 ht) v hv⟩
-- 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‖
⊢ ∀ᶠ (x_1 : E) in 𝓝 0, ‖HSub.hSub (β := F) (f (x + x_1) - f x) ((L : (a : E) → F) x_1 : F)‖ ≤ ε * ‖x_1‖
have apply : ∀ (v : E) (hv : Membership.mem (γ := Set E) (ball 0 r) 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
Tactic: apply Metric.mem_nhds_iff.2 ⟨r, r_pos, fun v hv ↦ ?_⟩
-- 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
⊢ 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 inl : ∀ (hv : Membership.mem (γ := Set E) (ball 0 r) 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} 0
Tactic: rcases eq_or_ne v 0 with rfl | v_ne
Cleared hypotheses: v, hv
-- 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
inl :
  ∀ (hv : Membership.mem (γ := Set E) (ball 0 r) 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}
      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 : ∀ (v_ne : v ≠ 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
Tactic: rcases eq_or_ne v 0 with rfl | v_ne
-- 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) (ρ : ℝ), Membership.mem (γ := Set E) (sphere 0 1) w ∧ v = ρ • w ∧ ρ = ‖v‖
have refine : v = ‖v‖ • ‖v‖⁻¹ • v
Tactic: refine ⟨‖v‖⁻¹ • v, ‖v‖, by simp [norm_smul, inv_mul_cancel₀ (norm_ne_zero_iff.2 v_ne)], ?_, rfl⟩
-- 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
⊢ 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 : ∀ (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
Tactic: obtain ⟨w, ρ, w_mem, hvw, hρ⟩ : ∃ w ρ, w ∈ sphere 0 1 ∧ v = ρ • w ∧ ρ = ‖v‖ := by
    refine ⟨‖v‖⁻¹ • v, ‖v‖, by simp [norm_smul, inv_mul_cancel₀ (norm_ne_zero_iff.2 v_ne)], ?_, rfl⟩
    simp [smul_smul, mul_inv_cancel₀ (norm_ne_zero_iff.2 v_ne)]
-- 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‖
⊢ ‖ρ‖ = ρ
have rw : ‖‖v‖‖ = ‖v‖
Tactic: rw [hρ, norm_norm]
-- 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‖
rw : ‖‖v‖‖ = ‖v‖
⊢ ‖ρ‖ = ρ
have rw₁ : ‖v‖ = ‖v‖
Tactic: rw [hρ, norm_norm]