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
u v : V
p : P
simp_rw :
  Eq.{u_3 + 1} (α := Filter P) (map ((fun (b : P) ↦ u +ᵥ b) ∘ fun (x : V) ↦ x +ᵥ p) (asymptoticNhds k V v))
    (map (fun (x : V) ↦ x +ᵥ u +ᵥ p) (asymptoticNhds k V v))
⊢ u +ᵥ HVAdd.hVAdd (β := Filter P) (asymptoticNhds k V v) (pure p) = asymptoticNhds k P v

Tactic:
simp_rw [← asymptoticNhds_vadd_pure v (u +ᵥ p), vadd_pure, ← Filter.map_vadd, map_map]

Premises used: AffineSpace.asymptoticNhds_vadd_pure, Filter.map_map, Filter.vadd_pure, HVAdd.hVAdd, Filter.map_vadd
-- 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
u v : V
p : P
e_m : ∀ (v : V), ((fun (b : P) ↦ u +ᵥ b) ∘ fun (x : V) ↦ x +ᵥ p) v = v +ᵥ u +ᵥ p
⊢ Eq.{u_3 + 1} (α := Filter P) (map ((fun (b : P) ↦ u +ᵥ b) ∘ fun (x : V) ↦ x +ᵥ p) (asymptoticNhds k V v))
    (map (fun (x : V) ↦ x +ᵥ u +ᵥ p) (asymptoticNhds k V v))

Tactic:
congr with 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
u v_1 : V
p : P
v : V
⊢ ((fun (b : P) ↦ u +ᵥ b) ∘ fun (x : V) ↦ x +ᵥ p) v = v +ᵥ u +ᵥ p

Tactic:
vadd_comm u v p

Premises used: VAddCommClass.vadd_comm
-- 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
u v_1 : V
p : P
v : V
⊢ ((fun (b : P) ↦ u +ᵥ b) ∘ fun (x : V) ↦ x +ᵥ p) v = v +ᵥ u +ᵥ p

Tactic:
exact vadd_comm u v p

Premises used: VAddCommClass.vadd_comm
-- 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
α : Type u_4
l : Filter α
f : α → V
v : V
p : P
hf : Tendsto f l (asymptoticNhds k V v)
rw : Tendsto.{u_4, u_3} (β := P) (fun (x : α) ↦ f x +ᵥ p) l (map (fun (x : V) ↦ x +ᵥ p) (asymptoticNhds k V v))
rw₁ : P
⊢ Tendsto (fun (x : α) ↦ f x +ᵥ p) l (asymptoticNhds k P v)

Tactic:
rw [← asymptoticNhds_vadd_pure, vadd_pure]

Premises used: AffineSpace.asymptoticNhds_vadd_pure, Filter.vadd_pure
-- 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
α : Type u_4
l : Filter α
f : α → V
v : V
p : P
hf : Tendsto f l (asymptoticNhds k V v)
⊢ Tendsto.{u_4, u_3} (β := P) (fun (x : α) ↦ f x +ᵥ p) l (map (fun (x : V) ↦ x +ᵥ p) (asymptoticNhds k V v))

Tactic:
tendsto_map.comp hf

Premises used: Filter.tendsto_map, Filter.Tendsto.comp
-- 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
α : Type u_4
l : Filter α
f : α → P
v u : V
hf : Tendsto f l (asymptoticNhds k P v)
rw : Tendsto (β := P) (fun (x : α) ↦ u +ᵥ f x) l (map (fun (b : P) ↦ u +ᵥ b) (asymptoticNhds k P v))
⊢ Tendsto (fun (x : α) ↦ u +ᵥ f x) l (asymptoticNhds k P v)

Tactic:
rw [← vadd_asymptoticNhds u, ← Filter.map_vadd]

Premises used: AffineSpace.vadd_asymptoticNhds, Filter.map_vadd
-- 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
α : Type u_4
l : Filter α
f : α → P
v u : V
hf : Tendsto f l (asymptoticNhds k P v)
⊢ Tendsto (β := P) (fun (x : α) ↦ u +ᵥ f x) l (map (fun (b : P) ↦ u +ᵥ b) (asymptoticNhds k P v))

Tactic:
tendsto_map.comp hf

Premises used: Filter.tendsto_map, Filter.Tendsto.comp
-- 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
α : Type u_4
l : Filter α
f : α → P
v u : V
hf : Tendsto f l (asymptoticNhds k P v)
⊢ Tendsto (β := P) (fun (x : α) ↦ u +ᵥ f x) l (map (fun (b : P) ↦ u +ᵥ b) (asymptoticNhds k P v))

Tactic:
exact tendsto_map.comp hf

Premises used: Filter.tendsto_map, Filter.Tendsto.comp
-- 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
v : V
unfold :
  ⨆ (p : V), HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)
⊢ asymptoticNhds k V v = HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)

Tactic:
unfold asymptoticNhds

Premises used: AffineSpace.asymptoticNhds
-- 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
v : V
a :
  ⨆ (p : V), HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p) ≤
    HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)
a₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v) ≤
    ⨆ (p : V), HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)
⊢ ⨆ (p : V), HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
v : V
⊢ ⨆ (p : V), HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p) ≤
    HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)

Tactic:
iSup_le fun u => ?_

Premises used: Set.Mem, iSup_le
-- 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
v : V
a :
  ∀ (u : V),
    HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure u) ≤
      HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)
⊢ ⨆ (p : V), HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p) ≤
    HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)

Tactic:
refine iSup_le fun u => ?_

Premises used: iSup_le
-- 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
v u : V
a :
  LE.le.{u_2} (α := Filter V) (map (fun (p : k × V) ↦ p.1 • p.2 + u) (SProd.sprod (α := Filter k) atTop (𝓝 v)))
    (map (fun (p : k × V) ↦ p.1 • p.2) (SProd.sprod (α := Filter k) atTop (𝓝 v)))
⊢ HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure u) ≤
    HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)

Tactic:
simp_rw [vadd_eq_add, add_pure, ← map₂_smul, map_map₂, ← map_prod_eq_map₂]

Premises used: Filter.add_pure, Filter.map₂_smul, Filter.map_prod_eq_map₂, vadd_eq_add, Filter.map_map₂
-- 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
v u : V
h :
  ∀ (a : k × V) (h : a.1 ≠ 0),
    a.1 • a.2 + u =
      Function.comp (β := k × V) (Function.uncurry fun (x1 : k) (x2 : V) ↦ x1 • x2)
        (fun (x : k × V) ↦ (x.1, x.2 + x.1⁻¹ • u)) a
⊢ (SProd.sprod (α := Filter k) atTop (𝓝 v)).EventuallyEq (β := V) (fun (x : k × V) ↦ x.1 • x.2 + u)
    (Function.comp (β := k × V) (Function.uncurry fun (x1 : k) (x2 : V) ↦ x1 • x2) fun (x : k × V) ↦
      (x.1, x.2 + x.1⁻¹ • u))

Tactic:
filter_upwards [tendsto_fst.eventually (eventually_ne_atTop 0)] with _ h

Premises used: Filter.eventually_ne_atTop, Filter.Tendsto.eventually, OfNat.ofNat, Filter.tendsto_fst
-- 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
v u : V
a : k × V
h : a.1 ≠ 0
⊢ a.1 • a.2 + u =
    Function.comp (β := k × V) (Function.uncurry fun (x1 : k) (x2 : V) ↦ x1 • x2)
      (fun (x : k × V) ↦ (x.1, x.2 + x.1⁻¹ • u)) a

Tactic:
simp [h]
-- 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
v u : V
⊢ (SProd.sprod (α := Filter k) atTop (𝓝 v)).EventuallyEq (β := V) (fun (x : k × V) ↦ x.1 • x.2 + u)
    (Function.comp (β := k × V) (Function.uncurry fun (x1 : k) (x2 : V) ↦ x1 • x2) fun (x : k × V) ↦
      (x.1, x.2 + x.1⁻¹ • u))

Tactic:
have : (fun x : k × V => x.1 • x.2 + u) =ᶠ[atTop ×ˢ 𝓝 v]
        (Function.uncurry (· • ·)) ∘ (fun x : k × V => (x.1, x.2 + x.1⁻¹ • u)) := by
      filter_upwards [tendsto_fst.eventually (eventually_ne_atTop 0)] with _ h
      simp [h]
-- 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
v u : V
this :
  (SProd.sprod (α := Filter k) atTop (𝓝 v)).EventuallyEq (β := V) (fun (x : k × V) ↦ x.1 • x.2 + u)
    (Function.comp (β := k × V) (Function.uncurry fun (x1 : k) (x2 : V) ↦ x1 • x2) fun (x : k × V) ↦
      (x.1, x.2 + x.1⁻¹ • u))
a :
  LE.le.{u_2} (α := Filter V)
    (map (α := k × V) (Function.uncurry fun (x1 : k) (x2 : V) ↦ x1 • x2)
      (map (fun (x : k × V) ↦ (x.1, x.2 + x.1⁻¹ • u)) (SProd.sprod (α := Filter k) atTop (𝓝 v))))
    (map (fun (p : k × V) ↦ p.1 • p.2) (SProd.sprod (α := Filter k) atTop (𝓝 v)))
⊢ LE.le.{u_2} (α := Filter V) (map (fun (p : k × V) ↦ p.1 • p.2 + u) (SProd.sprod (α := Filter k) atTop (𝓝 v)))
    (map (fun (p : k × V) ↦ p.1 • p.2) (SProd.sprod (α := Filter k) atTop (𝓝 v)))

Tactic:
rw [map_congr this, ← map_map]

Premises used: Filter.map_congr, Filter.map_map
-- 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
v u : V
this :
  (SProd.sprod (α := Filter k) atTop (𝓝 v)).EventuallyEq (β := V) (fun (x : k × V) ↦ x.1 • x.2 + u)
    (Function.comp (β := k × V) (Function.uncurry fun (x1 : k) (x2 : V) ↦ x1 • x2) fun (x : k × V) ↦
      (x.1, x.2 + x.1⁻¹ • u))
a :
  map (fun (x : k × V) ↦ (x.1, x.2 + x.1⁻¹ • u)) (SProd.sprod (α := Filter k) atTop (𝓝 v)) ≤
    SProd.sprod (α := Filter k) atTop (𝓝 v)
⊢ LE.le.{u_2} (α := Filter V)
    (map (α := k × V) (Function.uncurry fun (x1 : k) (x2 : V) ↦ x1 • x2)
      (map (fun (x : k × V) ↦ (x.1, x.2 + x.1⁻¹ • u)) (SProd.sprod (α := Filter k) atTop (𝓝 v))))
    (map (fun (p : k × V) ↦ p.1 • p.2) (SProd.sprod (α := Filter k) atTop (𝓝 v)))

Tactic:
apply map_mono

Premises used: Filter.map_mono
-- 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
v u : V
this :
  (SProd.sprod (α := Filter k) atTop (𝓝 v)).EventuallyEq (β := V) (fun (x : k × V) ↦ x.1 • x.2 + u)
    (Function.comp (β := k × V) (Function.uncurry fun (x1 : k) (x2 : V) ↦ x1 • x2) fun (x : k × V) ↦
      (x.1, x.2 + x.1⁻¹ • u))
⊢ Tendsto (fun (x : k × V) ↦ (x.1, x.2 + x.1⁻¹ • u)) (SProd.sprod (α := Filter k) atTop (𝓝 v))
    (SProd.sprod (α := Filter k) atTop (𝓝 (v + HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 u)))

Tactic:
have : Tendsto (fun x : k × V => (x.1, x.2 + x.1⁻¹ • u)) (atTop ×ˢ 𝓝 v) _ :=
      tendsto_fst.prodMk <| tendsto_snd.add <| tendsto_fst.inv_tendsto_atTop.smul_const 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
v u : V
this_1 :
  (SProd.sprod (α := Filter k) atTop (𝓝 v)).EventuallyEq (β := V) (fun (x : k × V) ↦ x.1 • x.2 + u)
    (Function.comp (β := k × V) (Function.uncurry fun (x1 : k) (x2 : V) ↦ x1 • x2) fun (x : k × V) ↦
      (x.1, x.2 + x.1⁻¹ • u))
this :
  Tendsto (fun (x : k × V) ↦ (x.1, x.2 + x.1⁻¹ • u)) (SProd.sprod (α := Filter k) atTop (𝓝 v))
    (SProd.sprod (α := Filter k) atTop (𝓝 (v + HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 u)))
⊢ map (fun (x : k × V) ↦ (x.1, x.2 + x.1⁻¹ • u)) (SProd.sprod (α := Filter k) atTop (𝓝 v)) ≤
    SProd.sprod (α := Filter k) atTop (𝓝 v)

Tactic:
simpa
-- 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
v : V
a :
  HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v) ≤
    HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure 0)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v) ≤
    ⨆ (p : V), HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)

Tactic:
apply (le_iSup _ 0).trans'

Premises used: le_iSup, OfNat.ofNat, LE.le.trans'
-- 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
v : V
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v) ≤
    HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure 0)

Tactic:
simp
-- 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
v : V
p : P
rw : asymptoticNhds k P v = HVAdd.hVAdd (β := Filter P) (asymptoticNhds k V v) (pure p)
rw₁ rw₂ : asymptoticNhds k P v = asymptoticNhds k P v
⊢ asymptoticNhds k P v = HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)

Tactic:
rw [← asymptoticNhds_eq_smul, asymptoticNhds_vadd_pure]

Premises used: AffineSpace.asymptoticNhds_vadd_pure, AffineSpace.asymptoticNhds_eq_smul
-- 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
α : Type u_4
l : Filter α
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
v : V
have : ∀ (p : P), (asymptoticNhds k P v).NeBot
⊢ (asymptoticNhds k P v).NeBot

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
α : Type u_4
l : Filter α
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
v : V
p : P
rw : (HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)).NeBot
⊢ (asymptoticNhds k P v).NeBot

Tactic:
rw [asymptoticNhds_eq_smul_vadd v p]

Premises used: AffineSpace.asymptoticNhds_eq_smul_vadd
-- 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
α : Type u_4
l : Filter α
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
v : V
p : P
⊢ (HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)).NeBot

Tactic:
infer_instance
-- 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
rw : ∀ (i : V), pure i ≤ asymptoticNhds k V 0
⊢ asymptoticNhds k V 0 = ⊤

Tactic:
rw [← top_le_iff, ← iSup_pure_eq_top, iSup_le_iff]

Premises used: Filter.iSup_pure_eq_top, top_le_iff, iSup_le_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
v : V
rw : map (fun (x : k) ↦ v) atTop ≤ asymptoticNhds k V 0
⊢ pure v ≤ asymptoticNhds k V 0

Tactic:
rw [← map_const (f := atTop (α := k))]

Premises used: Filter.map_const
-- 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
v : V
h :
  ∀ (a : k) (h : a ≠ 0),
    v = Function.comp (β := k × V) (Function.uncurry fun (x1 : k) (x2 : V) ↦ x1 • x2) (fun (c : k) ↦ (c, c⁻¹ • v)) a
⊢ EventuallyEq.{u_1, u_2} (β := V) atTop (fun (x : k) ↦ v)
    (Function.comp (β := k × V) (Function.uncurry fun (x1 : k) (x2 : V) ↦ x1 • x2) fun (c : k) ↦ (c, c⁻¹ • v))

Tactic:
filter_upwards [eventually_ne_atTop 0] with _ h

Premises used: Filter.eventually_ne_atTop, OfNat.ofNat
-- 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
v : V
a : k
h : a ≠ 0
⊢ v = Function.comp (β := k × V) (Function.uncurry fun (x1 : k) (x2 : V) ↦ x1 • x2) (fun (c : k) ↦ (c, c⁻¹ • v)) a

Tactic:
simp [h]
-- 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
v : V
⊢ EventuallyEq.{u_1, u_2} (β := V) atTop (fun (x : k) ↦ v)
    (Function.comp (β := k × V) (Function.uncurry fun (x1 : k) (x2 : V) ↦ x1 • x2) fun (c : k) ↦ (c, c⁻¹ • v))

Tactic:
have : (fun _ => v) =ᶠ[atTop (α := k)]
      (Function.uncurry (· • ·)) ∘ (fun c => (c, c⁻¹ • v)) := by
    filter_upwards [eventually_ne_atTop 0] with _ h
    simp [h]
-- 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
v : V
this :
  EventuallyEq.{u_1, u_2} (β := V) atTop (fun (x : k) ↦ v)
    (Function.comp (β := k × V) (Function.uncurry fun (x1 : k) (x2 : V) ↦ x1 • x2) fun (c : k) ↦ (c, c⁻¹ • v))
rw :
  LE.le.{u_2} (α := Filter V)
    (map (α := k × V) (Function.uncurry fun (x1 : k) (x2 : V) ↦ x1 • x2) (map (fun (c : k) ↦ (c, c⁻¹ • v)) atTop))
    (map (fun (p : k × V) ↦ p.1 • p.2) (SProd.sprod (α := Filter k) (β := Filter V) atTop (𝓝 0)))
⊢ map (fun (x : k) ↦ v) atTop ≤ asymptoticNhds k V 0

Tactic:
rw [map_congr this, ← map_map, asymptoticNhds_eq_smul, ← map₂_smul, ← map_prod_eq_map₂]

Premises used: Filter.map₂_smul, Filter.map_congr, Filter.map_map, Filter.map_prod_eq_map₂, 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
v : V
this :
  EventuallyEq.{u_1, u_2} (β := V) atTop (fun (x : k) ↦ v)
    (Function.comp (β := k × V) (Function.uncurry fun (x1 : k) (x2 : V) ↦ x1 • x2) fun (c : k) ↦ (c, c⁻¹ • v))
a : map (fun (c : k) ↦ (c, c⁻¹ • v)) atTop ≤ SProd.sprod (α := Filter k) (β := Filter V) atTop (𝓝 0)
⊢ LE.le.{u_2} (α := Filter V)
    (map (α := k × V) (Function.uncurry fun (x1 : k) (x2 : V) ↦ x1 • x2) (map (fun (c : k) ↦ (c, c⁻¹ • v)) atTop))
    (map (fun (p : k × V) ↦ p.1 • p.2) (SProd.sprod (α := Filter k) (β := Filter V) atTop (𝓝 0)))

Tactic:
apply map_mono

Premises used: Filter.map_mono