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 : 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
⊢ ∃ᶠ (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

Premises used: Filter.map₂_smul, Filter.frequently_map, Filter.vadd_pure, Filter.map_prod_eq_map₂, mem_asymptoticCone_iff, AffineSpace.asymptoticNhds_eq_smul_vadd
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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
apply : ∀ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), x.1 • x.2 +ᵥ p ∈ s → c • x.2 +ᵥ p ∈ s
⊢ ∃ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), c • x.2 +ᵥ p ∈ s

Tactic:
apply hv.mp

Premises used: Filter.Frequently.mp
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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
h : ∀ (ht : c ≤ t), (t, u).1 • (t, u).2 +ᵥ p ∈ s → c • (t, u).2 +ᵥ p ∈ s
⊢ c ≤ (t, u).1 → (t, u).1 • (t, u).2 +ᵥ p ∈ s → c • (t, u).2 +ᵥ p ∈ s

Tactic:
(ht : c ≤ t)
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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 : ∀ (h : t • u +ᵥ p ∈ s), c • (t, u).2 +ᵥ p ∈ s
⊢ (t, u).1 • (t, u).2 +ᵥ p ∈ s → c • (t, u).2 +ᵥ p ∈ s

Tactic:
(h : t • u +ᵥ p ∈ s)
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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
h : ∀ (t : k) (u : V) (ht : c ≤ t) (h : t • u +ᵥ p ∈ s), c • (t, u).2 +ᵥ p ∈ s
⊢ ∀ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), x.1 • x.2 +ᵥ p ∈ s → c • x.2 +ᵥ p ∈ s

Tactic:
filter_upwards [tendsto_fst.eventually (eventually_ge_atTop c)]
    with ⟨t, u⟩ (ht : c ≤ t) (h : t • u +ᵥ p ∈ s)

Premises used: Filter.Tendsto.eventually, Filter.eventually_ge_atTop, Filter.tendsto_fst
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : 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
h₁ : c • u +ᵥ p ∈ s
⊢ c • (t, u).2 +ᵥ p ∈ s

Tactic:
change c • u +ᵥ p ∈ s
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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
h₁ : c • u +ᵥ p ∈ segment k p (t • u +ᵥ p)
⊢ c • u +ᵥ p ∈ s

Tactic:
apply hs₁.segment_subset h

Premises used: StarConvex.segment_subset
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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
h₁ : SameRay k (c • u) ((t - c) • u)
⊢ c • u +ᵥ p ∈ segment k p (t • u +ᵥ p)

Tactic:
simp_rw [mem_segment_iff_sameRay, ← vsub_eq_sub, vadd_vsub, vadd_vsub_vadd_cancel_right,
    ← sub_smul]

Premises used: sub_smul, vadd_vsub_vadd_cancel_right, mem_segment_iff_sameRay, vadd_vsub, vsub_eq_sub
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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
⊢ SameRay k (c • u) ((t - c) • u)

Tactic:
(SameRay.sameRay_nonneg_smul_left _ hc).nonneg_smul_right (sub_nonneg.mpr ht)

Premises used: Iff.mpr, SameRay.nonneg_smul_right, SameRay.sameRay_nonneg_smul_left, sub_nonneg
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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
⊢ SameRay k (c • u) ((t - c) • u)

Tactic:
exact (SameRay.sameRay_nonneg_smul_left _ hc).nonneg_smul_right (sub_nonneg.mpr ht)

Premises used: Iff.mpr, SameRay.nonneg_smul_right, SameRay.sameRay_nonneg_smul_left, sub_nonneg
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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₁ : Convex k s
hs₂ : IsClosed[inst_7] s
hc : 0 ≤ c
hv : v ∈ asymptoticCone k s
hp : p ∈ s
⊢ c • v +ᵥ p ∈ s

Tactic:
(hs₁ hp).smul_vadd_mem_of_isClosed_of_mem_asymptoticCone hs₂ hc hv

Premises used: StarConvex.smul_vadd_mem_of_isClosed_of_mem_asymptoticCone
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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)
wlog : ∀ {s : Set V} (hs : Convex k s) (hs' : IsClosed[inst_7] s), Convex k (asymptoticCone k s)
⊢ Convex k (asymptoticCone k s)

Tactic:
wlog hs' : IsClosed s generalizing s

Premises used: IsClosed
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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
inr : Convex k (asymptoticCone k (closure[inst_7] s))
⊢ Convex k (asymptoticCone k s)

Tactic:
rw [← asymptoticCone_closure]

Premises used: asymptoticCone_closure
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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 (closure[inst_7] s))

Tactic:
this hs.closure isClosed_closure

Premises used: Convex.closure, isClosed_closure
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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 (closure[inst_7] s))

Tactic:
exact this hs.closure isClosed_closure

Premises used: Convex.closure, isClosed_closure
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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) ∅)
inr : ∀ (p : V) (hp : p ∈ s), Convex k (asymptoticCone k s)
⊢ Convex k (asymptoticCone k s)

Tactic:
rcases s.eq_empty_or_nonempty with rfl | ⟨p, hp⟩

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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.{u_1, u_2} k (E := V) ∅
hs' : IsClosed[inst_7] ∅
inl : Convex.{u_1, u_2} k (E := V) ∅
⊢ Convex k (asymptoticCone k (P := V) ∅)

Tactic:
rw [asymptoticCone_empty]

Premises used: asymptoticCone_empty
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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.{u_1, u_2} k (E := V) ∅
hs' : IsClosed[inst_7] ∅
⊢ Convex.{u_1, u_2} k (E := V) ∅

Tactic:
convex_empty

Premises used: convex_empty
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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.{u_1, u_2} k (E := V) ∅
hs' : IsClosed[inst_7] ∅
⊢ Convex.{u_1, u_2} k (E := V) ∅

Tactic:
exact convex_empty

Premises used: convex_empty
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ᶠ (p : V) in asymptoticNhds k V (a • v + b • u), p ∈ s

Tactic:
tendsto_id.atTop_smul_const_tendsto_asymptoticNhds _ |>.asymptoticNhds_vadd_const p
    |>.frequently (Eventually.frequently ?_)

Premises used: Filter.tendsto_id, Filter.Tendsto.frequently, Filter.Tendsto.atTop_smul_const_tendsto_asymptoticNhds, Filter.Eventually.frequently, Filter.Tendsto.asymptoticNhds_vadd_const
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
inr : ∀ᶠ (x : k) in atTop, id x • (a • v + b • u) +ᵥ p ∈ s
⊢ ∃ᶠ (p : V) in asymptoticNhds k V (a • v + b • u), p ∈ s

Tactic:
refine tendsto_id.atTop_smul_const_tendsto_asymptoticNhds _ |>.asymptoticNhds_vadd_const p
    |>.frequently (Eventually.frequently ?_)

Premises used: Filter.tendsto_id, Filter.Tendsto.frequently, Filter.Tendsto.atTop_smul_const_tendsto_asymptoticNhds, Filter.Eventually.frequently, Filter.Tendsto.asymptoticNhds_vadd_const
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : ∀ (c : k) (hc : 0 ≤ c), id c • (a • v + b • u) +ᵥ p ∈ s
⊢ ∀ᶠ (x : k) in atTop, id x • (a • v + b • u) +ᵥ p ∈ s

Tactic:
filter_upwards [eventually_ge_atTop 0] with c hc

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : 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
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
h : ((c * a) • v + (c * b) • u) +ᵥ p ∈ s
⊢ id c • (a • v + b • u) +ᵥ p ∈ s

Tactic:
simp_rw [id, smul_add, smul_smul]

Premises used: smul_smul, id, smul_add
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
⊢ c • v +ᵥ p ∈ s

Tactic:
have h₁ : c • v +ᵥ p ∈ s := hs.smul_vadd_mem_of_isClosed_of_mem_asymptoticCone hs' hc hv hp
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
h₁ : c • v +ᵥ p ∈ s
⊢ c • u +ᵥ p ∈ s

Tactic:
have h₂ : c • u +ᵥ p ∈ s := hs.smul_vadd_mem_of_isClosed_of_mem_asymptoticCone hs' hc hu hp
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
h₁ : c • v +ᵥ p ∈ s
h₂ : c • u +ᵥ p ∈ s
h : ((c * a) • v + (c * b) • u) +ᵥ p ∈ [c • v +ᵥ p -[k] c • u +ᵥ p]
⊢ ((c * a) • v + (c * b) • u) +ᵥ p ∈ s

Tactic:
apply hs.segment_subset h₁ h₂

Premises used: Convex.segment_subset
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
h₁ : c • v +ᵥ p ∈ s
h₂ : c • u +ᵥ p ∈ s
h : (c * a) • v + (c * b) • u ∈ [c • v -[k] c • u]
⊢ ((c * a) • v + (c * b) • u) +ᵥ p ∈ [c • v +ᵥ p -[k] c • u +ᵥ p]

Tactic:
rw [← affineSegment_eq_segment, mem_vadd_const_affineSegment, affineSegment_eq_segment]

Premises used: mem_vadd_const_affineSegment, affineSegment_eq_segment
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
h₁ : c • v +ᵥ p ∈ s
h₂ : c • u +ᵥ p ∈ s
h : a • c • v + b • c • u = (c * a) • v + (c * b) • u
⊢ (c * a) • v + (c * b) • u ∈ [c • v -[k] c • u]

Tactic:
exists a, b, ha, hb, hab
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
h₁ : c • v +ᵥ p ∈ s
h₂ : c • u +ᵥ p ∈ s
⊢ a • c • v + b • c • u = (c * a) • v + (c * b) • u

Tactic:
module
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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 : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : v ∈ asymptoticCone k s
⊢ ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s

Tactic:
rw [mem_asymptoticCone_iff, asymptoticNhds_eq_smul_vadd v (c • v +ᵥ p), vadd_pure,
    frequently_map, ← map₂_smul, ← map_prod_eq_map₂, frequently_map] at hv

Premises used: Filter.map₂_smul, Filter.frequently_map, Filter.vadd_pure, HVAdd.hVAdd, Filter.map_prod_eq_map₂, mem_asymptoticCone_iff, HSMul.hSMul, AffineSpace.asymptoticNhds_eq_smul_vadd
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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 : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
⊢ c • v +ᵥ p ∈ s

Tactic:
frequently_const.mp (hv.mp ?_)

Premises used: Filter.frequently_const, Iff.mp, Filter.Frequently.mp
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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 : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
refine : ∀ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), x.1 • x.2 +ᵥ c • v +ᵥ p ∈ s → c • v +ᵥ p ∈ s
⊢ c • v +ᵥ p ∈ s

Tactic:
refine frequently_const.mp (hv.mp ?_)

Premises used: Filter.frequently_const, Iff.mp, Filter.Frequently.mp
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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 : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
⊢ Continuous[inst_7, inst_7] fun (u : V) ↦ -(c • u) +ᵥ c • v +ᵥ p

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
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 : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
⊢ -(c • v) +ᵥ c • v +ᵥ p = p

Tactic:
simp