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
v : V
p : P → Prop
⊢ (∀ᶠ (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
have 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
Tactic: nth_rw 2 [← map_snd_prod (atTop (α := k)) (𝓝 v)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
v : V
p : P → Prop
⊢ (∀ᶠ (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
have 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
Tactic: rw [eventually_map]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
v : V
p : P → Prop
⊢ (∀ᶠ (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
have 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
Tactic: apply eventually_congr
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
v : V
p : P → Prop
c : k
u : V
⊢ 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)
have 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
Tactic: (hc : 0 < c)
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
v : V
p : P → Prop
⊢ ∀ᶠ (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
have 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
Tactic: filter_upwards [tendsto_fst.eventually (eventually_gt_atTop 0)] with ⟨c, u⟩ (hc : 0 < c)
-- 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
s t : Set P
⊢ asymptoticCone k (s ∪ t) = asymptoticCone k s ∪ asymptoticCone k t
have h : ∀ (x : V), x ∈ asymptoticCone k (s ∪ t) ↔ x ∈ asymptoticCone k s ∪ asymptoticCone k t
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
ι : Type u_4
s : Set ι
hs : s.Finite
f : ι → Set P
⊢ asymptoticCone.{u_1, u_2, u_3} k (P := P) (⋃ i ∈ s, f i) = ⋃ i ∈ s, asymptoticCone k (f i)
have 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)
Tactic: induction s, hs using Set.Finite.induction_on
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
ι : Type u_4
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)
⊢ asymptoticCone.{u_1, u_2, u_3} k (P := P) (⋃ i ∈ s, f i) = ⋃ i ∈ s, asymptoticCone k (f i)
have 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 a s, f i) = ⋃ i ∈ insert a s, asymptoticCone k (f i)
Tactic: induction s, hs using Set.Finite.induction_on
Cleared hypotheses: hs
-- 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
S : Set (Set P)
hS : S.Finite
⊢ asymptoticCone k (⋃₀ S) = ⋃ s ∈ S, asymptoticCone k s
have rw : asymptoticCone.{u_1, u_2, u_3} k (P := P) (⋃ i ∈ S, i) = ⋃ s ∈ S, asymptoticCone k s
Tactic: rw [Set.sUnion_eq_biUnion, asymptoticCone_biUnion hS]
-- 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
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
⊢ asymptoticCone k (⋃₀ S) = ⋃ s ∈ S, asymptoticCone k s
have rw₁ : Eq.{u_2 + 1} (α := Set V) (⋃ i ∈ S, asymptoticCone k i) (⋃ s ∈ S, asymptoticCone k s)
Tactic: rw [Set.sUnion_eq_biUnion, asymptoticCone_biUnion hS]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
ι : Type u_4
inst_6 : Finite ι
f : ι → Set P
⊢ asymptoticCone.{u_1, u_2, u_3} k (P := P) (⋃ (i : ι), f i) = ⋃ (i : ι), asymptoticCone k (f i)
have rw : asymptoticCone k (⋃₀ Set.range f) = ⋃ (i : ι), asymptoticCone k (f i)
Tactic: rw [← Set.sUnion_range, asymptoticCone_sUnion (Set.finite_range f), Set.biUnion_range]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
ι : Type u_4
inst_6 : Finite ι
f : ι → Set P
rw : asymptoticCone k (⋃₀ Set.range f) = ⋃ (i : ι), asymptoticCone k (f i)
⊢ asymptoticCone.{u_1, u_2, u_3} k (P := P) (⋃ (i : ι), f i) = ⋃ (i : ι), asymptoticCone k (f i)
have rw₁ : Eq.{u_2 + 1} (α := Set V) (⋃ s ∈ Set.range f, asymptoticCone k s) (⋃ (i : ι), asymptoticCone k (f i))
Tactic: rw [← Set.sUnion_range, asymptoticCone_sUnion (Set.finite_range f), Set.biUnion_range]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
ι : Type u_4
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))
⊢ asymptoticCone.{u_1, u_2, u_3} k (P := P) (⋃ (i : ι), f i) = ⋃ (i : ι), asymptoticCone k (f i)
have rw₂ : Eq.{u_2 + 1} (α := Set V) (⋃ (y : ι), asymptoticCone k (f y)) (⋃ (i : ι), asymptoticCone k (f i))
Tactic: rw [← Set.sUnion_range, asymptoticCone_sUnion (Set.finite_range f), Set.biUnion_range]
-- 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
⊢ 0 ∈ asymptoticCone k s ↔ s.Nonempty
have refine_1 : ¬s.Nonempty → 0 ∉ asymptoticCone k s
Tactic: refine ⟨Function.mtr ?_, fun _ => ?_⟩
-- 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
refine_1 : ¬s.Nonempty → 0 ∉ asymptoticCone k s
⊢ 0 ∈ asymptoticCone k s ↔ s.Nonempty
have refine_2 : s.Nonempty → 0 ∈ asymptoticCone k s
Tactic: refine ⟨Function.mtr ?_, fun _ => ?_⟩
-- 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 s).Nonempty ↔ s.Nonempty
have refine : ¬s.Nonempty → ¬(asymptoticCone k s).Nonempty
Tactic: refine ⟨Function.mtr ?_, fun h => ⟨0, zero_mem_asymptoticCone.mpr 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
c : k
v : V
hc : 0 ≤ c
h : v ∈ asymptoticCone k s
⊢ c • v ∈ asymptoticCone k s
have inl : ∀ (hc : LE.le.{u_1} (α := k) 0 0), HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 v ∈ asymptoticCone k s
Tactic: rcases hc.eq_or_lt with rfl | hc
Cleared hypotheses: c, hc
-- 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
c : k
v : V
hc : 0 ≤ c
h : v ∈ asymptoticCone k s
inl : ∀ (hc : LE.le.{u_1} (α := k) 0 0), HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 v ∈ asymptoticCone k s
⊢ c • v ∈ asymptoticCone k s
have inr : ∀ (hc : 0 < c), c • v ∈ asymptoticCone k s
Tactic: rcases hc.eq_or_lt with rfl | hc
-- 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
v : V
h : v ∈ asymptoticCone k s
hc : LE.le.{u_1} (α := k) 0 0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := k) 0 v ∈ asymptoticCone k s
have inl : (asymptoticCone k s).Nonempty
Tactic: rw [zero_smul, zero_mem_asymptoticCone, ← asymptoticCone_nonempty (k := k)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s
⊢ asymptoticCone k s = closure[inst_4] s
have h : ∀ (v : V), v ∈ asymptoticCone k s ↔ v ∈ closure[inst_4] s
Tactic: ext v
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s
v : V
⊢ v ∈ asymptoticCone k s ↔ v ∈ closure[inst_4] s
have h : (∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 ∈ s) ↔
  ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.2 ∈ s
Tactic: rw [mem_closure_iff_frequently, ← map_snd_prod (atTop (α := k)) (𝓝 v), frequently_map,
    mem_asymptoticCone_iff, asymptoticNhds_eq_smul, ← map₂_smul, ← map_prod_eq_map₂, frequently_map]
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s
v : V
⊢ (∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.1 • a.2 ∈ s) ↔
    ∃ᶠ (a : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), a.2 ∈ s
have h : ∀ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), x.1 • x.2 ∈ s ↔ x.2 ∈ s
Tactic: apply frequently_congr
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s
v : V
⊢ ∀ᶠ (x : k × V) in SProd.sprod (α := Filter k) atTop (𝓝 v), x.1 • x.2 ∈ s ↔ x.2 ∈ s
have h : ∀ (c : k) (u : V) (hc : 0 < (c, u).1), (c, u).1 • (c, u).2 ∈ s ↔ (c, u).2 ∈ s
Tactic: filter_upwards [tendsto_fst.eventually (eventually_gt_atTop 0)] with ⟨c, u⟩ hc
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s
v : V
c : k
u : V
hc : 0 < (c, u).1
⊢ (c, u).1 • (c, u).2 ∈ s ↔ (c, u).2 ∈ s
have h : ∀ (hu : (c, u).1 • (c, u).2 ∈ s), (c, u).2 ∈ s
Tactic: refine ⟨fun hu => ?_, hs c hc u⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (hypothesis)
Goal:
k : Type u_1
V : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : TopologicalSpace V
inst_5 : TopologicalSpace k
inst_6 : OrderTopology k
inst_7 : IsStrictOrderedRing k
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul k V
s : Set V
hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s
v : V
c : k
u : V
hc : 0 < (c, u).1
hu : (c, u).1 • (c, u).2 ∈ s
⊢ (c, u).2 ∈ s
have hs₁ : c⁻¹ • c • u ∈ s
Tactic: specialize hs c⁻¹ (inv_pos_of_pos hc) (c • u) hu
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 : 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
s : Set V
v : V
c : k
u : V
hc : 0 < (c, u).1
hu : (c, u).1 • (c, u).2 ∈ s
hs : c⁻¹ • c • u ∈ s
⊢ (c, u).2 ∈ s
have h : ∀ (hs : u ∈ s), (c, u).2 ∈ s
Tactic: rwa [inv_smul_smul₀ hc.ne'] at hs
Cleared hypotheses: hs
-- 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
⊢ asymptoticCone k (↑s : Set P) = closure[inst_5] (↑s.direction : Set V)
have have : ∀ (p : P) (hp : p ∈ (↑s : Set P)), asymptoticCone k (↑s : Set P) = closure[inst_5] (↑s.direction : Set V)
Tactic: have ⟨p, hp⟩ := hs
-- 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)
⊢ asymptoticCone k (↑s : Set P) = closure[inst_5] (↑s.direction : Set V)
have h : ∀ (v : V), v ∈ asymptoticCone k (↑s : Set P) ↔ v ∈ closure[inst_5] (↑s.direction : Set V)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Topology.Algebra.AsymptoticCone (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
inst_6 : TopologicalSpace k
inst_7 : OrderTopology k
inst_8 : IsStrictOrderedRing k
inst_9 : IsTopologicalAddGroup V
inst_10 : ContinuousSMul k V
s : AffineSubspace k P
hs : (↑s : Set P).Nonempty
p : P
hp : p ∈ (↑s : Set P)
v : V
⊢ v ∈ asymptoticCone k (↑s : Set P) ↔ v ∈ closure[inst_5] (↑s.direction : Set V)
have h : v ∈ asymptoticCone k (↑s : Set P) ↔ v ∈ asymptoticCone k (↑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)
⊢ v ∈ asymptoticCone k (↑s : Set P) ↔ v ∈ closure[inst_5] (↑s.direction : Set V)
have h₁ : (∃ᶠ (p : P) in asymptoticNhds k P v, 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)
⊢ v ∈ asymptoticCone k (↑s : Set P) ↔ v ∈ closure[inst_5] (↑s.direction : Set V)
have 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)
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)
⊢ v ∈ asymptoticCone k (↑s : Set P) ↔ v ∈ closure[inst_5] (↑s.direction : Set V)
have 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)
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]