awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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
⊢ 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)
have 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)))
Tactic: simp_rw [vadd_eq_add, add_pure, ← map₂_smul, map_map₂, ← map_prod_eq_map₂]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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))
have 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
Tactic: filter_upwards [tendsto_fst.eventually (eventually_ne_atTop 0)] with _ h
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (hypothesis)
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
⊢ 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)))
have 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))
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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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))
⊢ 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)))
have 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)))
Tactic: rw [map_congr this, ← map_map]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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))
⊢ 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)))
have 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)
Tactic: apply map_mono
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (hypothesis)
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))
⊢ map (fun (x : k × V) ↦ (x.1, x.2 + x.1⁻¹ • u)) (SProd.sprod (α := Filter k) atTop (𝓝 v)) ≤
    SProd.sprod (α := Filter k) atTop (𝓝 v)
have 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)))
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
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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) ≤
    ⨆ (p : V), HVAdd.hVAdd (β := Filter V) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)
have 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)
Tactic: apply (le_iSup _ 0).trans'
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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
⊢ asymptoticNhds k P v = HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)
have rw : asymptoticNhds k P v = HVAdd.hVAdd (β := Filter P) (asymptoticNhds k V v) (pure p)
Tactic: rw [← asymptoticNhds_eq_smul, asymptoticNhds_vadd_pure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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)
⊢ asymptoticNhds k P v = HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)
have rw₁ : asymptoticNhds k P v = asymptoticNhds k P v
Tactic: rw [← asymptoticNhds_eq_smul, asymptoticNhds_vadd_pure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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
⊢ (asymptoticNhds k P v).NeBot
have have : ∀ (p : P), (asymptoticNhds k P v).NeBot
Tactic: have ⟨p⟩ : Nonempty P := inferInstance
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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
⊢ (asymptoticNhds k P v).NeBot
have rw : (HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)).NeBot
Tactic: rw [asymptoticNhds_eq_smul_vadd v p]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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
⊢ asymptoticNhds k V 0 = ⊤
have rw : ∀ (i : V), pure i ≤ asymptoticNhds k V 0
Tactic: rw [← top_le_iff, ← iSup_pure_eq_top, iSup_le_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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
⊢ pure v ≤ asymptoticNhds k V 0
have rw : map (fun (x : k) ↦ v) atTop ≤ asymptoticNhds k V 0
Tactic: rw [← map_const (f := atTop (α := k))]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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))
have 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
Tactic: filter_upwards [eventually_ne_atTop 0] with _ h
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (hypothesis)
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
⊢ map (fun (x : k) ↦ v) atTop ≤ asymptoticNhds k V 0
have 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))
Tactic: have : (fun _ => v) =ᶠ[atTop (α := k)]
      (Function.uncurry (· • ·)) ∘ (fun c => (c, c⁻¹ • v)) := by
    filter_upwards [eventually_ne_atTop 0] with _ h
    simp [h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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))
⊢ map (fun (x : k) ↦ v) atTop ≤ asymptoticNhds k V 0
have 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)))
Tactic: rw [map_congr this, ← map_map, asymptoticNhds_eq_smul, ← map₂_smul, ← map_prod_eq_map₂]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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))
⊢ 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)))
have a : map (fun (c : k) ↦ (c, c⁻¹ • v)) atTop ≤ SProd.sprod (α := Filter k) (β := Filter V) atTop (𝓝 0)
Tactic: apply map_mono
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (hypothesis)
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))
⊢ map (fun (c : k) ↦ (c, c⁻¹ • v)) atTop ≤ SProd.sprod (α := Filter k) (β := Filter V) atTop (𝓝 0)
have this₁ : Tendsto (fun (c : k) ↦ (c, c⁻¹ • v)) atTop
  (SProd.sprod (α := Filter k) atTop (𝓝 (HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 v)))
Tactic: have : Tendsto (fun c => (c, c⁻¹ • v)) (atTop (α := k)) _ :=
    tendsto_id.prodMk <| tendsto_inv_atTop_zero.smul_const v
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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
⊢ asymptoticNhds k P 0 = ⊤
have have : ∀ (p : P), asymptoticNhds k P 0 = ⊤
Tactic: have ⟨p⟩ : Nonempty P := inferInstance
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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
p : P
⊢ asymptoticNhds k P 0 = ⊤
have rw : Eq.{u_3 + 1} (α := Filter P) (map (fun (x : V) ↦ x +ᵥ p) ⊤) ⊤
Tactic: rw [← asymptoticNhds_vadd_pure 0 p, asymptoticNhds_zero', vadd_pure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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
α : Type u_4
l : Filter α
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
f : α → k
g : α → V
v : V
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 v)
⊢ Tendsto (fun (x : α) ↦ f x • g x) l (asymptoticNhds k V v)
have rw : Tendsto.{u_4, u_2} (β := V) (fun (x : α) ↦ f x • g x) l
  (map (fun (p : k × V) ↦ p.1 • p.2) (SProd.sprod (α := Filter k) atTop (𝓝 v)))
Tactic: rw [asymptoticNhds_eq_smul, ← map₂_smul, ← map_prod_eq_map₂]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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
c : k
hc : 0 < c
⊢ asymptoticNhds k P (c • v) = asymptoticNhds k P v
have have : ∀ (p : P), asymptoticNhds k P (c • v) = asymptoticNhds k P v
Tactic: have ⟨p⟩ : Nonempty P := inferInstance
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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
c : k
hc : 0 < c
p : P
⊢ asymptoticNhds k P (c • v) = asymptoticNhds k P v
have simp_rw : HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 (c • v))) (pure p) =
  HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)
Tactic: simp_rw [asymptoticNhds_eq_smul_vadd _ p,
    ← show map (c • ·) (𝓝 v) = 𝓝 (c • v) from
      (Homeomorph.smulOfNeZero c hc.ne').map_nhds_eq v,
    ← map₂_smul, map₂_map_right, smul_smul, ← map₂_map_left,
    show map (· * c) atTop = atTop from (OrderIso.mulRight₀ _ hc).map_atTop]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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
c : k
hc : 0 < c
p : P
simp_rw :
  HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 (c • v))) (pure p) =
    HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)
⊢ asymptoticNhds k P (c • v) = asymptoticNhds k P v
have simp_rw₁ : HVAdd.hVAdd (β := Filter P)
    (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) (β := Filter V) atTop (map (fun (x : V) ↦ c • x) (𝓝 v))) (pure p) =
  HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)
Tactic: simp_rw [asymptoticNhds_eq_smul_vadd _ p,
    ← show map (c • ·) (𝓝 v) = 𝓝 (c • v) from
      (Homeomorph.smulOfNeZero c hc.ne').map_nhds_eq v,
    ← map₂_smul, map₂_map_right, smul_smul, ← map₂_map_left,
    show map (· * c) atTop = atTop from (OrderIso.mulRight₀ _ hc).map_atTop]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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
c : k
hc : 0 < c
p : P
simp_rw :
  HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 (c • v))) (pure p) =
    HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)
simp_rw₁ :
  HVAdd.hVAdd (β := Filter P)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) (β := Filter V) atTop (map (fun (x : V) ↦ c • x) (𝓝 v))) (pure p) =
    HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)
⊢ asymptoticNhds k P (c • v) = asymptoticNhds k P v
have simp_rw₂ : HVAdd.hVAdd (α := Filter V) (β := Filter P)
    (map₂ (fun (x1 : k) (x2 : V) ↦ x1 • x2) atTop (map (fun (x : V) ↦ c • x) (𝓝 v))) (pure p) =
  HVAdd.hVAdd (α := Filter V) (β := Filter P) (map₂ (fun (x1 : k) (x2 : V) ↦ x1 • x2) atTop (𝓝 v)) (pure p)
Tactic: simp_rw [asymptoticNhds_eq_smul_vadd _ p,
    ← show map (c • ·) (𝓝 v) = 𝓝 (c • v) from
      (Homeomorph.smulOfNeZero c hc.ne').map_nhds_eq v,
    ← map₂_smul, map₂_map_right, smul_smul, ← map₂_map_left,
    show map (· * c) atTop = atTop from (OrderIso.mulRight₀ _ hc).map_atTop]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
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
c : k
hc : 0 < c
p : P
simp_rw :
  HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 (c • v))) (pure p) =
    HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)
simp_rw₁ :
  HVAdd.hVAdd (β := Filter P)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) (β := Filter V) atTop (map (fun (x : V) ↦ c • x) (𝓝 v))) (pure p) =
    HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)
simp_rw₂ :
  HVAdd.hVAdd (α := Filter V) (β := Filter P)
      (map₂ (fun (x1 : k) (x2 : V) ↦ x1 • x2) atTop (map (fun (x : V) ↦ c • x) (𝓝 v))) (pure p) =
    HVAdd.hVAdd (α := Filter V) (β := Filter P) (map₂ (fun (x1 : k) (x2 : V) ↦ x1 • x2) atTop (𝓝 v)) (pure p)
⊢ asymptoticNhds k P (c • v) = asymptoticNhds k P v
have simp_rw₃ : HVAdd.hVAdd (α := Filter V) (β := Filter P) (map₂ (fun (a : k) (b : V) ↦ a • c • b) atTop (𝓝 v)) (pure p) =
  HVAdd.hVAdd (α := Filter V) (β := Filter P) (map₂ (fun (x1 : k) (x2 : V) ↦ x1 • x2) atTop (𝓝 v)) (pure p)
Tactic: simp_rw [asymptoticNhds_eq_smul_vadd _ p,
    ← show map (c • ·) (𝓝 v) = 𝓝 (c • v) from
      (Homeomorph.smulOfNeZero c hc.ne').map_nhds_eq v,
    ← map₂_smul, map₂_map_right, smul_smul, ← map₂_map_left,
    show map (· * c) atTop = atTop from (OrderIso.mulRight₀ _ hc).map_atTop]