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 : 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)
⊢ ∀ᶠ (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

Premises used: Classical.not_not, ne_eq, accPt_iff_frequently, Filter.not_frequently, not_and'
-- 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
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)
hx : ∀ᶠ (x_1 : E) in 𝓝 x, x_1 ∈ s → x_1 = x
⊢ ∀ᶠ (n : ι) in l, d n = 0

Tactic:
simpa using hds.mp (H₁.eventually hx)

Premises used: Filter.Eventually.mp, Filter.Tendsto.eventually
-- 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)
H₁ : Tendsto (fun (x_1 : ι) ↦ x + d x_1) l (𝓝 x)
⊢ ∀ᶠ (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)
-- 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)
H₁ : Tendsto (fun (x_1 : ι) ↦ x + d x_1) l (𝓝 x)
H₂ : ∀ᶠ (n : ι) in l, d n = 0
n : ι
hn : d n = 0
⊢ c n • d n = 0

Tactic:
simp [hn]
-- 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)
H₁ : Tendsto (fun (x_1 : ι) ↦ x + d x_1) l (𝓝 x)
H₂ : ∀ᶠ (n : ι) in l, d n = 0
⊢ ∀ᶠ (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]
-- 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)
H₁ : Tendsto (fun (x_1 : ι) ↦ x + d x_1) l (𝓝 x)
H₂ : ∀ᶠ (n : ι) in l, d n = 0
H₃ : ∀ᶠ (n : ι) in l, c n • d n = 0
⊢ Membership.mem (γ := Set E) 0 y

Tactic:
simpa using tendsto_nhds_unique_of_eventuallyEq hcd tendsto_const_nhds H₃

Premises used: tendsto_const_nhds, tendsto_nhds_unique_of_eventuallyEq
-- 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
y : E
hy : y ∈ tangentConeAt 𝕜 s x
hy₀ : y ≠ 0
contrapose : ∀ (hy₀ : ¬AccPt x (𝓟 s)), y = 0
⊢ AccPt x (𝓟 s)

Tactic:
contrapose hy₀
-- 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
y : E
hy : y ∈ tangentConeAt 𝕜 s x
hy₀ : ¬AccPt x (𝓟 s)
⊢ y = 0

Tactic:
tangentConeAt_subset_zero hy₀ hy

Premises used: Set.Mem, setOf, Set.singleton, tangentConeAt_subset_zero
-- 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
y : E
hy : y ∈ tangentConeAt 𝕜 s x
hy₀ : ¬AccPt x (𝓟 s)
⊢ y = 0

Tactic:
exact tangentConeAt_subset_zero hy₀ hy

Premises used: tangentConeAt_subset_zero
-- 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
inst_6 : Nontrivial E
h : UniqueDiffWithinAt 𝕜 s x
by_contra! : ∀ (h' : ¬AccPt x (𝓟 s)), False
⊢ AccPt x (𝓟 s)

Tactic:
by_contra! 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
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)
_a : tangentConeAt 𝕜 s x ⊆ 0
⊢ (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ⊆ (↑(Submodule.span 𝕜 0) : Set E)

Tactic:
gcongr
-- 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
inst_6 : Nontrivial E
h : UniqueDiffWithinAt 𝕜 s x
h' : ¬AccPt x (𝓟 s)
⊢ tangentConeAt 𝕜 s x ⊆ 0

Tactic:
tangentConeAt_subset_zero h'

Premises used: tangentConeAt_subset_zero
-- 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
inst_6 : Nontrivial E
h : UniqueDiffWithinAt 𝕜 s x
h' : ¬AccPt x (𝓟 s)
⊢ tangentConeAt 𝕜 s x ⊆ 0

Tactic:
exact tangentConeAt_subset_zero h'

Premises used: tangentConeAt_subset_zero
-- 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
inst_6 : Nontrivial E
h : UniqueDiffWithinAt 𝕜 s x
h' : ¬AccPt x (𝓟 s)
⊢ 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'
-- 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
inst_6 : Nontrivial E
h : UniqueDiffWithinAt 𝕜 s x
h' : ¬AccPt x (𝓟 s)
this : Dense (↑(Submodule.span 𝕜 0) : Set E)
⊢ False

Tactic:
simp [dense_iff_closure_eq] at this

Premises used: dense_iff_closure_eq
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
⊢ Tendsto c l (𝓝 0) ∧ ∀ᶠ (n : α) in l, Membership.mem (γ := Set 𝕜) {0}ᶜ (c n)

Tactic:
rw [tendsto_nhdsWithin_iff] at hc₀

Premises used: tendsto_nhdsWithin_iff
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
hc₁ : Tendsto c l (𝓝 0) ∧ ∀ᶠ (n : α) in l, Membership.mem (γ := Set 𝕜) {0}ᶜ (c n)
⊢ ∀ᶠ (n : α) in l, x + c n • y ∈ s

Tactic:
rw [tendsto_nhdsWithin_iff] at hc₀

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

Tactic:
mem_tangentConeAt_of_seq l c⁻¹ (c · • y) ?_ hmem ?_

Premises used: Inv.inv, mem_tangentConeAt_of_seq, HSMul.hSMul
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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)
refine_2 : Tendsto (fun (n : α) ↦ HSMul.hSMul (β := E) (c⁻¹ n) ((fun (x : α) ↦ c x • y) n)) l (𝓝 y)
⊢ y ∈ tangentConeAt 𝕜 s x

Tactic:
refine mem_tangentConeAt_of_seq l c⁻¹ (c · • y) ?_ hmem ?_

Premises used: Inv.inv, mem_tangentConeAt_of_seq, HSMul.hSMul
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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.{u_3, u_2} (β := E) (fun (x : α) ↦ c x • y) l (𝓝 0)

Tactic:
simpa using hc₀.1.smul (tendsto_const_nhds (x := y))

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

Tactic:
tendsto_nhds_of_eventually_eq <| hc₀.2.mono fun n hn ↦ ?_

Premises used: Filter.Eventually.mono, And.right, tendsto_nhds_of_eventually_eq
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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_2 :
  ∀ (n : α) (hn : Membership.mem (γ := Set 𝕜) {0}ᶜ (c n)), HSMul.hSMul (β := E) (c⁻¹ n) ((fun (x : α) ↦ c x • y) n) = y
⊢ Tendsto (fun (n : α) ↦ HSMul.hSMul (β := E) (c⁻¹ n) ((fun (x : α) ↦ c x • y) n)) l (𝓝 y)

Tactic:
refine tendsto_nhds_of_eventually_eq <| hc₀.2.mono fun n hn ↦ ?_

Premises used: Filter.Eventually.mono, And.right, tendsto_nhds_of_eventually_eq
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
n : α
hn : Membership.mem (γ := Set 𝕜) {0}ᶜ (c n)
⊢ HSMul.hSMul (β := E) (c⁻¹ n) ((fun (x : α) ↦ c x • y) n) = y

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
x : E
inst_6 : NeBot (α := 𝕜) (𝓝[≠] 0)
⊢ tangentConeAt 𝕜 univ x = univ

Tactic:
simp [tangentConeAt]

Premises used: tangentConeAt
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
rw₂ rw₃ : Eq.{u_2 + 1} (α := Set E) univ univ
⊢ tangentConeAt 𝕜 s x = univ

Tactic:
rw [← s.univ_inter, tangentConeAt_inter_nhds h, tangentConeAt_univ]

Premises used: tangentConeAt_inter_nhds, tangentConeAt_univ, Set.univ_inter
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
⊢ UniqueDiffOn.{u_1, u_2} 𝕜 (E := E) ∅

Tactic:
fun _ hx => hx.elim

Premises used: UniqueDiffOn, False.elim
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
x y : E
s : Set E
h : UniqueDiffWithinAt 𝕜 s x
hy : x = y
⊢ UniqueDiffWithinAt 𝕜 s y

Tactic:
hy ▸ h

Premises used: Eq.rec
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
simp_all :
  ∀ (hs : Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ∧ x ∈ closure[inst_3] s),
    Dense (↑(Submodule.span 𝕜' (tangentConeAt 𝕜' s x)) : Set E)
⊢ UniqueDiffWithinAt 𝕜' s x

Tactic:
simp_all only [uniqueDiffWithinAt_iff, and_true]

Premises used: and_true, uniqueDiffWithinAt_iff
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
apply : (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set E) ⊆ (↑(Submodule.span 𝕜' (tangentConeAt 𝕜' s x)) : Set E)
⊢ Dense (↑(Submodule.span 𝕜' (tangentConeAt 𝕜' s x)) : Set E)

Tactic:
apply Dense.mono _ hs.1

Premises used: Dense.mono, And.left
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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)
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)

Tactic:
trans ↑(Submodule.span 𝕜 (tangentConeAt 𝕜' s x))

Premises used: Submodule.span, tangentConeAt
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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)

Tactic:
simp [Submodule.span_mono tangentConeAt_mono_field]

Premises used: tangentConeAt_mono_field, Submodule.span_mono
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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)

Tactic:
simp [Submodule.span_mono tangentConeAt_mono_field]

Premises used: tangentConeAt_mono_field, Submodule.span_mono
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
s : Set E
𝕜' : Type u_3
inst_4 : Semiring 𝕜'
inst_5 : SMul 𝕜 𝕜'
inst_6 : Module 𝕜' E
inst_7 : IsScalarTower 𝕜 𝕜' E
hs : UniqueDiffOn 𝕜 s
⊢ UniqueDiffOn 𝕜' s

Tactic:
fun x hx ↦ (hs x hx).mono_field

Premises used: UniqueDiffOn, UniqueDiffWithinAt.mono_field
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
⊢ UniqueDiffWithinAt 𝕜 (closure[inst_3] s) x ↔ UniqueDiffWithinAt 𝕜 s x

Tactic:
simp [uniqueDiffWithinAt_iff]

Premises used: uniqueDiffWithinAt_iff
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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 t : Set E
inst_4 : ContinuousAdd E
inst_5 : ContinuousConstSMul 𝕜 E
h : UniqueDiffWithinAt 𝕜 s x
st : s ⊆ closure[inst_3] t
⊢ UniqueDiffWithinAt 𝕜 t x

Tactic:
(h.mono st).of_closure

Premises used: UniqueDiffWithinAt.of_closure, UniqueDiffWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
rw : Dense (↑(Submodule.span 𝕜 univ) : Set E) ∧ Membership.mem (γ := Set E) (closure[inst_3] univ) x
⊢ UniqueDiffWithinAt 𝕜 univ x

Tactic:
rw [uniqueDiffWithinAt_iff, tangentConeAt_univ]

Premises used: tangentConeAt_univ, uniqueDiffWithinAt_iff
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
⊢ Dense (↑(Submodule.span 𝕜 univ) : Set E) ∧ Membership.mem (γ := Set E) (closure[inst_3] univ) x

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
⊢ UniqueDiffOn.{u_1, u_2} 𝕜 (E := E) univ

Tactic:
fun _ _ => uniqueDiffWithinAt_univ

Premises used: UniqueDiffOn, uniqueDiffWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
s : Set E
inst_7 : ContinuousAdd E
h : s ∈ 𝓝 x
⊢ UniqueDiffWithinAt 𝕜 s x

Tactic:
simpa only [univ_inter] using uniqueDiffWithinAt_univ.inter h

Premises used: Set.univ_inter, UniqueDiffWithinAt.inter, uniqueDiffWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
s : Set E
inst_7 : ContinuousAdd E
hs : IsOpen[inst_3] s
xs : x ∈ s
⊢ UniqueDiffWithinAt 𝕜 s x

Tactic:
uniqueDiffWithinAt_of_mem_nhds (IsOpen.mem_nhds hs xs)

Premises used: uniqueDiffWithinAt_of_mem_nhds, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Calculus.TangentCone.Basic
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
s : Set E
inst_7 : ContinuousAdd E
hs : IsOpen[inst_3] s
⊢ UniqueDiffOn 𝕜 s

Tactic:
fun _ hx => IsOpen.uniqueDiffWithinAt hs hx

Premises used: UniqueDiffOn, IsOpen.uniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.TangentCone.Defs
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))
⊢ (l ⊓ 𝓟 {x_1 : α | x + d x_1 ∈ s}).NeBot

Tactic:
rw [frequently_iff_neBot] at hds

Premises used: Filter.frequently_iff_neBot
-- Module: Mathlib.Analysis.Calculus.TangentCone.Defs
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))
hds₁ : (l ⊓ 𝓟 {x_1 : α | x + d x_1 ∈ s}).NeBot
⊢ Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)

Tactic:
rw [frequently_iff_neBot] at hds

Premises used: Filter.frequently_iff_neBot
-- Module: Mathlib.Analysis.Calculus.TangentCone.Defs
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))
hds₁ : (l ⊓ 𝓟 {x_1 : α | x + d x_1 ∈ s}).NeBot
hcd₁ : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)
⊢ 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))

Tactic:
rw [frequently_iff_neBot] at hds

Premises used: Filter.frequently_iff_neBot