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
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : AffineSubspace k P
hs : (↑s : Set P).Nonempty
p : P
hp : p ∈ (↑s : Set P)
v : V
h : v ∈ asymptoticCone k (↑s : Set P) ↔ v ∈ asymptoticCone k (↑s.direction : Set V)
h₁ :
  (∃ᶠ (p : P) in asymptoticNhds k P v, p ∈ (↑s : Set P)) ↔
    ∃ᶠ (p : V) in asymptoticNhds k V v, p ∈ (↑s.direction : Set V)
h₂ :
  (∃ᶠ (p : P) in HVAdd.hVAdd (β := Filter P) (asymptoticNhds k V v) (pure p), p ∈ (↑s : Set P)) ↔
    ∃ᶠ (p : V) in asymptoticNhds k V v, p ∈ (↑s.direction : Set V)
h₃ :
  (∃ᶠ (p : P) in map (fun (x : V) ↦ x +ᵥ p) (asymptoticNhds k V v), p ∈ (↑s : Set P)) ↔
    ∃ᶠ (p : V) in asymptoticNhds k V v, p ∈ (↑s.direction : Set V)
⊢ v ∈ asymptoticCone k (↑s : Set P) ↔ v ∈ closure[inst_5] (↑s.direction : Set V)
have h₄ : (∃ᶠ (a : V) in asymptoticNhds k V v, a +ᵥ p ∈ (↑s : Set P)) ↔
  ∃ᶠ (p : V) in asymptoticNhds k V v, p ∈ (↑s.direction : Set V)
Tactic: simp_rw [← asymptoticCone_submodule, mem_asymptoticCone_iff, ← asymptoticNhds_vadd_pure v p,
    vadd_pure, frequently_map, SetLike.mem_coe, s.vadd_mem_iff_mem_direction _ hp]
-- 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
s : AffineSubspace k P
hs : (↑s : Set P).Nonempty
p : P
hp : p ∈ (↑s : Set P)
v : V
h : v ∈ asymptoticCone k (↑s : Set P) ↔ v ∈ asymptoticCone k (↑s.direction : Set V)
h₁ :
  (∃ᶠ (p : P) in asymptoticNhds k P v, p ∈ (↑s : Set P)) ↔
    ∃ᶠ (p : V) in asymptoticNhds k V v, p ∈ (↑s.direction : Set V)
h₂ :
  (∃ᶠ (p : P) in HVAdd.hVAdd (β := Filter P) (asymptoticNhds k V v) (pure p), p ∈ (↑s : Set P)) ↔
    ∃ᶠ (p : V) in asymptoticNhds k V v, p ∈ (↑s.direction : Set V)
h₃ :
  (∃ᶠ (p : P) in map (fun (x : V) ↦ x +ᵥ p) (asymptoticNhds k V v), p ∈ (↑s : Set P)) ↔
    ∃ᶠ (p : V) in asymptoticNhds k V v, p ∈ (↑s.direction : Set V)
h₄ :
  (∃ᶠ (a : V) in asymptoticNhds k V v, a +ᵥ p ∈ (↑s : Set P)) ↔
    ∃ᶠ (p : V) in asymptoticNhds k V v, p ∈ (↑s.direction : Set V)
⊢ v ∈ asymptoticCone k (↑s : Set P) ↔ v ∈ closure[inst_5] (↑s.direction : Set V)
have h₅ : (∃ᶠ (a : V) in asymptoticNhds k V v, a +ᵥ p ∈ s) ↔ ∃ᶠ (p : V) in asymptoticNhds k V v, p ∈ s.direction
Tactic: simp_rw [← asymptoticCone_submodule, mem_asymptoticCone_iff, ← asymptoticNhds_vadd_pure v p,
    vadd_pure, frequently_map, SetLike.mem_coe, s.vadd_mem_iff_mem_direction _ hp]
-- 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
⊢ asymptoticCone.{u_1, u_2, u_3} k (P := P) Set.univ = Set.univ
have rw : asymptoticCone k (↑⊤ : Set P) = Set.univ
Tactic: rw [← AffineSubspace.top_coe k, asymptoticCone_affineSubspace Set.univ_nonempty,
    AffineSubspace.direction_top, Submodule.top_coe, closure_univ]
-- 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
rw : asymptoticCone k (↑⊤ : Set P) = Set.univ
⊢ asymptoticCone.{u_1, u_2, u_3} k (P := P) Set.univ = Set.univ
have rw₁ : closure[inst_5] (↑(AffineSubspace.direction.{u_1, u_2, u_3} (P := P) ⊤) : Set V) = Set.univ
Tactic: rw [← AffineSubspace.top_coe k, asymptoticCone_affineSubspace Set.univ_nonempty,
    AffineSubspace.direction_top, Submodule.top_coe, closure_univ]
-- 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
rw : asymptoticCone k (↑⊤ : Set P) = Set.univ
rw₁ : closure[inst_5] (↑(AffineSubspace.direction.{u_1, u_2, u_3} (P := P) ⊤) : Set V) = Set.univ
⊢ asymptoticCone.{u_1, u_2, u_3} k (P := P) Set.univ = Set.univ
have rw₂ : closure[inst_5] (↑⊤ : Set V) = Set.univ
Tactic: rw [← AffineSubspace.top_coe k, asymptoticCone_affineSubspace Set.univ_nonempty,
    AffineSubspace.direction_top, Submodule.top_coe, closure_univ]
-- 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
rw : asymptoticCone k (↑⊤ : Set P) = Set.univ
rw₁ : closure[inst_5] (↑(AffineSubspace.direction.{u_1, u_2, u_3} (P := P) ⊤) : Set V) = Set.univ
rw₂ : closure[inst_5] (↑⊤ : Set V) = Set.univ
⊢ asymptoticCone.{u_1, u_2, u_3} k (P := P) Set.univ = Set.univ
have rw₃ : Eq.{u_2 + 1} (α := Set V) (closure[inst_5] Set.univ) Set.univ
Tactic: rw [← AffineSubspace.top_coe k, asymptoticCone_affineSubspace Set.univ_nonempty,
    AffineSubspace.direction_top, Submodule.top_coe, closure_univ]
-- 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
rw : asymptoticCone k (↑⊤ : Set P) = Set.univ
rw₁ : closure[inst_5] (↑(AffineSubspace.direction.{u_1, u_2, u_3} (P := P) ⊤) : Set V) = Set.univ
rw₂ : closure[inst_5] (↑⊤ : Set V) = Set.univ
rw₃ : Eq.{u_2 + 1} (α := Set V) (closure[inst_5] Set.univ) Set.univ
⊢ asymptoticCone.{u_1, u_2, u_3} k (P := P) Set.univ = Set.univ
have rw₄ : Eq.{u_2 + 1} (α := Set V) Set.univ Set.univ
Tactic: rw [← AffineSubspace.top_coe k, asymptoticCone_affineSubspace Set.univ_nonempty,
    AffineSubspace.direction_top, Submodule.top_coe, closure_univ]
-- 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
inst_11 : TopologicalSpace P
inst_12 : IsTopologicalAddTorsor P
s : Set P
⊢ asymptoticCone k (closure[inst_11] s) = asymptoticCone k s
have h : ∀ (x : V), x ∈ asymptoticCone k (closure[inst_11] s) ↔ x ∈ asymptoticCone k s
Tactic: ext
-- 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
inst_11 : TopologicalSpace P
inst_12 : IsTopologicalAddTorsor P
s : Set P
x : V
⊢ x ∈ asymptoticCone k (closure[inst_11] s) ↔ x ∈ asymptoticCone k s
have h : (∃ᶠ (p : P) in asymptoticNhds k P x, p ∈ closure[inst_11] s) ↔ ∃ᶠ (p : P) in asymptoticNhds k P x, p ∈ s
Tactic: simp_rw [mem_asymptoticCone_iff, mem_closure_iff_frequently, ← frequently_bind,
    asymptoticNhds_bind_nhds]
-- 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
inst_11 : TopologicalSpace P
inst_12 : IsTopologicalAddTorsor P
s : Set P
x : V
h : (∃ᶠ (p : P) in asymptoticNhds k P x, p ∈ closure[inst_11] s) ↔ ∃ᶠ (p : P) in asymptoticNhds k P x, p ∈ s
⊢ x ∈ asymptoticCone k (closure[inst_11] s) ↔ x ∈ asymptoticCone k s
have h₁ : (∃ᶠ (p : P) in asymptoticNhds k P x, ∃ᶠ (x : P) in 𝓝 p, x ∈ s) ↔ ∃ᶠ (x : P) in asymptoticNhds k P x, x ∈ s
Tactic: simp_rw [mem_asymptoticCone_iff, mem_closure_iff_frequently, ← frequently_bind,
    asymptoticNhds_bind_nhds]
-- 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
inst_11 : TopologicalSpace P
inst_12 : IsTopologicalAddTorsor P
s : Set P
x : V
h : (∃ᶠ (p : P) in asymptoticNhds k P x, p ∈ closure[inst_11] s) ↔ ∃ᶠ (p : P) in asymptoticNhds k P x, p ∈ s
h₁ : (∃ᶠ (p : P) in asymptoticNhds k P x, ∃ᶠ (x : P) in 𝓝 p, x ∈ s) ↔ ∃ᶠ (x : P) in asymptoticNhds k P x, x ∈ s
⊢ x ∈ asymptoticCone k (closure[inst_11] s) ↔ x ∈ asymptoticCone k s
have h₂ : (∃ᶠ (x : P) in (asymptoticNhds k P x).bind 𝓝, x ∈ s) ↔ ∃ᶠ (x : P) in asymptoticNhds k P x, x ∈ s
Tactic: simp_rw [mem_asymptoticCone_iff, mem_closure_iff_frequently, ← frequently_bind,
    asymptoticNhds_bind_nhds]
-- 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
s : Set P
⊢ IsClosed[inst_5] (asymptoticCone k s)
have have : ∀ (p : P), IsClosed[inst_5] (asymptoticCone k s)
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
s : Set P
p : P
⊢ IsClosed[inst_5] (asymptoticCone k s)
have rw : ∀ (x : V), (∃ᶠ (y : V) in 𝓝 x, y ∈ asymptoticCone k s) → x ∈ asymptoticCone k s
Tactic: rw [isClosed_iff_frequently]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : Set P
p : P
v : V
h : ∃ᶠ (y : V) in 𝓝 v, y ∈ asymptoticCone k s
⊢ v ∈ asymptoticCone k s
have h₁ : ∃ᶠ (p : P) in asymptoticNhds k P v, p ∈ s
Tactic: simp_rw [mem_asymptoticCone_iff, ← frequently_bind, nhds_bind_asymptoticNhds] at h
Cleared hypotheses: h
-- 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
s : Set P
⊢ asymptoticCone k (asymptoticCone k s) = asymptoticCone k s
have h : ∀ (x : V), x ∈ asymptoticCone k (asymptoticCone k s) ↔ x ∈ asymptoticCone k s
Tactic: ext
-- 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
s : Set P
x : V
⊢ x ∈ asymptoticCone k (asymptoticCone k s) ↔ x ∈ asymptoticCone k s
have h : (∃ᶠ (p : V) in asymptoticNhds k V x, ∃ᶠ (p : P) in asymptoticNhds k P p, p ∈ s) ↔
  ∃ᶠ (p : P) in asymptoticNhds k P x, p ∈ s
Tactic: simp_rw [mem_asymptoticCone_iff, ← Filter.frequently_bind, asymptoticNhds_bind_asymptoticNhds]
-- 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
s : Set P
x : V
h :
  (∃ᶠ (p : V) in asymptoticNhds k V x, ∃ᶠ (p : P) in asymptoticNhds k P p, p ∈ s) ↔
    ∃ᶠ (p : P) in asymptoticNhds k P x, p ∈ s
⊢ x ∈ asymptoticCone k (asymptoticCone k s) ↔ x ∈ asymptoticCone k s
have h₁ : (∃ᶠ (p : P) in (asymptoticNhds k V x).bind (asymptoticNhds k P), p ∈ s) ↔ ∃ᶠ (p : P) in asymptoticNhds k P x, p ∈ s
Tactic: simp_rw [mem_asymptoticCone_iff, ← Filter.frequently_bind, asymptoticNhds_bind_asymptoticNhds]
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst_7] s
hc : 0 ≤ c
hv : v ∈ asymptoticCone k s
⊢ c • v +ᵥ p ∈ s
have refine : ∃ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), c • x.2 +ᵥ p ∈ s
Tactic: refine isClosed_iff_frequently.mp hs₂ _ <|
    tendsto_snd (f := atTop (α := k)) |>.const_smul _ |>.vadd_const _ |>.frequently ?_
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst_7] s
hc : 0 ≤ c
hv : v ∈ asymptoticCone k s
⊢ ∃ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), c • x.2 +ᵥ p ∈ s
have hv₁ : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ p ∈ s
Tactic: rw [mem_asymptoticCone_iff, asymptoticNhds_eq_smul_vadd v p, vadd_pure, frequently_map,
    ← map₂_smul, ← map_prod_eq_map₂, frequently_map] at hv
Cleared hypotheses: hv
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst_7] s
hc : 0 ≤ c
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ p ∈ s
⊢ ∃ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), c • x.2 +ᵥ p ∈ s
have apply : ∀ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), x.1 • x.2 +ᵥ p ∈ s → c • x.2 +ᵥ p ∈ s
Tactic: apply hv.mp
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst_7] s
hc : 0 ≤ c
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ p ∈ s
t : k
u : V
⊢ c ≤ (t, u).1 → (t, u).1 • (t, u).2 +ᵥ p ∈ s → c • (t, u).2 +ᵥ p ∈ s
have h : ∀ (ht : c ≤ t), (t, u).1 • (t, u).2 +ᵥ p ∈ s → c • (t, u).2 +ᵥ p ∈ s
Tactic: (ht : c ≤ t)
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst_7] s
hc : 0 ≤ c
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ p ∈ s
t : k
u : V
ht : c ≤ t
⊢ (t, u).1 • (t, u).2 +ᵥ p ∈ s → c • (t, u).2 +ᵥ p ∈ s
have h : ∀ (h : t • u +ᵥ p ∈ s), c • (t, u).2 +ᵥ p ∈ s
Tactic: (h : t • u +ᵥ p ∈ s)
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst_7] s
hc : 0 ≤ c
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ p ∈ s
⊢ ∀ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), x.1 • x.2 +ᵥ p ∈ s → c • x.2 +ᵥ p ∈ s
have h : ∀ (t : k) (u : V) (ht : c ≤ t) (h : t • u +ᵥ p ∈ s), c • (t, u).2 +ᵥ p ∈ s
Tactic: filter_upwards [tendsto_fst.eventually (eventually_ge_atTop c)]
    with ⟨t, u⟩ (ht : c ≤ t) (h : t • u +ᵥ p ∈ s)
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst_7] s
hc : 0 ≤ c
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ p ∈ s
t : k
u : V
ht : c ≤ t
h : t • u +ᵥ p ∈ s
⊢ c • (t, u).2 +ᵥ p ∈ s
have h₁ : c • u +ᵥ p ∈ s
Tactic: change c • u +ᵥ p ∈ s
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst_7] s
hc : 0 ≤ c
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ p ∈ s
t : k
u : V
ht : c ≤ t
h : t • u +ᵥ p ∈ s
⊢ c • u +ᵥ p ∈ s
have h₁ : c • u +ᵥ p ∈ segment k p (t • u +ᵥ p)
Tactic: apply hs₁.segment_subset 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst_7] s
hc : 0 ≤ c
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ p ∈ s
t : k
u : V
ht : c ≤ t
h : t • u +ᵥ p ∈ s
⊢ c • u +ᵥ p ∈ segment k p (t • u +ᵥ p)
have h₁ : SameRay k (c • u) ((t - c) • u)
Tactic: simp_rw [mem_segment_iff_sameRay, ← vsub_eq_sub, vadd_vsub, vadd_vsub_vadd_cancel_right,
    ← sub_smul]
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
hs : Convex k s
⊢ Convex k (asymptoticCone k s)
have inr : ∀ (this : ∀ {s : Set V} (hs : Convex k s) (hs' : IsClosed[inst_7] s), Convex k (asymptoticCone k s))
  (hs' : ¬IsClosed[inst_7] s), Convex k (asymptoticCone k s)
Tactic: wlog hs' : IsClosed s generalizing s
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
hs : Convex k s
inr :
  ∀ (this : ∀ {s : Set V} (hs : Convex k s) (hs' : IsClosed[inst_7] s), Convex k (asymptoticCone k s))
    (hs' : ¬IsClosed[inst_7] s), Convex k (asymptoticCone k s)
⊢ Convex k (asymptoticCone k s)
have wlog : ∀ {s : Set V} (hs : Convex k s) (hs' : IsClosed[inst_7] s), Convex k (asymptoticCone k s)
Tactic: wlog hs' : IsClosed s generalizing s
Cleared hypotheses: hs
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
hs : Convex k s
this : ∀ {s : Set V} (hs : Convex k s) (hs' : IsClosed[inst_7] s), Convex k (asymptoticCone k s)
hs' : ¬IsClosed[inst_7] s
⊢ Convex k (asymptoticCone k s)
have inr : Convex k (asymptoticCone k (closure[inst_7] s))
Tactic: rw [← asymptoticCone_closure]
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s_1 s : Set V
hs : Convex k s
hs' : IsClosed[inst_7] s
⊢ Convex k (asymptoticCone k s)
have inl : ∀ (hs : Convex.{u_1, u_2} k (E := V) ∅) (hs' : IsClosed[inst_7] ∅), Convex k (asymptoticCone k (P := V) ∅)
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨p, hp⟩
Cleared hypotheses: s, hs, hs'
-- 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 : IsStrictOrderedRing k
inst_3 : TopologicalSpace k
inst_4 : OrderTopology k
inst_5 : AddCommGroup V
inst_6 : Module k V
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s_1 s : Set V
hs : Convex k s
hs' : IsClosed[inst_7] s
inl : ∀ (hs : Convex.{u_1, u_2} k (E := V) ∅) (hs' : IsClosed[inst_7] ∅), Convex k (asymptoticCone k (P := V) ∅)
⊢ Convex k (asymptoticCone k s)
have inr : ∀ (p : V) (hp : p ∈ s), Convex k (asymptoticCone k s)
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨p, hp⟩