awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
⊢ 0 ∈ asymptoticCone k s ↔ s.Nonempty

Tactic:
⟨Function.mtr ?_, fun _ => ?_⟩

Premises used: Function.mtr, Iff.intro
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
refine_1 : ¬s.Nonempty → 0 ∉ asymptoticCone k s
refine_2 : s.Nonempty → 0 ∈ asymptoticCone k s
⊢ 0 ∈ asymptoticCone k s ↔ s.Nonempty

Tactic:
refine ⟨Function.mtr ?_, fun _ => ?_⟩
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
⊢ ¬s.Nonempty → 0 ∉ asymptoticCone k s

Tactic:
simp +contextual [Set.not_nonempty_iff_eq_empty]

Premises used: Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
h : s.Nonempty
⊢ 0 ∈ asymptoticCone k s

Tactic:
simpa [mem_asymptoticCone_iff]

Premises used: mem_asymptoticCone_iff
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
⊢ (asymptoticCone k s).Nonempty ↔ s.Nonempty

Tactic:
⟨Function.mtr ?_, fun h => ⟨0, zero_mem_asymptoticCone.mpr h⟩⟩

Premises used: Iff.mpr, zero_mem_asymptoticCone, Function.mtr, Iff.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
refine : ¬s.Nonempty → ¬(asymptoticCone k s).Nonempty
⊢ (asymptoticCone k s).Nonempty ↔ s.Nonempty

Tactic:
refine ⟨Function.mtr ?_, fun h => ⟨0, zero_mem_asymptoticCone.mpr h⟩⟩
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
⊢ ¬s.Nonempty → ¬(asymptoticCone k s).Nonempty

Tactic:
simp +contextual [Set.not_nonempty_iff_eq_empty]

Premises used: Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
c : k
v : V
hc : 0 ≤ c
h : v ∈ asymptoticCone k s
inl : ∀ (hc : LE.le.{u_1} (α := k) 0 0), HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 v ∈ asymptoticCone k s
inr : ∀ (hc : 0 < c), c • v ∈ asymptoticCone k s
⊢ c • v ∈ asymptoticCone k s

Tactic:
rcases hc.eq_or_lt with rfl | hc

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
v : V
h : v ∈ asymptoticCone k s
hc : LE.le.{u_1} (α := k) 0 0
inl : (asymptoticCone k s).Nonempty
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 v ∈ asymptoticCone k s

Tactic:
rw [zero_smul, zero_mem_asymptoticCone, ← asymptoticCone_nonempty (k := k)]

Premises used: zero_mem_asymptoticCone, zero_smul, asymptoticCone_nonempty
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
v : V
h : v ∈ asymptoticCone k s
hc : LE.le.{u_1} (α := k) 0 0
⊢ (asymptoticCone k s).Nonempty

Tactic:
⟨v, h⟩

Premises used: Set.Nonempty, Exists.intro
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
v : V
h : v ∈ asymptoticCone k s
hc : LE.le.{u_1} (α := k) 0 0
⊢ (asymptoticCone k s).Nonempty

Tactic:
exact ⟨v, h⟩
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
c : k
v : V
hc_1 : 0 ≤ c
h : v ∈ asymptoticCone k s
hc : 0 < c
inr inr₁ inr₂ inr₃ : v ∈ asymptoticCone k s
⊢ c • v ∈ asymptoticCone k s

Tactic:
rwa [smul_mem_asymptoticCone_iff hc]

Premises used: smul_mem_asymptoticCone_iff
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s
h : ∀ (v : V), v ∈ asymptoticCone k s ↔ v ∈ closure[inst_4] s
⊢ asymptoticCone k s = closure[inst_4] s

Tactic:
ext v
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s
v : V
h :
  (∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 ∈ s) ↔
    ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.2 ∈ s
⊢ v ∈ asymptoticCone k s ↔ v ∈ closure[inst_4] s

Tactic:
rw [mem_closure_iff_frequently, ← map_snd_prod (atTop (α := k)) (𝓝 v), frequently_map,
    mem_asymptoticCone_iff, asymptoticNhds_eq_smul, ← map₂_smul, ← map_prod_eq_map₂, frequently_map]

Premises used: Filter.map_snd_prod, Filter.map₂_smul, mem_closure_iff_frequently, nhds, Filter.frequently_map, Filter.atTop, Filter.map_prod_eq_map₂, mem_asymptoticCone_iff, AffineSpace.asymptoticNhds_eq_smul
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s
v : V
h : ∀ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), x.1 • x.2 ∈ s ↔ x.2 ∈ s
⊢ (∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 ∈ s) ↔
    ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.2 ∈ s

Tactic:
apply frequently_congr

Premises used: Filter.frequently_congr
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s
v : V
h : ∀ (c : k) (u : V) (hc : 0 < (c, u).1), (c, u).1 • (c, u).2 ∈ s ↔ (c, u).2 ∈ s
⊢ ∀ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), x.1 • x.2 ∈ s ↔ x.2 ∈ s

Tactic:
filter_upwards [tendsto_fst.eventually (eventually_gt_atTop 0)] with ⟨c, u⟩ hc

Premises used: Filter.Tendsto.eventually, OfNat.ofNat, Filter.tendsto_fst, Filter.eventually_gt_atTop
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s
v : V
c : k
u : V
hc : 0 < (c, u).1
⊢ (c, u).1 • (c, u).2 ∈ s ↔ (c, u).2 ∈ s

Tactic:
⟨fun hu => ?_, hs c hc u⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s
v : V
c : k
u : V
hc : 0 < (c, u).1
h : ∀ (hu : (c, u).1 • (c, u).2 ∈ s), (c, u).2 ∈ s
⊢ (c, u).1 • (c, u).2 ∈ s ↔ (c, u).2 ∈ s

Tactic:
refine ⟨fun hu => ?_, hs c hc u⟩
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s
v : V
c : k
u : V
hc : 0 < (c, u).1
hu : (c, u).1 • (c, u).2 ∈ s
⊢ c⁻¹ • c • u ∈ s

Tactic:
specialize hs c⁻¹ (inv_pos_of_pos hc) (c • u) hu

Premises used: inv_pos_of_pos, Inv.inv, HSMul.hSMul
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
v : V
c : k
u : V
hc : 0 < (c, u).1
hu : (c, u).1 • (c, u).2 ∈ s
hs : c⁻¹ • c • u ∈ s
h h₁ h₂ h₃ : ∀ (hs : u ∈ s), (c, u).2 ∈ s
⊢ (c, u).2 ∈ s

Tactic:
rwa [inv_smul_smul₀ hc.ne'] at hs

Premises used: inv_smul_smul₀, LT.lt.ne'
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Submodule k V
⊢ asymptoticCone k (↑s : Set V) = closure[inst_4] (↑s : Set V)

Tactic:
asymptoticCone_eq_closure_of_forall_smul_mem fun _ _ _ h => s.smul_mem _ h

Premises used: asymptoticCone_eq_closure_of_forall_smul_mem, Submodule.smul_mem
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : AffineSubspace k P
hs : (↑s : Set P).Nonempty
have : ∀ (p : P) (hp : p ∈ (↑s : Set P)), asymptoticCone k (↑s : Set P) = closure[inst_5] (↑s.direction : Set V)
⊢ asymptoticCone k (↑s : Set P) = closure[inst_5] (↑s.direction : Set V)

Tactic:
have ⟨p, hp⟩ := hs
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : AffineSubspace k P
hs : (↑s : Set P).Nonempty
p : P
hp : p ∈ (↑s : Set P)
h : ∀ (v : V), v ∈ asymptoticCone k (↑s : Set P) ↔ v ∈ closure[inst_5] (↑s.direction : Set V)
⊢ asymptoticCone k (↑s : Set P) = closure[inst_5] (↑s.direction : Set V)

Tactic:
ext v
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : AffineSubspace k P
hs : (↑s : Set P).Nonempty
p : P
hp : p ∈ (↑s : Set P)
v : V
h : v ∈ asymptoticCone k (↑s : Set P) ↔ v ∈ asymptoticCone k (↑s.direction : Set V)
h₁ :
  (∃ᶠ (p : P) in asymptoticNhds k P v, p ∈ (↑s : Set P)) ↔
    ∃ᶠ (p : V) in asymptoticNhds k V v, p ∈ (↑s.direction : Set V)
h₂ :
  (∃ᶠ (p : P) in HVAdd.hVAdd (β := Filter P) (asymptoticNhds k V v) (pure p), p ∈ (↑s : Set P)) ↔
    ∃ᶠ (p : V) in asymptoticNhds k V v, p ∈ (↑s.direction : Set V)
h₃ :
  (∃ᶠ (p : P) in map (fun (x : V) ↦ x +ᵥ p) (asymptoticNhds k V v), p ∈ (↑s : Set P)) ↔
    ∃ᶠ (p : V) in asymptoticNhds k V v, p ∈ (↑s.direction : Set V)
h₄ :
  (∃ᶠ (a : V) in asymptoticNhds k V v, a +ᵥ p ∈ (↑s : Set P)) ↔
    ∃ᶠ (p : V) in asymptoticNhds k V v, p ∈ (↑s.direction : Set V)
h₅ : (∃ᶠ (a : V) in asymptoticNhds k V v, a +ᵥ p ∈ s) ↔ ∃ᶠ (p : V) in asymptoticNhds k V v, p ∈ s.direction
⊢ v ∈ asymptoticCone k (↑s : Set P) ↔ v ∈ closure[inst_5] (↑s.direction : Set V)

Tactic:
simp_rw [← asymptoticCone_submodule, mem_asymptoticCone_iff, ← asymptoticNhds_vadd_pure v p,
    vadd_pure, frequently_map, SetLike.mem_coe, s.vadd_mem_iff_mem_direction _ hp]

Premises used: AffineSpace.asymptoticNhds_vadd_pure, Filter.frequently_map, Filter.vadd_pure, SetLike.mem_coe, mem_asymptoticCone_iff, AffineSubspace.vadd_mem_iff_mem_direction, asymptoticCone_submodule
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
rw : asymptoticCone k (↑⊤ : Set P) = Set.univ
rw₁ : closure[inst_5] (↑(AffineSubspace.direction.{u_1, u_2, u_3} (P := P) ⊤) : Set V) = Set.univ
rw₂ : closure[inst_5] (↑⊤ : Set V) = Set.univ
rw₃ : Eq.{u_2 + 1} (α := Set V) (closure[inst_5] Set.univ) Set.univ
rw₄ rw₅ : Eq.{u_2 + 1} (α := Set V) Set.univ Set.univ
⊢ asymptoticCone.{u_1, u_2, u_3} k (P := P) Set.univ = Set.univ

Tactic:
rw [← AffineSubspace.top_coe k, asymptoticCone_affineSubspace Set.univ_nonempty,
    AffineSubspace.direction_top, Submodule.top_coe, closure_univ]

Premises used: asymptoticCone_affineSubspace, AffineSubspace.direction_top, AffineSubspace.top_coe, Submodule.top_coe, closure_univ
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
inst_11 : TopologicalSpace P
inst_12 : IsTopologicalAddTorsor P
s : Set P
h : ∀ (x : V), x ∈ asymptoticCone k (closure[inst_11] s) ↔ x ∈ asymptoticCone k s
⊢ asymptoticCone k (closure[inst_11] s) = asymptoticCone k s

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
inst_11 : TopologicalSpace P
inst_12 : IsTopologicalAddTorsor P
s : Set P
x : V
h : (∃ᶠ (p : P) in asymptoticNhds k P x, p ∈ closure[inst_11] s) ↔ ∃ᶠ (p : P) in asymptoticNhds k P x, p ∈ s
h₁ : (∃ᶠ (p : P) in asymptoticNhds k P x, ∃ᶠ (x : P) in 𝓝 p, x ∈ s) ↔ ∃ᶠ (x : P) in asymptoticNhds k P x, x ∈ s
h₂ : (∃ᶠ (x : P) in (asymptoticNhds k P x).bind 𝓝, x ∈ s) ↔ ∃ᶠ (x : P) in asymptoticNhds k P x, x ∈ s
⊢ x ∈ asymptoticCone k (closure[inst_11] s) ↔ x ∈ asymptoticCone k s

Tactic:
simp_rw [mem_asymptoticCone_iff, mem_closure_iff_frequently, ← frequently_bind,
    asymptoticNhds_bind_nhds]

Premises used: Filter.frequently_bind, mem_closure_iff_frequently, mem_asymptoticCone_iff, AffineSpace.asymptoticNhds_bind_nhds
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
have : ∀ (p : P), IsClosed[inst_5] (asymptoticCone k s)
⊢ IsClosed[inst_5] (asymptoticCone k s)

Tactic:
have ⟨p⟩ : Nonempty P := inferInstance
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
p : P
rw : ∀ (x : V), (∃ᶠ (y : V) in 𝓝 x, y ∈ asymptoticCone k s) → x ∈ asymptoticCone k s
⊢ IsClosed[inst_5] (asymptoticCone k s)

Tactic:
rw [isClosed_iff_frequently]

Premises used: isClosed_iff_frequently
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
p : P
v : V
h : ∃ᶠ (y : V) in 𝓝 v, y ∈ asymptoticCone k s
⊢ ∃ᶠ (p : P) in asymptoticNhds k P v, p ∈ s

Tactic:
simp_rw [mem_asymptoticCone_iff, ← frequently_bind, nhds_bind_asymptoticNhds] at h

Premises used: Filter.frequently_bind, AffineSpace.nhds_bind_asymptoticNhds, mem_asymptoticCone_iff
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
p : P
v : V
h : ∃ᶠ (p : P) in asymptoticNhds k P v, p ∈ s
⊢ v ∈ asymptoticCone k s

Tactic:
h

Premises used: Set.Mem, setOf, Filter.Frequently, asymptoticCone, Not
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
p : P
v : V
h : ∃ᶠ (p : P) in asymptoticNhds k P v, p ∈ s
⊢ v ∈ asymptoticCone k s

Tactic:
exact h
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
h : ∀ (x : V), x ∈ asymptoticCone k (asymptoticCone k s) ↔ x ∈ asymptoticCone k s
⊢ asymptoticCone k (asymptoticCone k s) = asymptoticCone k s

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
x : V
h :
  (∃ᶠ (p : V) in asymptoticNhds k V x, ∃ᶠ (p : P) in asymptoticNhds k P p, p ∈ s) ↔
    ∃ᶠ (p : P) in asymptoticNhds k P x, p ∈ s
h₁ : (∃ᶠ (p : P) in (asymptoticNhds k V x).bind (asymptoticNhds k P), p ∈ s) ↔ ∃ᶠ (p : P) in asymptoticNhds k P x, p ∈ s
⊢ x ∈ asymptoticCone k (asymptoticCone k s) ↔ x ∈ asymptoticCone k s

Tactic:
simp_rw [mem_asymptoticCone_iff, ← Filter.frequently_bind, asymptoticNhds_bind_asymptoticNhds]

Premises used: Filter.frequently_bind, AffineSpace.asymptoticNhds_bind_asymptoticNhds, mem_asymptoticCone_iff
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst_7] s
hc : 0 ≤ c
hv : v ∈ asymptoticCone k s
⊢ c • v +ᵥ p ∈ s

Tactic:
isClosed_iff_frequently.mp hs₂ _ <|
    tendsto_snd (f := atTop (α := k)) |>.const_smul _ |>.vadd_const _ |>.frequently ?_

Premises used: Filter.Tendsto.frequently, Filter.Tendsto.vadd_const, isClosed_iff_frequently, Filter.Tendsto.const_smul, Iff.mp, Filter.tendsto_snd
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst_7] s
hc : 0 ≤ c
hv : v ∈ asymptoticCone k s
refine : ∃ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), c • x.2 +ᵥ p ∈ s
⊢ c • v +ᵥ p ∈ s

Tactic:
refine isClosed_iff_frequently.mp hs₂ _ <|
    tendsto_snd (f := atTop (α := k)) |>.const_smul _ |>.vadd_const _ |>.frequently ?_

Premises used: Filter.Tendsto.frequently, Filter.Tendsto.vadd_const, isClosed_iff_frequently, Filter.Tendsto.const_smul, Iff.mp, Filter.tendsto_snd