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

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

Tactic:
⟨(t₁ ∩ Set.Ioi 0) • t₃, smul_mem_smul (inter_mem ht₁ (Ioi_mem_atTop _)) ht₃,
    Set.forall_mem_image2.mpr fun c ⟨hc₁, hc₂⟩ u hu => ?_⟩

Premises used: Iff.mpr, Set.Ioi, Filter.smul_mem_smul, Set.forall_mem_image2, Filter.inter_mem, Function.comp, Membership.mem, nhds, Filter.Ioi_mem_atTop, HVAdd.hVAdd, Inter.inter, And.intro, Exists.intro, HSMul.hSMul, OfNat.ofNat, _private.0.AffineSpace.asymptoticNhds_bind_nhds.match_1
-- 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
hs : t₁ • t₂ ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
t₃ : Set V
ht₃ : t₃ ∈ 𝓝 v
ht₂ : ∀ x ∈ t₃, t₂ ∈ 𝓝 x
refine :
  ∀ c ∈ t₁ ∩ Set.Ioi 0,
    ∀ (u : V) (hu : u ∈ t₃) (hc₁ : c ∈ t₁) (hc₂ : Membership.mem (γ := Set k) (Set.Ioi 0) c),
      Membership.mem (γ := Filter P) ((𝓝 ∘ fun (x : V) ↦ x +ᵥ p) (c • u)) s
⊢ ∃ t ∈ HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v),
    ∀ x ∈ t, Membership.mem (γ := Filter P) ((𝓝 ∘ fun (x : V) ↦ x +ᵥ p) x) s

Tactic:
refine ⟨(t₁ ∩ Set.Ioi 0) • t₃, smul_mem_smul (inter_mem ht₁ (Ioi_mem_atTop _)) ht₃,
    Set.forall_mem_image2.mpr fun c ⟨hc₁, hc₂⟩ u hu => ?_⟩
-- 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
hs : t₁ • t₂ ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
t₃ : Set V
ht₃ : t₃ ∈ 𝓝 v
ht₂ : ∀ x ∈ t₃, t₂ ∈ 𝓝 x
c : k
h : c ∈ t₁ ∩ Set.Ioi 0
u : V
hu : u ∈ t₃
hc₁ : c ∈ t₁
hc₂ : Membership.mem (γ := Set k) (Set.Ioi 0) c
⊢ s = Set.preimage.{u_3, u_2} (β := V) (fun (x : P) ↦ x -ᵥ p) ((fun (x : V) ↦ x +ᵥ p) ⁻¹' s)

Tactic:
simp [Set.preimage_preimage]

Premises used: Set.preimage_preimage
-- 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
hs : t₁ • t₂ ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
t₃ : Set V
ht₃ : t₃ ∈ 𝓝 v
ht₂ : ∀ x ∈ t₃, t₂ ∈ 𝓝 x
c : k
h : c ∈ t₁ ∩ Set.Ioi 0
u : V
hu : u ∈ t₃
hc₁ : c ∈ t₁
hc₂ : Membership.mem (γ := Set k) (Set.Ioi 0) c
rw :
  Membership.mem (γ := Filter P) ((𝓝 ∘ fun (x : V) ↦ x +ᵥ p) (c • u))
    (Set.preimage.{u_3, u_2} (β := V) (fun (x : P) ↦ x -ᵥ p) ((fun (x : V) ↦ x +ᵥ p) ⁻¹' s))
⊢ Membership.mem (γ := Filter P) ((𝓝 ∘ fun (x : V) ↦ x +ᵥ p) (c • u)) s

Tactic:
rw [show s = (· -ᵥ p) ⁻¹' ((· +ᵥ p) ⁻¹' s) by simp [Set.preimage_preimage]]
-- 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
hs : t₁ • t₂ ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
t₃ : Set V
ht₃ : t₃ ∈ 𝓝 v
ht₂ : ∀ x ∈ t₃, t₂ ∈ 𝓝 x
c : k
h : c ∈ t₁ ∩ Set.Ioi 0
u : V
hu : u ∈ t₃
hc₁ : c ∈ t₁
hc₂ : Membership.mem (γ := Set k) (Set.Ioi 0) c
a : (fun (x : V) ↦ x +ᵥ p) ⁻¹' s ∈ 𝓝 ((fun (x : V) ↦ x +ᵥ p) (c • u) -ᵥ p)
⊢ Membership.mem (γ := Filter P) ((𝓝 ∘ fun (x : V) ↦ x +ᵥ p) (c • u))
    (Set.preimage.{u_3, u_2} (β := V) (fun (x : P) ↦ x -ᵥ p) ((fun (x : V) ↦ x +ᵥ p) ⁻¹' s))

Tactic:
apply tendsto_id.vsub tendsto_const_nhds

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.vsub
-- 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
hs : t₁ • t₂ ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
t₃ : Set V
ht₃ : t₃ ∈ 𝓝 v
ht₂ : ∀ x ∈ t₃, t₂ ∈ 𝓝 x
c : k
h : c ∈ t₁ ∩ Set.Ioi 0
u : V
hu : u ∈ t₃
hc₁ : c ∈ t₁
hc₂ : Membership.mem (γ := Set k) (Set.Ioi 0) c
a : (fun (x : V) ↦ x +ᵥ p) ⁻¹' s ∈ 𝓝 (c • u)
⊢ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s ∈ 𝓝 ((fun (x : V) ↦ x +ᵥ p) (c • u) -ᵥ p)

Tactic:
rw [vadd_vsub]

Premises used: vadd_vsub
-- 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
hs : t₁ • t₂ ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
t₃ : Set V
ht₃ : t₃ ∈ 𝓝 v
ht₂ : ∀ x ∈ t₃, t₂ ∈ 𝓝 x
c : k
h_1 : c ∈ t₁ ∩ Set.Ioi 0
u : V
hu : u ∈ t₃
hc₁ : c ∈ t₁
hc₂ : Membership.mem (γ := Set k) (Set.Ioi 0) c
h : ∀ a ∈ c • t₂, Membership.mem (γ := Set V) ((fun (x : V) ↦ x +ᵥ p) ⁻¹' s) a
⊢ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s ∈ 𝓝 (c • u)

Tactic:
filter_upwards [smul_mem_nhds_smul₀ hc₂.ne' (ht₂ u hu)]

Premises used: smul_mem_nhds_smul₀, LT.lt.ne'
-- 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
hs : t₁ • t₂ ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
t₃ : Set V
ht₃ : t₃ ∈ 𝓝 v
ht₂ : ∀ x ∈ t₃, t₂ ∈ 𝓝 x
c : k
h_1 : c ∈ t₁ ∩ Set.Ioi 0
u : V
hu : u ∈ t₃
hc₁ : c ∈ t₁
hc₂ : Membership.mem (γ := Set k) (Set.Ioi 0) c
h : ∀ ⦃x : V⦄, x ∈ t₂ → Membership.mem (γ := Set V) ((fun (x : V) ↦ x +ᵥ p) ⁻¹' s) (c • x)
⊢ ∀ a ∈ c • t₂, Membership.mem (γ := Set V) ((fun (x : V) ↦ x +ᵥ p) ⁻¹' s) a

Tactic:
rw [← Set.image_smul, Set.forall_mem_image]

Premises used: Set.image_smul, Set.forall_mem_image
-- 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
hs : t₁ • t₂ ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
t₃ : Set V
ht₃ : t₃ ∈ 𝓝 v
ht₂ : ∀ x ∈ t₃, t₂ ∈ 𝓝 x
c : k
h : c ∈ t₁ ∩ Set.Ioi 0
u : V
hu : u ∈ t₃
hc₁ : c ∈ t₁
hc₂ : Membership.mem (γ := Set k) (Set.Ioi 0) c
⊢ ∀ ⦃x : V⦄, x ∈ t₂ → Membership.mem (γ := Set V) ((fun (x : V) ↦ x +ᵥ p) ⁻¹' s) (c • x)

Tactic:
fun w hw => hs (Set.smul_mem_smul hc₁ hw)

Premises used: Set.smul_mem_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
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
hs : t₁ • t₂ ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
t₃ : Set V
ht₃ : t₃ ∈ 𝓝 v
ht₂ : ∀ x ∈ t₃, t₂ ∈ 𝓝 x
c : k
h : c ∈ t₁ ∩ Set.Ioi 0
u : V
hu : u ∈ t₃
hc₁ : c ∈ t₁
hc₂ : Membership.mem (γ := Set k) (Set.Ioi 0) c
⊢ ∀ ⦃x : V⦄, x ∈ t₂ → Membership.mem (γ := Set V) ((fun (x : V) ↦ x +ᵥ p) ⁻¹' s) (c • x)

Tactic:
exact fun w hw => hs (Set.smul_mem_smul hc₁ hw)

Premises used: Set.smul_mem_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
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 V v).bind (asymptoticNhds k P) = asymptoticNhds k P v

Tactic:
Filter.ext' fun p => ?_

Premises used: Filter.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
v : V
refine :
  ∀ (p : P → Prop),
    (∀ᶠ (x : P) in (asymptoticNhds k V v).bind (asymptoticNhds k P), p x) ↔ ∀ᶠ (x : P) in asymptoticNhds k P v, p x
⊢ (asymptoticNhds k V v).bind (asymptoticNhds k P) = asymptoticNhds k P v

Tactic:
refine Filter.ext' fun p => ?_

Premises used: Filter.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
v : V
p : P → Prop
rw :
  (∀ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), ∀ᶠ (y : P) in asymptoticNhds k P (a.1 • a.2), p y) ↔
    ∀ᶠ (x : V) in 𝓝 v, ∀ᶠ (y : P) in asymptoticNhds k P x, p y
⊢ (∀ᶠ (x : P) in (asymptoticNhds k V v).bind (asymptoticNhds k P), p x) ↔ ∀ᶠ (x : P) in asymptoticNhds k P v, p x

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

Premises used: Filter.map₂_smul, Filter.eventually_bind, AffineSpace.nhds_bind_asymptoticNhds, Filter.eventually_map, Filter.map_prod_eq_map₂, 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
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 → Prop
nth_rw :
  (∀ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), ∀ᶠ (y : P) in asymptoticNhds k P (a.1 • a.2), p y) ↔
    ∀ᶠ (x : V) in map Prod.snd (SProd.sprod (α := Filter k) atTop (𝓝 v)), ∀ᶠ (y : P) in asymptoticNhds k P x, p y
⊢ (∀ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), ∀ᶠ (y : P) in asymptoticNhds k P (a.1 • a.2), p y) ↔
    ∀ᶠ (x : V) in 𝓝 v, ∀ᶠ (y : P) in asymptoticNhds k P x, p y

Tactic:
nth_rw 2 [← map_snd_prod (atTop (α := k)) (𝓝 v)]

Premises used: Filter.map_snd_prod, nhds, Filter.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
p : P → Prop
rw :
  (∀ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), ∀ᶠ (y : P) in asymptoticNhds k P (a.1 • a.2), p y) ↔
    ∀ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), ∀ᶠ (y : P) in asymptoticNhds k P a.2, p y
⊢ (∀ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), ∀ᶠ (y : P) in asymptoticNhds k P (a.1 • a.2), p y) ↔
    ∀ᶠ (x : V) in map Prod.snd (SProd.sprod (α := Filter k) atTop (𝓝 v)), ∀ᶠ (y : P) in asymptoticNhds k P x, p y

Tactic:
rw [eventually_map]

Premises used: Filter.eventually_map
-- 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 → Prop
h :
  ∀ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v),
    (∀ᶠ (y : P) in asymptoticNhds k P (x.1 • x.2), p y) ↔ ∀ᶠ (y : P) in asymptoticNhds k P x.2, p y
⊢ (∀ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), ∀ᶠ (y : P) in asymptoticNhds k P (a.1 • a.2), p y) ↔
    ∀ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), ∀ᶠ (y : P) in asymptoticNhds k P a.2, p y

Tactic:
apply eventually_congr

Premises used: Filter.eventually_congr
-- 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 → Prop
c : k
u : V
h :
  ∀ (hc : 0 < c),
    (∀ᶠ (y : P) in asymptoticNhds k P ((c, u).1 • (c, u).2), p y) ↔ ∀ᶠ (y : P) in asymptoticNhds k P (c, u).2, p y
⊢ 0 < (c, u).1 →
    ((∀ᶠ (y : P) in asymptoticNhds k P ((c, u).1 • (c, u).2), p y) ↔ ∀ᶠ (y : P) in asymptoticNhds k P (c, u).2, p y)

Tactic:
(hc : 0 < c)
-- 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 → Prop
h :
  ∀ (c : k) (u : V) (hc : 0 < c),
    (∀ᶠ (y : P) in asymptoticNhds k P ((c, u).1 • (c, u).2), p y) ↔ ∀ᶠ (y : P) in asymptoticNhds k P (c, u).2, p y
⊢ ∀ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v),
    (∀ᶠ (y : P) in asymptoticNhds k P (x.1 • x.2), p y) ↔ ∀ᶠ (y : P) in asymptoticNhds k P x.2, p y

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

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
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 → Prop
c : k
u : V
hc : 0 < c
⊢ (∀ᶠ (y : P) in asymptoticNhds k P ((c, u).1 • (c, u).2), p y) ↔ ∀ᶠ (y : P) in asymptoticNhds k P (c, u).2, p y

Tactic:
simp only [asymptoticNhds_smul _ hc]

Premises used: AffineSpace.asymptoticNhds_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
v : V
s : Set P
⊢ v ∈ asymptoticCone k s ↔ ∃ᶠ (p : P) in asymptoticNhds k P v, p ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, 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
⊢ asymptoticCone.{u_1, u_2, u_3} k (P := P) ∅ = ∅

Tactic:
Set.eq_empty_iff_forall_notMem.mpr fun _ => frequently_false _

Premises used: Iff.mpr, Filter.frequently_false, Set.eq_empty_iff_forall_notMem, AffineSpace.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
s t : Set P
h : s ⊆ t
⊢ asymptoticCone k s ⊆ asymptoticCone k t

Tactic:
fun _ h' => h'.mono h

Premises used: Set.Mem, setOf, Set.Subset, Filter.Frequently, Filter.Frequently.mono, 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
s t : Set P
h : ∀ (x : V), x ∈ asymptoticCone k (s ∪ t) ↔ x ∈ asymptoticCone k s ∪ asymptoticCone k t
⊢ asymptoticCone k (s ∪ t) = asymptoticCone k s ∪ asymptoticCone k t

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
s t : Set P
x : V
⊢ x ∈ asymptoticCone k (s ∪ t) ↔ x ∈ asymptoticCone k s ∪ asymptoticCone k t

Tactic:
simp only [Set.mem_union, mem_asymptoticCone_iff, Filter.frequently_or_distrib]

Premises used: Set.mem_union, mem_asymptoticCone_iff, Filter.frequently_or_distrib
-- 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
s : Set ι
hs : s.Finite
f : ι → Set P
empty :
  asymptoticCone.{u_1, u_2, u_3} k (P := P) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), f i) =
    ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), asymptoticCone k (f i)
insert :
  ∀ {a : ι} {s : Set ι},
    a ∉ s →
      s.Finite →
        asymptoticCone.{u_1, u_2, u_3} k (P := P) (⋃ i ∈ s, f i) = ⋃ i ∈ s, asymptoticCone k (f i) →
          asymptoticCone.{u_1, u_2, u_3} k (P := P) (⋃ i ∈ Insert.insert a s, f i) =
            ⋃ i ∈ Insert.insert a s, asymptoticCone k (f i)
⊢ asymptoticCone.{u_1, u_2, u_3} k (P := P) (⋃ i ∈ s, f i) = ⋃ i ∈ s, asymptoticCone k (f i)

Tactic:
induction s, hs using Set.Finite.induction_on
-- 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
s : Set ι
f : ι → Set P
⊢ asymptoticCone.{u_1, u_2, u_3} k (P := P) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), f i) =
    ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), asymptoticCone k (f i)

Tactic:
simp [asymptoticCone_union, *]

Premises used: asymptoticCone_union
-- 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
s : Set ι
f : ι → Set P
a : ι
s_1 : Set ι
h : a ∉ s_1
hs : s_1.Finite
h_1 : asymptoticCone.{u_1, u_2, u_3} k (P := P) (⋃ i ∈ s_1, f i) = ⋃ i ∈ s_1, asymptoticCone k (f i)
⊢ asymptoticCone.{u_1, u_2, u_3} k (P := P) (⋃ i ∈ insert a s_1, f i) = ⋃ i ∈ insert a s_1, asymptoticCone k (f i)

Tactic:
simp [asymptoticCone_union, *]

Premises used: asymptoticCone_union
-- 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
S : Set (Set P)
hS : S.Finite
rw : asymptoticCone.{u_1, u_2, u_3} k (P := P) (⋃ i ∈ S, i) = ⋃ s ∈ S, asymptoticCone k s
rw₁ rw₂ : Eq.{u_2 + 1} (α := Set V) (⋃ i ∈ S, asymptoticCone k i) (⋃ s ∈ S, asymptoticCone k s)
⊢ asymptoticCone k (⋃₀ S) = ⋃ s ∈ S, asymptoticCone k s

Tactic:
rw [Set.sUnion_eq_biUnion, asymptoticCone_biUnion hS]

Premises used: Set.sUnion_eq_biUnion, asymptoticCone_biUnion
-- 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
s : Finset ι
f : ι → Set P
⊢ asymptoticCone.{u_1, u_2, u_3} k (P := P) (⋃ i ∈ s, f i) = ⋃ i ∈ s, asymptoticCone k (f i)

Tactic:
asymptoticCone_biUnion s.finite_toSet f

Premises used: asymptoticCone_biUnion, Finset.finite_toSet
-- 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
inst_6 : Finite ι
f : ι → Set P
rw : asymptoticCone k (⋃₀ Set.range f) = ⋃ (i : ι), asymptoticCone k (f i)
rw₁ : Eq.{u_2 + 1} (α := Set V) (⋃ s ∈ Set.range f, asymptoticCone k s) (⋃ (i : ι), asymptoticCone k (f i))
rw₂ rw₃ : Eq.{u_2 + 1} (α := Set V) (⋃ (y : ι), asymptoticCone k (f y)) (⋃ (i : ι), asymptoticCone k (f i))
⊢ asymptoticCone.{u_1, u_2, u_3} k (P := P) (⋃ (i : ι), f i) = ⋃ (i : ι), asymptoticCone k (f i)

Tactic:
rw [← Set.sUnion_range, asymptoticCone_sUnion (Set.finite_range f), Set.biUnion_range]

Premises used: Set.sUnion_range, Set.biUnion_range, Set.finite_range, asymptoticCone_sUnion