awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s : Set E
x : E
inst_3 : ContinuousAdd E
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
d : ι → E
hd : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
⊢ x ∈ closure[inst_2] s
have refine : Tendsto (fun (x_1 : ι) ↦ x + d x_1) l (𝓝 x)
Tactic: refine mem_closure_of_tendsto ?_ hds
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s : Set E
x : E
inst_3 : ContinuousAdd E
inst_4 : ContinuousConstSMul 𝕜 E
⊢ tangentConeAt 𝕜 (closure[inst_2] s) x = tangentConeAt 𝕜 s x
have refine : tangentConeAt 𝕜 (closure[inst_2] s) x ⊆ tangentConeAt 𝕜 s x
Tactic: refine Subset.antisymm ?_ (tangentConeAt_mono subset_closure)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s : Set E
x : E
inst_3 : ContinuousAdd E
inst_4 : ContinuousConstSMul 𝕜 E
⊢ tangentConeAt 𝕜 (closure[inst_2] s) x ⊆ tangentConeAt 𝕜 s x
have simp : Subset.{u_2} (α := Set E)
  (⋂ (i : Set E),
    ⋂ (_ : 0 ∈ i ∧ IsOpen[inst_2] i),
      closure[inst_2]
        (HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (i ∩ (fun (x_2 : E) ↦ x + x_2) ⁻¹' closure[inst_2] s)))
  (⋂ (i : Set E),
    ⋂ (_ : 0 ∈ i ∧ IsOpen[inst_2] i),
      closure[inst_2] (HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (i ∩ (fun (x_2 : E) ↦ x + x_2) ⁻¹' s)))
Tactic: simp only [(nhds_basis_opens _).tangentConeAt_eq_biInter_closure]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s : Set E
x : E
inst_3 : ContinuousAdd E
inst_4 : ContinuousConstSMul 𝕜 E
⊢ Subset.{u_2} (α := Set E)
    (⋂ (i : Set E),
      ⋂ (_ : 0 ∈ i ∧ IsOpen[inst_2] i),
        closure[inst_2]
          (HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (i ∩ (fun (x_2 : E) ↦ x + x_2) ⁻¹' closure[inst_2] s)))
    (⋂ (i : Set E),
      ⋂ (_ : 0 ∈ i ∧ IsOpen[inst_2] i),
        closure[inst_2] (HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (i ∩ (fun (x_2 : E) ↦ x + x_2) ⁻¹' s)))
have refine : ∀ (U : Set E) (hU : 0 ∈ U ∧ IsOpen[inst_2] U),
  HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ (fun (x_1 : E) ↦ x + x_1) ⁻¹' closure[inst_2] s) ⊆
    closure[inst_2] (HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ (fun (x_1 : E) ↦ x + x_1) ⁻¹' s))
Tactic: refine iInter₂_mono fun U hU ↦ closure_minimal ?_ isClosed_closure
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s : Set E
x : E
inst_3 : ContinuousAdd E
inst_4 : ContinuousConstSMul 𝕜 E
U : Set E
hU : 0 ∈ U ∧ IsOpen[inst_2] U
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ (fun (x_1 : E) ↦ x + x_1) ⁻¹' closure[inst_2] s) ⊆
    closure[inst_2] (HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ (fun (x_1 : E) ↦ x + x_1) ⁻¹' s))
have grw : HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ closure[inst_2] ((fun (x_1 : E) ↦ x + x_1) ⁻¹' s)) ⊆
  closure[inst_2] (HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ (fun (x_1 : E) ↦ x + x_1) ⁻¹' s))
Tactic: grw [(isOpenMap_add_left x).preimage_closure_subset_closure_preimage, hU.2.inter_closure,
    set_smul_closure_subset]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s : Set E
x : E
inst_3 : ContinuousAdd E
inst_4 : ContinuousConstSMul 𝕜 E
U : Set E
hU : 0 ∈ U ∧ IsOpen[inst_2] U
grw :
  HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ closure[inst_2] ((fun (x_1 : E) ↦ x + x_1) ⁻¹' s)) ⊆
    closure[inst_2] (HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ (fun (x_1 : E) ↦ x + x_1) ⁻¹' s))
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ (fun (x_1 : E) ↦ x + x_1) ⁻¹' closure[inst_2] s) ⊆
    closure[inst_2] (HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ (fun (x_1 : E) ↦ x + x_1) ⁻¹' s))
have grw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (closure[inst_2] (U ∩ (fun (x_1 : E) ↦ x + x_1) ⁻¹' s)) ⊆
  closure[inst_2] (HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ (fun (x_1 : E) ↦ x + x_1) ⁻¹' s))
Tactic: grw [(isOpenMap_add_left x).preimage_closure_subset_closure_preimage, hU.2.inter_closure,
    set_smul_closure_subset]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s : Set E
x : E
inst_3 : ContinuousAdd E
inst_4 : ContinuousConstSMul 𝕜 E
U : Set E
hU : 0 ∈ U ∧ IsOpen[inst_2] U
grw :
  HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ closure[inst_2] ((fun (x_1 : E) ↦ x + x_1) ⁻¹' s)) ⊆
    closure[inst_2] (HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ (fun (x_1 : E) ↦ x + x_1) ⁻¹' s))
grw₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (closure[inst_2] (U ∩ (fun (x_1 : E) ↦ x + x_1) ⁻¹' s)) ⊆
    closure[inst_2] (HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ (fun (x_1 : E) ↦ x + x_1) ⁻¹' s))
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ (fun (x_1 : E) ↦ x + x_1) ⁻¹' closure[inst_2] s) ⊆
    closure[inst_2] (HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ (fun (x_1 : E) ↦ x + x_1) ⁻¹' s))
have grw₂ : closure[inst_2] (HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ (fun (x_1 : E) ↦ x + x_1) ⁻¹' s)) ⊆
  closure[inst_2] (HSMul.hSMul.{u_1, u_2, u_2} (α := Set 𝕜) univ (U ∩ (fun (x_1 : E) ↦ x + x_1) ⁻¹' s))
Tactic: grw [(isOpenMap_add_left x).preimage_closure_subset_closure_preimage, hU.2.inter_closure,
    set_smul_closure_subset]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Semiring 𝕜
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
s t : Set E
x : E
h : UniqueDiffWithinAt 𝕜 s x
st : s ⊆ t
⊢ UniqueDiffWithinAt 𝕜 t x
have rw : ∀ (h : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s) (st : s ⊆ t),
  Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t x)) : Set E) ∧ x ∈ closure[inst_3] t
Tactic: rw [uniqueDiffWithinAt_iff] at *
Cleared hypotheses: h, st
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Semiring 𝕜
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
s t : Set E
x : E
h : UniqueDiffWithinAt 𝕜 s x
st : 𝓝[s] x ≤ 𝓝[t] x
⊢ UniqueDiffWithinAt 𝕜 t x
have simp : ∀ (h : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s),
  Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t x)) : Set E) ∧ x ∈ closure[inst_3] t
Tactic: simp only [uniqueDiffWithinAt_iff] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Semiring 𝕜
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
s t : Set E
x : E
st : 𝓝[s] x ≤ 𝓝[t] x
h : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s
⊢ Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t x)) : Set E) ∧ x ∈ closure[inst_3] t
have rw : ∀ (h : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ (𝓝[s] x).NeBot),
  Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t x)) : Set E) ∧ (𝓝[t] x).NeBot
Tactic: rw [mem_closure_iff_nhdsWithin_neBot] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Semiring 𝕜
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
s : Set E
x : E
hx : x ∈ closure[inst_3] s
⊢ 0 ∈ tangentConeAt 𝕜 s x
have hx₁ : ∃ᶠ (x : E) in 𝓝 x, x ∈ s
Tactic: rw [mem_closure_iff_frequently] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Semiring 𝕜
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
s : Set E
x : E
hx : ∃ᶠ (x : E) in 𝓝 x, x ∈ s
⊢ 0 ∈ tangentConeAt 𝕜 s x
have hd₀ : Tendsto (β := E) (fun (x_1 : E) ↦ x_1 + -x) (𝓝 x) (𝓝 0)
Tactic: apply mem_tangentConeAt_of_frequently (𝓝 x) 1 (· + (-x))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Semiring 𝕜
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
s : Set E
x : E
hx : ∃ᶠ (x : E) in 𝓝 x, x ∈ s
hd₀ : Tendsto (β := E) (fun (x_1 : E) ↦ x_1 + -x) (𝓝 x) (𝓝 0)
⊢ 0 ∈ tangentConeAt 𝕜 s x
have hds : ∃ᶠ (n : E) in 𝓝 x, x + (n + -x) ∈ s
Tactic: apply mem_tangentConeAt_of_frequently (𝓝 x) 1 (· + (-x))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Semiring 𝕜
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
s : Set E
x : E
hx : ∃ᶠ (x : E) in 𝓝 x, x ∈ s
hd₀ : Tendsto (β := E) (fun (x_1 : E) ↦ x_1 + -x) (𝓝 x) (𝓝 0)
hds : ∃ᶠ (n : E) in 𝓝 x, x + (n + -x) ∈ s
⊢ 0 ∈ tangentConeAt 𝕜 s x
have hcd : Tendsto (β := E) (fun (n : E) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (1 n) (n + -x)) (𝓝 x) (𝓝 0)
Tactic: apply mem_tangentConeAt_of_frequently (𝓝 x) 1 (· + (-x))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Semiring 𝕜
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
s : Set E
x : E
hx : ∃ᶠ (x : E) in 𝓝 x, x ∈ s
⊢ Tendsto (β := E) (fun (n : E) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (1 n) (n + -x)) (𝓝 x) (𝓝 0)
have hcd : Tendsto (β := E) (fun (n : E) ↦ n + -x) (𝓝 x) (𝓝 0)
Tactic: simp only [Pi.one_apply, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Semiring 𝕜
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
s : Set E
x : E
inst_5 : T2Space E
hx : ¬AccPt x (𝓟 s)
y : E
hy : y ∈ tangentConeAt 𝕜 s x
⊢ Membership.mem (γ := Set E) 0 y
have rcases : ∀ (ι : Type (max u_1 u_2)) (l : Filter ι) (hl : l.NeBot) (c : ι → 𝕜) (d : ι → E) (hd₀ : Tendsto d l (𝓝 0))
  (hds : ∀ᶠ (n : ι) in l, x + d n ∈ s) (hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)),
  Membership.mem (γ := Set E) 0 y
Tactic: rcases exists_fun_of_mem_tangentConeAt hy with ⟨ι, l, hl, c, d, hd₀, hds, hcd⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Semiring 𝕜
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
s : Set E
x : E
inst_5 : T2Space E
hx : ¬AccPt x (𝓟 s)
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
⊢ Membership.mem (γ := Set E) 0 y
have H₁ : Tendsto (fun (x_1 : ι) ↦ x + d x_1) l (𝓝 x)
Tactic: have H₁ : Tendsto (x + d ·) l (𝓝 x) := by
    simpa using tendsto_const_nhds.add hd₀
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Semiring 𝕜
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
s : Set E
x : E
inst_5 : T2Space E
hx : ¬AccPt x (𝓟 s)
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
H₁ : Tendsto (fun (x_1 : ι) ↦ x + d x_1) l (𝓝 x)
⊢ ∀ᶠ (n : ι) in l, d n = 0
have hx₁ : ∀ᶠ (x_1 : E) in 𝓝 x, x_1 ∈ s → x_1 = x
Tactic: simp only [accPt_iff_frequently, not_frequently, not_and', ne_eq, not_not] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Semiring 𝕜
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
s : Set E
x : E
inst_5 : T2Space E
hx : ¬AccPt x (𝓟 s)
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
H₁ : Tendsto (fun (x_1 : ι) ↦ x + d x_1) l (𝓝 x)
⊢ Membership.mem (γ := Set E) 0 y
have H₂ : ∀ᶠ (n : ι) in l, d n = 0
Tactic: have H₂ : ∀ᶠ n in l, d n = 0 := by
    simp only [accPt_iff_frequently, not_frequently, not_and', ne_eq, not_not] at hx
    simpa using hds.mp (H₁.eventually hx)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Semiring 𝕜
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
s : Set E
x : E
inst_5 : T2Space E
hx : ¬AccPt x (𝓟 s)
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
H₁ : Tendsto (fun (x_1 : ι) ↦ x + d x_1) l (𝓝 x)
H₂ : ∀ᶠ (n : ι) in l, d n = 0
⊢ Membership.mem (γ := Set E) 0 y
have H₃ : ∀ᶠ (n : ι) in l, c n • d n = 0
Tactic: have H₃ : ∀ᶠ n in l, c n • d n = 0 := H₂.mono fun n hn ↦ by simp [hn]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Semiring 𝕜
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
s : Set E
x : E
inst_5 : T2Space E
y : E
hy : y ∈ tangentConeAt 𝕜 s x
hy₀ : y ≠ 0
⊢ AccPt x (𝓟 s)
have contrapose : ∀ (hy₀ : ¬AccPt x (𝓟 s)), y = 0
Tactic: contrapose hy₀
Cleared hypotheses: hy₀
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Semiring 𝕜
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
s : Set E
x : E
inst_5 : T2Space E
inst_6 : Nontrivial E
h : UniqueDiffWithinAt 𝕜 s x
⊢ AccPt x (𝓟 s)
have by_contra! : ∀ (h' : ¬AccPt x (𝓟 s)), False
Tactic: by_contra! h'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Semiring 𝕜
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
s : Set E
x : E
inst_5 : T2Space E
inst_6 : Nontrivial E
h : UniqueDiffWithinAt 𝕜 s x
h' : ¬AccPt x (𝓟 s)
⊢ (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ⊆ (↑(Submodule.span 𝕜 0) : Set E)
have _a : tangentConeAt 𝕜 s x ⊆ 0
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Semiring 𝕜
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
s : Set E
x : E
inst_5 : T2Space E
inst_6 : Nontrivial E
h : UniqueDiffWithinAt 𝕜 s x
h' : ¬AccPt x (𝓟 s)
⊢ False
have this : Dense (↑(Submodule.span 𝕜 0) : Set E)
Tactic: have : Dense (Submodule.span 𝕜 (0 : Set E) : Set E) :=
    h.1.mono <| by gcongr; exact tangentConeAt_subset_zero h'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DivisionSemiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace 𝕜
inst_4 : TopologicalSpace E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
x y : E
α : Type u_3
l : Filter α
inst_6 : l.NeBot
c : α → 𝕜
hc₀ : Tendsto c l (𝓝[≠] 0)
hmem : ∀ᶠ (n : α) in l, x + c n • y ∈ s
⊢ y ∈ tangentConeAt 𝕜 s x
have hc₁ : Tendsto c l (𝓝 0) ∧ ∀ᶠ (n : α) in l, Membership.mem (γ := Set 𝕜) {0}ᶜ (c n)
Tactic: rw [tendsto_nhdsWithin_iff] at hc₀
Cleared hypotheses: hc₀, hmem
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DivisionSemiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace 𝕜
inst_4 : TopologicalSpace E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
x y : E
α : Type u_3
l : Filter α
inst_6 : l.NeBot
c : α → 𝕜
hc₀ : Tendsto c l (𝓝 0) ∧ ∀ᶠ (n : α) in l, Membership.mem (γ := Set 𝕜) {0}ᶜ (c n)
hmem : ∀ᶠ (n : α) in l, x + c n • y ∈ s
⊢ y ∈ tangentConeAt 𝕜 s x
have refine_1 : Tendsto.{u_3, u_2} (β := E) (fun (x : α) ↦ c x • y) l (𝓝 0)
Tactic: refine mem_tangentConeAt_of_seq l c⁻¹ (c · • y) ?_ hmem ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DivisionSemiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace 𝕜
inst_4 : TopologicalSpace E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
x y : E
α : Type u_3
l : Filter α
inst_6 : l.NeBot
c : α → 𝕜
hc₀ : Tendsto c l (𝓝 0) ∧ ∀ᶠ (n : α) in l, Membership.mem (γ := Set 𝕜) {0}ᶜ (c n)
hmem : ∀ᶠ (n : α) in l, x + c n • y ∈ s
refine_1 : Tendsto.{u_3, u_2} (β := E) (fun (x : α) ↦ c x • y) l (𝓝 0)
⊢ y ∈ tangentConeAt 𝕜 s x
have refine_2 : Tendsto (fun (n : α) ↦ HSMul.hSMul (β := E) (c⁻¹ n) ((fun (x : α) ↦ c x • y) n)) l (𝓝 y)
Tactic: refine mem_tangentConeAt_of_seq l c⁻¹ (c · • y) ?_ hmem ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DivisionSemiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace 𝕜
inst_4 : TopologicalSpace E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
x y : E
α : Type u_3
l : Filter α
inst_6 : l.NeBot
c : α → 𝕜
hc₀ : Tendsto c l (𝓝 0) ∧ ∀ᶠ (n : α) in l, Membership.mem (γ := Set 𝕜) {0}ᶜ (c n)
hmem : ∀ᶠ (n : α) in l, x + c n • y ∈ s
⊢ Tendsto (fun (n : α) ↦ HSMul.hSMul (β := E) (c⁻¹ n) ((fun (x : α) ↦ c x • y) n)) l (𝓝 y)
have refine_2 : ∀ (n : α) (hn : Membership.mem (γ := Set 𝕜) {0}ᶜ (c n)), HSMul.hSMul (β := E) (c⁻¹ n) ((fun (x : α) ↦ c x • y) n) = y
Tactic: refine tendsto_nhds_of_eventually_eq <| hc₀.2.mono fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DivisionSemiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace 𝕜
inst_4 : TopologicalSpace E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
x : E
inst_6 : NeBot (α := 𝕜) (𝓝[≠] 0)
inst_7 : ContinuousAdd E
h : s ∈ 𝓝 x
⊢ tangentConeAt 𝕜 s x = univ
have rw : tangentConeAt 𝕜 (univ ∩ s) x = univ
Tactic: rw [← s.univ_inter, tangentConeAt_inter_nhds h, tangentConeAt_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DivisionSemiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace 𝕜
inst_4 : TopologicalSpace E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
x : E
inst_6 : NeBot (α := 𝕜) (𝓝[≠] 0)
inst_7 : ContinuousAdd E
h : s ∈ 𝓝 x
rw : tangentConeAt 𝕜 (univ ∩ s) x = univ
⊢ tangentConeAt 𝕜 s x = univ
have rw₁ : tangentConeAt 𝕜 univ x = univ
Tactic: rw [← s.univ_inter, tangentConeAt_inter_nhds h, tangentConeAt_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DivisionSemiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace 𝕜
inst_4 : TopologicalSpace E
inst_5 : ContinuousSMul 𝕜 E
s : Set E
x : E
inst_6 : NeBot (α := 𝕜) (𝓝[≠] 0)
inst_7 : ContinuousAdd E
h : s ∈ 𝓝 x
rw : tangentConeAt 𝕜 (univ ∩ s) x = univ
rw₁ : tangentConeAt 𝕜 univ x = univ
⊢ tangentConeAt 𝕜 s x = univ
have rw₂ : Eq.{u_2 + 1} (α := Set E) univ univ
Tactic: rw [← s.univ_inter, tangentConeAt_inter_nhds h, tangentConeAt_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
x : E
s : Set E
𝕜' : Type u_3
inst_4 : Semiring 𝕜'
inst_5 : SMul 𝕜 𝕜'
inst_6 : Module 𝕜' E
inst_7 : IsScalarTower 𝕜 𝕜' E
hs : UniqueDiffWithinAt 𝕜 s x
⊢ UniqueDiffWithinAt 𝕜' s x
have simp_all : ∀ (hs : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s),
  Dense (↑(Submodule.span 𝕜' (tangentConeAt 𝕜' s x)) : Set E)
Tactic: simp_all only [uniqueDiffWithinAt_iff, and_true]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
x : E
s : Set E
𝕜' : Type u_3
inst_4 : Semiring 𝕜'
inst_5 : SMul 𝕜 𝕜'
inst_6 : Module 𝕜' E
inst_7 : IsScalarTower 𝕜 𝕜' E
hs : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s
⊢ Dense (↑(Submodule.span 𝕜' (tangentConeAt 𝕜' s x)) : Set E)
have apply : (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ⊆ (↑(Submodule.span 𝕜' (tangentConeAt 𝕜' s x)) : Set E)
Tactic: apply Dense.mono _ hs.1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
x : E
s : Set E
𝕜' : Type u_3
inst_4 : Semiring 𝕜'
inst_5 : SMul 𝕜 𝕜'
inst_6 : Module 𝕜' E
inst_7 : IsScalarTower 𝕜 𝕜' E
hs : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s
⊢ (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ⊆ (↑(Submodule.span 𝕜' (tangentConeAt 𝕜' s x)) : Set E)
have trans : (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ⊆ (↑(Submodule.span 𝕜 (tangentConeAt 𝕜' s x)) : Set E)
Tactic: trans ↑(Submodule.span 𝕜 (tangentConeAt 𝕜' s x))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
x : E
s : Set E
𝕜' : Type u_3
inst_4 : Semiring 𝕜'
inst_5 : SMul 𝕜 𝕜'
inst_6 : Module 𝕜' E
inst_7 : IsScalarTower 𝕜 𝕜' E
hs : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s
trans : (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ⊆ (↑(Submodule.span 𝕜 (tangentConeAt 𝕜' s x)) : Set E)
⊢ (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ⊆ (↑(Submodule.span 𝕜' (tangentConeAt 𝕜' s x)) : Set E)
have trans₁ : (↑(Submodule.span 𝕜 (tangentConeAt 𝕜' s x)) : Set E) ⊆ (↑(Submodule.span 𝕜' (tangentConeAt 𝕜' s x)) : Set E)
Tactic: trans ↑(Submodule.span 𝕜 (tangentConeAt 𝕜' s x))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : DivisionSemiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : TopologicalSpace 𝕜
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
inst_6 : ContinuousSMul 𝕜 E
x : E
⊢ UniqueDiffWithinAt 𝕜 univ x
have rw : Dense (↑(Submodule.span 𝕜 univ) : Set E) ∧ Membership.mem (γ := Set E) (closure[inst_3] univ) x
Tactic: rw [uniqueDiffWithinAt_iff, tangentConeAt_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.TangentCone.Defs (hypothesis)
Goal:
R : Type u
E : Type v
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∃ᶠ (n : α) in l, x + d n ∈ s
hcd : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
this :
  Tendsto (fun (n : α) ↦ c n • d n) (l ⊓ 𝓟 {y : α | x + d y ∈ s})
    (HSMul.hSMul.{u, v, v} (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
⊢ y ∈ tangentConeAt R s x
have hds₁ : (l ⊓ 𝓟 {x_1 : α | x + d x_1 ∈ s}).NeBot
Tactic: rw [frequently_iff_neBot] at hds
Cleared hypotheses: hcd, this