awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : ∃ᶠ (n : α) in l, x + d n ∈ s
hds : (l ⊓ 𝓟 {x_1 : α | x + d x_1 ∈ s}).NeBot
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))
rw :
  Membership.mem (γ := Set E)
    {y : E |
      ClusterPt y (HSMul.hSMul.{u, v, v} (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))}
    y
⊢ y ∈ tangentConeAt R s x

Tactic:
rw [tangentConeAt_def]

Premises used: tangentConeAt_def
-- 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_1 : ∃ᶠ (n : α) in l, x + d n ∈ s
hds : (l ⊓ 𝓟 {x_1 : α | x + d x_1 ∈ s}).NeBot
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))
⊢ Membership.mem (γ := Set E)
    {y : E |
      ClusterPt y (HSMul.hSMul.{u, v, v} (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))}
    y

Tactic:
ClusterPt.mono (hcd.mono_left inf_le_left).mapClusterPt this

Premises used: Filter.Tendsto.mapClusterPt, ClusterPt.mono, Set.Mem, setOf, ClusterPt, Filter.Tendsto.mono_left, inf_le_left
-- 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_1 : ∃ᶠ (n : α) in l, x + d n ∈ s
hds : (l ⊓ 𝓟 {x_1 : α | x + d x_1 ∈ s}).NeBot
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))
⊢ Membership.mem (γ := Set E)
    {y : E |
      ClusterPt y (HSMul.hSMul.{u, v, v} (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))}
    y

Tactic:
exact ClusterPt.mono (hcd.mono_left inf_le_left).mapClusterPt this

Premises used: Filter.Tendsto.mapClusterPt, ClusterPt.mono, Filter.Tendsto.mono_left, inf_le_left
-- 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)
suffices :
  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

Tactic:
suffices Tendsto (fun n ↦ c n • d n) (l ⊓ 𝓟 {y | x + d y ∈ s}) (⊤ • 𝓝[(x + ·) ⁻¹' s] 0) by
    rw [frequently_iff_neBot] at hds
    rw [tangentConeAt_def]
    exact ClusterPt.mono (hcd.mono_left inf_le_left).mapClusterPt this
-- 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)
rw :
  Tendsto.{u_1, v} (β := E) (fun (n : α) ↦ c n • d n) (l ⊓ 𝓟 {y : α | x + d y ∈ s})
    (map (fun (p : R × E) ↦ p.1 • p.2)
      (SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)))
⊢ 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 [← map₂_smul, ← map_prod_eq_map₂]

Premises used: Filter.map₂_smul, Filter.map_prod_eq_map₂
-- 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)
⊢ Tendsto.{u_1, v} (β := E) (fun (n : α) ↦ c n • d n) (l ⊓ 𝓟 {y : α | x + d y ∈ s})
    (map (fun (p : R × E) ↦ p.1 • p.2)
      (SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)))

Tactic:
tendsto_map.comp (tendsto_top.prodMk (tendsto_nhdsWithin_iff.mpr ⟨?_, ?_⟩))

Premises used: Iff.mpr, tendsto_nhdsWithin_iff, Filter.tendsto_map, Filter.tendsto_top, And.intro, Filter.Tendsto.prodMk, Filter.Tendsto.comp
-- 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)
refine_1 : Tendsto d (l ⊓ 𝓟 {y : α | x + d y ∈ s}) (𝓝 0)
refine_2 :
  ∀ᶠ (n : α) in l ⊓ 𝓟 {y : α | x + d y ∈ s}, Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' s) (d n)
⊢ Tendsto.{u_1, v} (β := E) (fun (n : α) ↦ c n • d n) (l ⊓ 𝓟 {y : α | x + d y ∈ s})
    (map (fun (p : R × E) ↦ p.1 • p.2)
      (SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)))

Tactic:
refine tendsto_map.comp (tendsto_top.prodMk (tendsto_nhdsWithin_iff.mpr ⟨?_, ?_⟩))

Premises used: Iff.mpr, tendsto_nhdsWithin_iff, Filter.tendsto_map, Filter.tendsto_top, And.intro, Filter.Tendsto.prodMk, Filter.Tendsto.comp
-- 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)
⊢ Tendsto d (l ⊓ 𝓟 {y : α | x + d y ∈ s}) (𝓝 0)

Tactic:
hd₀.mono_left inf_le_left

Premises used: Filter.Tendsto.mono_left, inf_le_left
-- 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)
⊢ Tendsto d (l ⊓ 𝓟 {y : α | x + d y ∈ s}) (𝓝 0)

Tactic:
exact hd₀.mono_left inf_le_left

Premises used: Filter.Tendsto.mono_left, inf_le_left
-- 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)
⊢ ∀ᶠ (n : α) in l ⊓ 𝓟 {y : α | x + d y ∈ s}, Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' s) (d n)

Tactic:
simp [eventually_inf_principal]

Premises used: Filter.eventually_inf_principal
-- 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 α
inst_3 : l.NeBot
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)
⊢ y ∈ tangentConeAt R s x

Tactic:
mem_tangentConeAt_of_frequently l c d hd₀ hds.frequently hcd

Premises used: mem_tangentConeAt_of_frequently, Filter.Eventually.frequently
-- 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
h : y ∈ tangentConeAt R s x
⊢ (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot

Tactic:
rw [tangentConeAt, mem_setOf, ← map₂_smul, ← map_prod_eq_map₂, ClusterPt,
    ← neBot_inf_comap_iff_map'] at h

Premises used: Filter.map₂_smul, Set.mem_setOf, Filter.neBot_inf_comap_iff_map', Filter.map_prod_eq_map₂, ClusterPt, tangentConeAt
-- 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
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
⊢ ∃ (α : Type (max u v)) (l : Filter α) (_ : l.NeBot) (c : α → R) (d : α → E),
    Tendsto d l (𝓝 0) ∧ (∀ᶠ (n : α) in l, x + d n ∈ s) ∧ Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)

Tactic:
⟨R × E, _, h, Prod.fst, Prod.snd, ?_, ?_, ?_⟩

Premises used: Prod.fst, And.intro, Exists.intro, Prod, Prod.snd
-- 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
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
refine_1 :
  Tendsto Prod.snd
    (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
    (𝓝 0)
refine_2 :
  ∀ᶠ (n : R × E) in
    comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0),
    x + n.2 ∈ s
refine_3 :
  Tendsto (fun (n : R × E) ↦ n.1 • n.2)
    (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
    (𝓝 y)
⊢ ∃ (α : Type (max u v)) (l : Filter α) (_ : l.NeBot) (c : α → R) (d : α → E),
    Tendsto d l (𝓝 0) ∧ (∀ᶠ (n : α) in l, x + d n ∈ s) ∧ Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 y)

Tactic:
refine ⟨R × E, _, h, Prod.fst, Prod.snd, ?_, ?_, ?_⟩
-- 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
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
⊢ Tendsto Prod.snd
    (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
    (𝓝 0)

Tactic:
(tendsto_snd (f := ⊤)).mono_left <| inf_le_right.trans <| ?_

Premises used: inf_le_right, Filter.Tendsto.mono_left, LE.le.trans, Filter.tendsto_snd
-- 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
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
refine_1 :
  SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) ≤
    SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝 0)
⊢ Tendsto Prod.snd
    (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
    (𝓝 0)

Tactic:
refine (tendsto_snd (f := ⊤)).mono_left <| inf_le_right.trans <| ?_

Premises used: inf_le_right, Filter.Tendsto.mono_left, LE.le.trans, Filter.tendsto_snd
-- 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
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
refine_1 : LE.le (α := Filter E) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) (𝓝 0)
⊢ SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) ≤
    SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝 0)

Tactic:
gcongr
-- 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
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
⊢ LE.le (α := Filter E) (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0) (𝓝 0)

Tactic:
apply nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds
-- 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
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
⊢ ∀ᶠ (n : R × E) in
    comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0),
    x + n.2 ∈ s

Tactic:
.filter_mono inf_le_right ?_

Premises used: Filter.Eventually.filter_mono, inf_le_right
-- 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
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
refine_2 :
  ∀ᶠ (x_1 : R × E) in SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0),
    x + x_1.2 ∈ s
⊢ ∀ᶠ (n : R × E) in
    comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0),
    x + n.2 ∈ s

Tactic:
refine .filter_mono inf_le_right ?_
-- 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
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
refine_2 : ∀ᶠ (b : E) in 𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0, ∀ (a : R × E), a.2 = b → x + a.2 ∈ s
⊢ ∀ᶠ (x_1 : R × E) in SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0),
    x + x_1.2 ∈ s

Tactic:
rw [top_prod, eventually_comap]

Premises used: Filter.top_prod, Filter.eventually_comap
-- 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
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
h₁ :
  ∀ (a : E),
    Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' s) a → ∀ (a_2 : R × E), a_2.2 = a → x + a_2.2 ∈ s
⊢ ∀ᶠ (b : E) in 𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0, ∀ (a : R × E), a.2 = b → x + a.2 ∈ s

Tactic:
filter_upwards [eventually_mem_nhdsWithin]

Premises used: eventually_mem_nhdsWithin
-- 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
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
⊢ ∀ (a : E),
    Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' s) a → ∀ (a_2 : R × E), a_2.2 = a → x + a_2.2 ∈ s

Tactic:
simp +contextual
-- 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
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
⊢ Tendsto (fun (n : R × E) ↦ n.1 • n.2)
    (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
    (𝓝 y)

Tactic:
tendsto_comap.mono_left inf_le_left

Premises used: Filter.tendsto_comap, Filter.Tendsto.mono_left, inf_le_left
-- 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
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
⊢ Tendsto (fun (n : R × E) ↦ n.1 • n.2)
    (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
    (𝓝 y)

Tactic:
exact tendsto_comap.mono_left inf_le_left

Premises used: Filter.tendsto_comap, Filter.Tendsto.mono_left, inf_le_left
-- Module: Mathlib.Analysis.Calculus.TangentCone.Defs
Goal:
R : Type u
E : Type v
inst : Semiring R
inst_1 : AddCommGroup E
inst_2 : Module R E
inst_3 : TopologicalSpace E
s : Set E
x : E
hs : UniqueDiffOn R s
h : x ∈ s
⊢ UniqueDiffWithinAt R s x

Tactic:
hs x h
-- Module: Mathlib.Analysis.Calculus.TangentCone.DimOne
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
⊢ tangentConeAt 𝕜 s x = univ

Tactic:
eq_univ_of_forall fun y ↦ ?_

Premises used: Set.eq_univ_of_forall
-- Module: Mathlib.Analysis.Calculus.TangentCone.DimOne
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
refine : ∀ (y : 𝕜), y ∈ tangentConeAt 𝕜 s x
⊢ tangentConeAt 𝕜 s x = univ

Tactic:
refine eq_univ_of_forall fun y ↦ ?_

Premises used: Set.eq_univ_of_forall
-- Module: Mathlib.Analysis.Calculus.TangentCone.DimOne
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
hd₀ : Tendsto (β := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (𝓝[≠] x) (𝓝 0)
hds : ∃ᶠ (n : 𝕜) in 𝓝[≠] x, x + (n - x) ∈ s
hcd : Tendsto (fun (n : 𝕜) ↦ (y / (n - x)) • (n - x)) (𝓝[≠] x) (𝓝 y)
⊢ y ∈ tangentConeAt 𝕜 s x

Tactic:
apply mem_tangentConeAt_of_frequently (𝓝[≠] x) (fun z ↦ y / (z - x)) (· - x)

Premises used: Compl.compl, nhdsWithin, mem_tangentConeAt_of_frequently, HSub.hSub, HDiv.hDiv, Singleton.singleton
-- Module: Mathlib.Analysis.Calculus.TangentCone.DimOne
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun (x_1 : 𝕜) ↦ x_1 - x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.TangentCone.DimOne
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
⊢ x - x = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.TangentCone.DimOne
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
⊢ Tendsto (β := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) (𝓝[≠] x) (𝓝 0)

Tactic:
exact Continuous.tendsto' (by fun_prop) _ _ (by simp) |>.mono_left inf_le_left

Premises used: Filter.Tendsto.mono_left, inf_le_left, Continuous.tendsto'
-- Module: Mathlib.Analysis.Calculus.TangentCone.DimOne
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
⊢ ∃ᶠ (n : 𝕜) in 𝓝[≠] x, x + (n - x) ∈ s

Tactic:
simpa [accPt_iff_frequently_nhdsNE] using hx

Premises used: accPt_iff_frequently_nhdsNE
-- Module: Mathlib.Analysis.Calculus.TangentCone.DimOne
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
hcd : ∀ᶠ (x' : 𝕜) in 𝓝[≠] x, (y / (x' - x)) • (x' - x) = y
⊢ Tendsto (fun (n : 𝕜) ↦ (y / (n - x)) • (n - x)) (𝓝[≠] x) (𝓝 y)

Tactic:
apply tendsto_nhds_of_eventually_eq

Premises used: tendsto_nhds_of_eventually_eq
-- Module: Mathlib.Analysis.Calculus.TangentCone.DimOne
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
⊢ ∀ᶠ (x' : 𝕜) in 𝓝[≠] x, (y / (x' - x)) • (x' - x) = y

Tactic:
eventually_mem_nhdsWithin.mono fun z hz ↦ ?_

Premises used: eventually_mem_nhdsWithin, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Calculus.TangentCone.DimOne
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
hcd : ∀ (z : 𝕜) (hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z), (y / (z - x)) • (z - x) = y
⊢ ∀ᶠ (x' : 𝕜) in 𝓝[≠] x, (y / (x' - x)) • (x' - x) = y

Tactic:
refine eventually_mem_nhdsWithin.mono fun z hz ↦ ?_

Premises used: eventually_mem_nhdsWithin, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Calculus.TangentCone.DimOne
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z
⊢ z - x ≠ 0

Tactic:
simpa [sub_eq_zero] using hz

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.Calculus.TangentCone.DimOne
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z
⊢ z - x ≠ 0

Tactic:
have : z - x ≠ 0 := by simpa [sub_eq_zero] using hz
-- Module: Mathlib.Analysis.Calculus.TangentCone.DimOne
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z
this : z - x ≠ 0
⊢ (y / (z - x)) • (z - x) = y

Tactic:
simp [div_mul_cancel₀ _ this]

Premises used: div_mul_cancel₀
-- Module: Mathlib.Analysis.Calculus.TangentCone.DimOne
Goal:
𝕜 : Type u_1
inst : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
h : AccPt x (𝓟 s)
⊢ Dense (↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) : Set 𝕜)

Tactic:
simp [tangentConeAt_eq_univ h]

Premises used: tangentConeAt_eq_univ
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
inst_6 : DecidableEq ι
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure[inst_3 j] (s j)
rw :
  MapsTo (Pi.single (M := E) i) (tangentConeAt 𝕜 (s i) (x i))
    (tangentConeAt 𝕜 (closure[Pi.topologicalSpace] (Set.pi (α := E) univ s)) x)
⊢ MapsTo (Pi.single (M := E) i) (tangentConeAt 𝕜 (s i) (x i)) (tangentConeAt 𝕜 (Set.pi (α := E) univ s) x)

Tactic:
rw [← tangentConeAt_closure (s := .pi _ _)]

Premises used: tangentConeAt_closure
-- Module: Mathlib.Analysis.Calculus.TangentCone.Pi
Goal:
𝕜 : Type u_1
inst : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (E i)
inst_2 : (i : ι) → Module.{u_1, u_3} 𝕜 (E i)
inst_3 : (i : ι) → TopologicalSpace (E i)
inst_4 : ∀ (i : ι), ContinuousAdd.{u_3} (E i)
inst_5 : ∀ (i : ι), ContinuousConstSMul.{u_1, u_3} 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
inst_6 : DecidableEq ι
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure[inst_3 j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
rcases :
  ∀ (ι_1 : Type (max u_1 u_3)) (l : Filter ι_1) (hl : l.NeBot) (c : ι_1 → 𝕜) (d : ι_1 → E i) (hd₀ : Tendsto d l (𝓝 0))
    (hds : ∀ᶠ (n : ι_1) in l, x i + d n ∈ s i) (hcd : Tendsto (fun (n : ι_1) ↦ c n • d n) l (𝓝 y)),
    Pi.single (M := E) i y ∈ tangentConeAt 𝕜 (closure[Pi.topologicalSpace] (Set.pi (α := E) univ s)) x
⊢ Pi.single (M := E) i y ∈ tangentConeAt 𝕜 (closure[Pi.topologicalSpace] (Set.pi (α := E) univ s)) x

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

Premises used: exists_fun_of_mem_tangentConeAt