awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s t : Set E
x : E
inst_3 : ContinuousAdd E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
hy : ClusterPt y (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
h₁ : Tendsto (fun (x_1 : E) ↦ x + x_1) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) (𝓝[s] x)
⊢ Membership.mem (γ := Filter E) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' t)

Tactic:
suffices Tendsto (x + ·) (𝓝[(x + ·) ⁻¹' s] 0) (𝓝[s] x) from
    this.mono_right h |> tendsto_nhdsWithin_iff.mp |>.2
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s t : Set E
x : E
inst_3 : ContinuousAdd E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
hy : ClusterPt y (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
⊢ Tendsto (fun (x_1 : E) ↦ x + x_1) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) (𝓝[s] x)

Tactic:
.inf ?_ (mapsTo_preimage _ _).tendsto

Premises used: Set.MapsTo.tendsto, nhdsWithin, Set.mapsTo_preimage, Filter.Tendsto.inf
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s t : Set E
x : E
inst_3 : ContinuousAdd E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
hy : ClusterPt y (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
h₁ : Tendsto (fun (x_1 : E) ↦ x + x_1) (𝓝 0) (𝓝 x)
⊢ Tendsto (fun (x_1 : E) ↦ x + x_1) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) (𝓝[s] x)

Tactic:
refine .inf ?_ (mapsTo_preimage _ _).tendsto
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s t : Set E
x : E
inst_3 : ContinuousAdd E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
hy : ClusterPt y (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
⊢ Tendsto (fun (x_1 : E) ↦ x + x_1) (𝓝 0) (𝓝 x)

Tactic:
(continuous_const_add x).tendsto' 0 x (add_zero _)

Premises used: Continuous.tendsto', continuous_const_add, add_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s t : Set E
x : E
inst_3 : ContinuousAdd E
h : 𝓝[s] x ≤ 𝓝[t] x
y : E
hy : ClusterPt y (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter 𝕜) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
⊢ Tendsto (fun (x_1 : E) ↦ x + x_1) (𝓝 0) (𝓝 x)

Tactic:
exact (continuous_const_add x).tendsto' 0 x (add_zero _)

Premises used: Continuous.tendsto', continuous_const_add, add_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s t : Set E
x : E
inst_3 : ContinuousAdd E
h : 𝓝[s] x = 𝓝[t] x
⊢ tangentConeAt 𝕜 s x = tangentConeAt 𝕜 t x

Tactic:
Subset.antisymm (tangentConeAt_mono_nhds h.le) (tangentConeAt_mono_nhds h.ge)

Premises used: Set.Subset.antisymm, Eq.ge, Eq.le, tangentConeAt_mono_nhds
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul 𝕜 E
inst_2 : TopologicalSpace E
s t : Set E
x : E
inst_3 : ContinuousAdd E
ht : t ∈ 𝓝 x
⊢ tangentConeAt 𝕜 (s ∩ t) x = tangentConeAt 𝕜 s x

Tactic:
tangentConeAt_congr (nhdsWithin_restrict' _ ht).symm

Premises used: tangentConeAt_congr, nhdsWithin_restrict', Eq.symm
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
h : (tangentConeAt 𝕜 s x).Nonempty
rcases : ∀ (y : E) (hy : y ∈ tangentConeAt 𝕜 s x), x ∈ closure[inst_2] s
⊢ x ∈ closure[inst_2] s

Tactic:
rcases h with ⟨y, hy⟩
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
rcases :
  ∀ (ι : 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
⊢ x ∈ closure[inst_2] s

Tactic:
rcases exists_fun_of_mem_tangentConeAt hy with ⟨ι, l, hl, -, d, hd, hds, -⟩

Premises used: exists_fun_of_mem_tangentConeAt
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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

Tactic:
mem_closure_of_tendsto ?_ hds

Premises used: mem_closure_of_tendsto
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
refine : Tendsto (fun (x_1 : ι) ↦ x + d x_1) l (𝓝 x)
⊢ x ∈ closure[inst_2] s

Tactic:
refine mem_closure_of_tendsto ?_ hds

Premises used: mem_closure_of_tendsto
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
⊢ Tendsto (fun (x_1 : ι) ↦ x + d x_1) l (𝓝 x)

Tactic:
simpa using tendsto_const_nhds.add hd

Premises used: tendsto_const_nhds, Filter.Tendsto.add
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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

Tactic:
Subset.antisymm ?_ (tangentConeAt_mono subset_closure)

Premises used: Set.Subset.antisymm, subset_closure, tangentConeAt_mono
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
refine : tangentConeAt 𝕜 (closure[inst_2] s) x ⊆ tangentConeAt 𝕜 s x
⊢ tangentConeAt 𝕜 (closure[inst_2] s) x = tangentConeAt 𝕜 s x

Tactic:
refine Subset.antisymm ?_ (tangentConeAt_mono subset_closure)

Premises used: Set.Subset.antisymm, subset_closure, tangentConeAt_mono
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
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)))
⊢ tangentConeAt 𝕜 (closure[inst_2] s) x ⊆ tangentConeAt 𝕜 s x

Tactic:
simp only [(nhds_basis_opens _).tangentConeAt_eq_biInter_closure]

Premises used: nhds_basis_opens, Filter.HasBasis.tangentConeAt_eq_biInter_closure
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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)))

Tactic:
iInter₂_mono fun U hU ↦ closure_minimal ?_ isClosed_closure

Premises used: closure_minimal, Set.iInter₂_mono, isClosed_closure
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
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))
⊢ 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:
refine iInter₂_mono fun U hU ↦ closure_minimal ?_ isClosed_closure

Premises used: closure_minimal, Set.iInter₂_mono, isClosed_closure
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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))
grw₂ 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))
⊢ 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:
grw [(isOpenMap_add_left x).preimage_closure_subset_closure_preimage, hU.2.inter_closure,
    set_smul_closure_subset]

Premises used: set_smul_closure_subset, isOpenMap_add_left, IsOpen.inter_closure, And.right, IsOpenMap.preimage_closure_subset_closure_preimage
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
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
⊢ UniqueDiffWithinAt 𝕜 t x

Tactic:
rw [uniqueDiffWithinAt_iff] at *

Premises used: uniqueDiffWithinAt_iff
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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 : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s
st : s ⊆ t
grw : 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:
grw [← st]
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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 : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s
st : s ⊆ t
⊢ Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s

Tactic:
h
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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 : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s
st : s ⊆ t
⊢ Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s

Tactic:
exact h
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : Semiring 𝕜
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
s : Set E
x : E
h : UniqueDiffWithinAt 𝕜 s x
⊢ UniqueDiffWithinAt 𝕜 (closure[inst_3] s) x

Tactic:
h.mono subset_closure

Premises used: subset_closure, UniqueDiffWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
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
⊢ UniqueDiffWithinAt 𝕜 t x

Tactic:
simp only [uniqueDiffWithinAt_iff] at *

Premises used: uniqueDiffWithinAt_iff
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
rw :
  ∀ (h : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ (𝓝[s] x).NeBot),
    Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t x)) : Set E) ∧ (𝓝[t] x).NeBot
⊢ Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t x)) : Set E) ∧ x ∈ closure[inst_3] t

Tactic:
rw [mem_closure_iff_nhdsWithin_neBot] at h ⊢

Premises used: mem_closure_iff_nhdsWithin_neBot
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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) ∧ (𝓝[s] x).NeBot
⊢ Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t x)) : Set E) ∧ (𝓝[t] x).NeBot

Tactic:
⟨h.1.mono <| Submodule.span_mono <| tangentConeAt_mono_nhds st, h.2.mono st⟩

Premises used: Filter.NeBot.mono, Dense.mono, tangentConeAt_mono_nhds, And.right, And.left, And.intro, Submodule.span_mono
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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) ∧ (𝓝[s] x).NeBot
⊢ Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 t x)) : Set E) ∧ (𝓝[t] x).NeBot

Tactic:
exact ⟨h.1.mono <| Submodule.span_mono <| tangentConeAt_mono_nhds st, h.2.mono st⟩
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
⊢ UniqueDiffWithinAt 𝕜 s x ↔ UniqueDiffWithinAt 𝕜 t x

Tactic:
⟨fun h => h.mono_nhds <| le_of_eq st, fun h => h.mono_nhds <| le_of_eq st.symm⟩

Premises used: Iff.intro, le_of_eq, Eq.symm, UniqueDiffWithinAt.mono_nhds
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
ht : t ∈ 𝓝 x
⊢ UniqueDiffWithinAt 𝕜 (s ∩ t) x ↔ UniqueDiffWithinAt 𝕜 s x

Tactic:
uniqueDiffWithinAt_congr <| (nhdsWithin_restrict' _ ht).symm

Premises used: uniqueDiffWithinAt_congr, nhdsWithin_restrict', Eq.symm
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
hs : UniqueDiffWithinAt 𝕜 s x
ht : t ∈ 𝓝 x
⊢ UniqueDiffWithinAt 𝕜 (s ∩ t) x

Tactic:
(uniqueDiffWithinAt_inter ht).2 hs

Premises used: Iff.mpr, uniqueDiffWithinAt_inter
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
hs : UniqueDiffOn 𝕜 s
ht : IsOpen[inst_3] t
⊢ UniqueDiffOn 𝕜 (s ∩ t)

Tactic:
fun x hx => (hs x hx.1).inter (IsOpen.mem_nhds ht hx.2)

Premises used: UniqueDiffOn, UniqueDiffWithinAt.inter, And.right, And.left, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
ht : t ∈ 𝓝[s] x
⊢ UniqueDiffWithinAt 𝕜 (s ∩ t) x ↔ UniqueDiffWithinAt 𝕜 s x

Tactic:
uniqueDiffWithinAt_congr <| (nhdsWithin_restrict'' _ ht).symm

Premises used: nhdsWithin_restrict'', uniqueDiffWithinAt_congr, Eq.symm
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
hs : UniqueDiffWithinAt 𝕜 s x
ht : t ∈ 𝓝[s] x
⊢ UniqueDiffWithinAt 𝕜 (s ∩ t) x

Tactic:
(uniqueDiffWithinAt_inter' ht).2 hs

Premises used: Iff.mpr, uniqueDiffWithinAt_inter'
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
⊢ ∃ᶠ (x : E) in 𝓝 x, x ∈ s

Tactic:
rw [mem_closure_iff_frequently] at hx

Premises used: mem_closure_iff_frequently
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
hcd : Tendsto (β := E) (fun (n : E) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (1 n) (n + -x)) (𝓝 x) (𝓝 0)
⊢ 0 ∈ tangentConeAt 𝕜 s x

Tactic:
apply mem_tangentConeAt_of_frequently (𝓝 x) 1 (· + (-x))

Premises used: mem_tangentConeAt_of_frequently, nhds, HAdd.hAdd, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
⊢ Continuous[inst_3, inst_3] fun (x_1 : E) ↦ x_1 + -x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
⊢ x + -x = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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 (x_1 : E) ↦ x_1 + -x) (𝓝 x) (𝓝 0)

Tactic:
exact Continuous.tendsto' (by fun_prop) _ _ (by simp)

Premises used: Continuous.tendsto'
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
⊢ ∃ᶠ (n : E) in 𝓝 x, x + (n + -x) ∈ s

Tactic:
simpa
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
hcd : Tendsto (β := E) (fun (n : E) ↦ n + -x) (𝓝 x) (𝓝 0)
⊢ Tendsto (β := E) (fun (n : E) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (1 n) (n + -x)) (𝓝 x) (𝓝 0)

Tactic:
simp only [Pi.one_apply, one_smul]

Premises used: Pi.one_apply, one_smul
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
⊢ Continuous[inst_3, inst_3] fun (n : E) ↦ n + -x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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) ↦ n + -x) (𝓝 x) (𝓝 0)

Tactic:
exact Continuous.tendsto' (by fun_prop) _ _ (by simp)

Premises used: Continuous.tendsto'
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
⊢ 0 ∈ tangentConeAt 𝕜 s x ↔ x ∈ closure[inst_3] s

Tactic:
⟨fun h ↦ mem_closure_of_nonempty_tangentConeAt ⟨_, h⟩, zero_mem_tangentConeAt⟩

Premises used: Iff.intro, zero_mem_tangentConeAt, Exists.intro, OfNat.ofNat, mem_closure_of_nonempty_tangentConeAt
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
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
⊢ Membership.mem (γ := Set E) 0 y

Tactic:
rcases exists_fun_of_mem_tangentConeAt hy with ⟨ι, l, hl, c, d, hd₀, hds, hcd⟩

Premises used: exists_fun_of_mem_tangentConeAt
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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)
⊢ Tendsto (fun (x_1 : ι) ↦ x + d x_1) l (𝓝 x)

Tactic:
simpa using tendsto_const_nhds.add hd₀

Premises used: tendsto_const_nhds, Filter.Tendsto.add
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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)
⊢ 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₀