awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
⊢ 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
-- 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_1 :
  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))
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)))
⊢ map (fun (c : k) ↦ (c, c⁻¹ • v)) atTop ≤ SProd.sprod (α := Filter k) (β := Filter V) atTop (𝓝 0)

Tactic:
simpa
-- 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
have : ∀ (p : P), asymptoticNhds k P 0 = ⊤
⊢ asymptoticNhds k P 0 = ⊤

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
p : P
rw : Eq.{u_3 + 1} (α := Filter P) (map (fun (x : V) ↦ x +ᵥ p) ⊤) ⊤
⊢ asymptoticNhds k P 0 = ⊤

Tactic:
rw [← asymptoticNhds_vadd_pure 0 p, asymptoticNhds_zero', vadd_pure]

Premises used: AffineSpace.asymptoticNhds_vadd_pure, Filter.vadd_pure, _private.0.AffineSpace.asymptoticNhds_zero', 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
p : P
⊢ Eq.{u_3 + 1} (α := Filter P) (map (fun (x : V) ↦ x +ᵥ p) ⊤) ⊤

Tactic:
(Equiv.vaddConst p).surjective.filter_map_top

Premises used: Equiv.vaddConst, Function.Surjective.filter_map_top, Equiv.surjective
-- 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
p : P
⊢ Eq.{u_3 + 1} (α := Filter P) (map (fun (x : V) ↦ x +ᵥ p) ⊤) ⊤

Tactic:
exact (Equiv.vaddConst p).surjective.filter_map_top

Premises used: Equiv.vaddConst, Function.Surjective.filter_map_top, Equiv.surjective
-- 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
α : 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)
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)))
⊢ Tendsto (fun (x : α) ↦ f x • g x) l (asymptoticNhds k V v)

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

Premises used: Filter.map₂_smul, 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
α : 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.{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:
tendsto_map.comp (hf.prodMk hg)

Premises used: Filter.tendsto_map, Filter.Tendsto.prodMk, 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
α : 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.{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:
exact tendsto_map.comp (hf.prodMk hg)

Premises used: Filter.tendsto_map, Filter.Tendsto.prodMk, 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
α : 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
v : V
hf : Tendsto f l atTop
⊢ Tendsto (fun (x : α) ↦ f x • v) l (asymptoticNhds k V v)

Tactic:
hf.atTop_smul_nhds_tendsto_asymptoticNhds tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.atTop_smul_nhds_tendsto_asymptoticNhds
-- 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
c : k
hc : 0 < c
have : ∀ (p : P), asymptoticNhds k P (c • v) = asymptoticNhds k P v
⊢ asymptoticNhds k P (c • v) = asymptoticNhds k P v

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
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)
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)
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)
simp_rw₅ :
  HVAdd.hVAdd (β := Filter P) (map₂.{u_1, u_2, u_2} (α := k) HSMul.hSMul (map (fun (a : k) ↦ a * c) atTop) (𝓝 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

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]

Premises used: Filter.map₂_smul, Filter.map₂_map_right, Homeomorph.map_nhds_eq, Filter.map₂_map_left, OrderIso.mulRight₀, smul_smul, LT.lt.ne', Homeomorph.smulOfNeZero, AffineSpace.asymptoticNhds_eq_smul_vadd, OrderIso.map_atTop
-- 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
a : (𝓝 v).bind (asymptoticNhds k P) ≤ asymptoticNhds k P v
a₁ : asymptoticNhds k P v ≤ (𝓝 v).bind (asymptoticNhds k P)
⊢ (𝓝 v).bind (asymptoticNhds k P) = asymptoticNhds k P v

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
a : ∀ (p : P), (𝓝 v).bind (asymptoticNhds k P) ≤ asymptoticNhds k P v
⊢ (𝓝 v).bind (asymptoticNhds k P) ≤ asymptoticNhds k P v

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
v : V
p : P
a :
  LE.le.{u_3} (α := Filter P)
    ((𝓝 v).bind fun (v : V) ↦ map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
    (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
⊢ ((𝓝 v).bind fun (v : V) ↦ asymptoticNhds k P v) ≤ asymptoticNhds k P v

Tactic:
simp_rw [asymptoticNhds_eq_smul_vadd _ p, vadd_pure]

Premises used: Filter.vadd_pure, 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
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
a :
  LE.le.{u_3} (α := Filter P)
    ((𝓝 v).bind fun (v : V) ↦ map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
    (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop ((𝓝 v).bind 𝓝)))
⊢ LE.le.{u_3} (α := Filter P)
    ((𝓝 v).bind fun (v : V) ↦ map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
    (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))

Tactic:
nth_rw 2 [← nhds_bind_nhds]

Premises used: nhds_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
v : V
p : P
a :
  ∀ (x : Set P),
    (∃ (s : Set k),
        Membership.mem (γ := Filter k) atTop s ∧
          ∃ (t : Set V),
            (∃ t_1 ∈ 𝓝 v, ∀ x ∈ t_1, t ∈ 𝓝 x) ∧
              Subset (α := Set V) (Set.image2 (fun (x1 : k) (x2 : V) ↦ x1 • x2) s t) ((fun (x : V) ↦ x +ᵥ p) ⁻¹' x)) →
      ∃ t ∈ 𝓝 v,
        ∀ x_1 ∈ t,
          ∃ (s : Set k),
            Membership.mem (γ := Filter k) atTop s ∧
              ∃ t ∈ 𝓝 x_1,
                Subset (α := Set V) (Set.image2 (fun (x1 : k) (x2 : V) ↦ x1 • x2) s t) ((fun (x : V) ↦ x +ᵥ p) ⁻¹' x)
⊢ LE.le.{u_3} (α := Filter P)
    ((𝓝 v).bind fun (v : V) ↦ map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
    (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop ((𝓝 v).bind 𝓝)))

Tactic:
simp only [le_def, mem_map, ← map₂_smul, mem_map₂_iff, mem_bind]

Premises used: Filter.map₂_smul, Filter.mem_bind, Filter.mem_map₂_iff, Filter.mem_map, Filter.le_def
-- 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
⊢ ∀ (x : Set P),
    (∃ (s : Set k),
        Membership.mem (γ := Filter k) atTop s ∧
          ∃ (t : Set V),
            (∃ t_1 ∈ 𝓝 v, ∀ x ∈ t_1, t ∈ 𝓝 x) ∧
              Subset (α := Set V) (Set.image2 (fun (x1 : k) (x2 : V) ↦ x1 • x2) s t) ((fun (x : V) ↦ x +ᵥ p) ⁻¹' x)) →
      ∃ t ∈ 𝓝 v,
        ∀ x_1 ∈ t,
          ∃ (s : Set k),
            Membership.mem (γ := Filter k) atTop s ∧
              ∃ t ∈ 𝓝 x_1,
                Subset (α := Set V) (Set.image2 (fun (x1 : k) (x2 : V) ↦ x1 • x2) s t) ((fun (x : V) ↦ x +ᵥ p) ⁻¹' x)

Tactic:
grind
-- 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
⊢ Filter.bind (pure v) (asymptoticNhds k P) ≤ (𝓝 v).bind (asymptoticNhds k P)

Tactic:
bind_mono (pure_le_nhds v) .rfl

Premises used: Filter.EventuallyLE.rfl, pure_le_nhds, Filter.bind_mono
-- 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
⊢ Filter.bind (pure v) (asymptoticNhds k P) ≤ (𝓝 v).bind (asymptoticNhds k P)

Tactic:
exact bind_mono (pure_le_nhds v) .rfl

Premises used: Filter.EventuallyLE.rfl, pure_le_nhds, Filter.bind_mono
-- 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
v : V
⊢ (asymptoticNhds k P v).bind 𝓝 = asymptoticNhds k P v

Tactic:
le_antisymm (fun s h => ?_) (bind_mono le_rfl (.of_forall pure_le_nhds))

Premises used: le_rfl, pure_le_nhds, Filter.Eventually.of_forall, le_antisymm, Filter.bind_mono
-- 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
v : V
refine : ∀ (s : Set P) (h : s ∈ asymptoticNhds k P v), s ∈ (asymptoticNhds k P v).bind 𝓝
⊢ (asymptoticNhds k P v).bind 𝓝 = asymptoticNhds k P v

Tactic:
refine le_antisymm (fun s h => ?_) (bind_mono le_rfl (.of_forall pure_le_nhds))

Premises used: le_rfl, pure_le_nhds, Filter.Eventually.of_forall, le_antisymm, Filter.bind_mono
-- 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
v : V
s : Set P
h : s ∈ asymptoticNhds k P v
have : ∀ (p : P), s ∈ (asymptoticNhds k P v).bind 𝓝
⊢ s ∈ (asymptoticNhds k P v).bind 𝓝

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
inst_11 : TopologicalSpace P
inst_12 : IsTopologicalAddTorsor P
v : V
s : Set P
h : s ∈ asymptoticNhds k P v
p : P
rw :
  ∀
    (h :
      Membership.mem (γ := Filter P)
        (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v))) s),
    Membership.mem (γ := Filter P)
      (Filter.bind (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v))) 𝓝) s
⊢ s ∈ (asymptoticNhds k P v).bind 𝓝

Tactic:
rw [asymptoticNhds_eq_smul_vadd _ p, vadd_pure] at h ⊢

Premises used: Filter.vadd_pure, 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
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
v : V
s : Set P
p : P
h :
  Membership.mem (γ := Filter P) (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
    s
⊢ Membership.mem (γ := Filter P)
    (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop ((𝓝 v).bind 𝓝))) s

Tactic:
rw [← nhds_bind_nhds] at h

Premises used: nhds_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
inst_11 : TopologicalSpace P
inst_12 : IsTopologicalAddTorsor P
v : V
s : Set P
p : P
h :
  Membership.mem (γ := Filter P)
    (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop ((𝓝 v).bind 𝓝))) s
obtain :
  ∀ (t₁ : Set k) (ht₁ : Membership.mem (γ := Filter k) atTop t₁) (t₂ : Set V) (ht₂ : t₂ ∈ (𝓝 v).bind 𝓝)
    (hs : t₁ • t₂ ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s),
    Membership.mem (γ := Filter P)
      (Filter.bind (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v))) 𝓝) s
⊢ Membership.mem (γ := Filter P)
    (Filter.bind (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v))) 𝓝) s

Tactic:
obtain ⟨t₁, ht₁, t₂, ht₂, hs⟩ := 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
inst_11 : TopologicalSpace P
inst_12 : IsTopologicalAddTorsor P
v : V
s : Set P
p : P
t₁ : Set k
ht₁ : Membership.mem (γ := Filter k) atTop t₁
t₂ : Set V
ht₂ : t₂ ∈ (𝓝 v).bind 𝓝
hs : t₁ • t₂ ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
⊢ ∃ t ∈ 𝓝 v, ∀ x ∈ t, t₂ ∈ 𝓝 x

Tactic:
rw [mem_bind] at ht₂

Premises used: Filter.mem_bind
-- 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
v : V
s : Set P
p : P
t₁ : Set k
ht₁ : Membership.mem (γ := Filter k) atTop t₁
t₂ : Set V
ht₂ : t₂ ∈ (𝓝 v).bind 𝓝
hs : t₁ • t₂ ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
ht₃ : ∃ t ∈ 𝓝 v, ∀ x ∈ t, t₂ ∈ 𝓝 x
⊢ t₁ • t₂ ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s

Tactic:
rw [mem_bind] at ht₂

Premises used: Filter.mem_bind
-- 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
v : V
s : Set P
p : P
t₁ : Set k
ht₁ : Membership.mem (γ := Filter k) atTop t₁
t₂ : Set V
ht₂ : ∃ t ∈ 𝓝 v, ∀ x ∈ t, t₂ ∈ 𝓝 x
hs : t₁ • t₂ ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
obtain :
  ∀ (t₃ : Set V) (ht₃ : t₃ ∈ 𝓝 v) (ht₂ : ∀ x ∈ t₃, t₂ ∈ 𝓝 x),
    Membership.mem (γ := Filter P)
      (Filter.bind (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v))) 𝓝) s
⊢ Membership.mem (γ := Filter P)
    (Filter.bind (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v))) 𝓝) s

Tactic:
obtain ⟨t₃, ht₃, ht₂⟩ := ht₂