awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Rademacher
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 →ₗ[ℝ] ℝ)
⊢ ∃ (L : StrongDual ℝ E), ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) x v

Tactic:
⟨L, fun v hv ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Analysis.Calculus.Rademacher
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 →ₗ[ℝ] ℝ)
h : ∀ (v : E) (hv : v ∈ s), HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) x v
⊢ ∃ (L : StrongDual ℝ E), ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) x v

Tactic:
refine ⟨L, fun v hv ↦ ?_⟩
-- Module: Mathlib.Analysis.Calculus.Rademacher
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
⊢ (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]
-- Module: Mathlib.Analysis.Calculus.Rademacher
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
J : (L : (a : E) → ℝ) v = lineDeriv ℝ f x v
⊢ HasLineDerivAt ℝ f ((L : (a : E) → ℝ) v) x v

Tactic:
simpa [J] using (h'x v hv).hasLineDerivAt

Premises used: LineDifferentiableAt.hasLineDerivAt
-- Module: Mathlib.Analysis.Calculus.Rademacher
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
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‖
⊢ HasFDerivAt f L x

Tactic:
rw [hasFDerivAt_iff_isLittleO_nhds_zero, isLittleO_iff]

Premises used: Asymptotics.isLittleO_iff, hasFDerivAt_iff_isLittleO_nhds_zero
-- Module: Mathlib.Analysis.Calculus.Rademacher
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 < ε
⊢ 0 < ε / ((↑C : ℝ) + ‖L‖ + 1)

Tactic:
positivity
-- Module: Mathlib.Analysis.Calculus.Rademacher
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 < ε
⊢ (↑C : ℝ) + ‖L‖ + 1 ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Calculus.Rademacher
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 < ε
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‖
⊢ ∀ᶠ (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)⟩

Premises used: Norm.norm, HAdd.hAdd, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Analysis.Calculus.Rademacher
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) * δ = ε
apply :
  ∀ (z : E) (hz : z ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s),
    Membership.mem (γ := Set E) (⋃ y ∈ s, ball y δ) z
⊢ Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ s, ball y δ)

Tactic:
apply hs.trans (fun z hz ↦ ?_)

Premises used: HasSubset.Subset.trans
-- Module: Mathlib.Analysis.Calculus.Rademacher
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
⊢ ∃ y ∈ s, dist z y < δ

Tactic:
Metric.mem_closure_iff.1 hz δ δpos

Premises used: Metric.mem_closure_iff, Iff.mp
-- Module: Mathlib.Analysis.Calculus.Rademacher
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
obtain : ∀ (y : E) (ys : y ∈ s) (hy : dist z y < δ), Membership.mem (γ := Set E) (⋃ y ∈ s, ball y δ) z
⊢ 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

Premises used: Metric.mem_closure_iff, Iff.mp
-- Module: Mathlib.Analysis.Calculus.Rademacher
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
y : E
ys : y ∈ s
hy : dist z y < δ
⊢ Membership.mem (γ := Set E) (⋃ y ∈ s, ball y δ) z

Tactic:
mem_biUnion ys hy

Premises used: Set.mem_biUnion
-- Module: Mathlib.Analysis.Calculus.Rademacher
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
y : E
ys : y ∈ s
hy : dist z y < δ
⊢ Membership.mem (γ := Set E) (⋃ y ∈ s, ball y δ) z

Tactic:
exact mem_biUnion ys hy

Premises used: Set.mem_biUnion
-- Module: Mathlib.Analysis.Calculus.Rademacher
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 δ)

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
-- Module: Mathlib.Analysis.Calculus.Rademacher
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) * δ = ε
this : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ s, ball y δ)
⊢ ∃ q ⊆ s, q.Finite ∧ Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)

Tactic:
(isCompact_sphere 0 1).elim_finite_subcover_image (fun y _hy ↦ isOpen_ball) this

Premises used: isCompact_sphere, Metric.isOpen_ball, IsCompact.elim_finite_subcover_image, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Rademacher
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) * δ = ε
this : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ s, ball y δ)
⊢ ∃ q ⊆ s, q.Finite ∧ Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)

Tactic:
exact (isCompact_sphere 0 1).elim_finite_subcover_image (fun y _hy ↦ isOpen_ball) this

Premises used: isCompact_sphere, Metric.isOpen_ball, IsCompact.elim_finite_subcover_image, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Rademacher
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) * δ = ε
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‖
⊢ ∀ᶠ (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

Premises used: OfNat.ofNat, Metric.sphere
-- Module: Mathlib.Analysis.Calculus.Rademacher
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 δ)
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‖
⊢ ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖

Tactic:
apply (Finite.eventually_all q_fin).2 (fun v hv ↦ ?_)

Premises used: Iff.mpr, Set.Finite.eventually_all
-- Module: Mathlib.Analysis.Calculus.Rademacher
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
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
⊢ ∀ᶠ (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 Asymptotics.IsLittleO.def ?_ δpos

Premises used: Asymptotics.IsLittleO.def