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
c : k
hc : 0 < c
p : P
simp_rw :
  HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 (c • v))) (pure p) =
    HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)
simp_rw₁ :
  HVAdd.hVAdd (β := Filter P)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) (β := Filter V) atTop (map (fun (x : V) ↦ c • x) (𝓝 v))) (pure p) =
    HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)
simp_rw₂ :
  HVAdd.hVAdd (α := Filter V) (β := Filter P)
      (map₂ (fun (x1 : k) (x2 : V) ↦ x1 • x2) atTop (map (fun (x : V) ↦ c • x) (𝓝 v))) (pure p) =
    HVAdd.hVAdd (α := Filter V) (β := Filter P) (map₂ (fun (x1 : k) (x2 : V) ↦ x1 • x2) atTop (𝓝 v)) (pure p)
simp_rw₃ :
  HVAdd.hVAdd (α := Filter V) (β := Filter P) (map₂ (fun (a : k) (b : V) ↦ a • c • b) atTop (𝓝 v)) (pure p) =
    HVAdd.hVAdd (α := Filter V) (β := Filter P) (map₂ (fun (x1 : k) (x2 : V) ↦ x1 • x2) atTop (𝓝 v)) (pure p)
⊢ asymptoticNhds k P (c • v) = asymptoticNhds k P v
have simp_rw₄ : HVAdd.hVAdd (α := Filter V) (β := Filter P) (map₂ (fun (a : k) (b : V) ↦ (a * c) • b) atTop (𝓝 v)) (pure p) =
  HVAdd.hVAdd (α := Filter V) (β := Filter P) (map₂ (fun (x1 : k) (x2 : V) ↦ x1 • x2) atTop (𝓝 v)) (pure p)
Tactic: simp_rw [asymptoticNhds_eq_smul_vadd _ p,
    ← show map (c • ·) (𝓝 v) = 𝓝 (c • v) from
      (Homeomorph.smulOfNeZero c hc.ne').map_nhds_eq v,
    ← map₂_smul, map₂_map_right, smul_smul, ← map₂_map_left,
    show map (· * c) atTop = atTop from (OrderIso.mulRight₀ _ hc).map_atTop]
-- 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
c : k
hc : 0 < c
p : P
simp_rw :
  HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 (c • v))) (pure p) =
    HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)
simp_rw₁ :
  HVAdd.hVAdd (β := Filter P)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) (β := Filter V) atTop (map (fun (x : V) ↦ c • x) (𝓝 v))) (pure p) =
    HVAdd.hVAdd (β := Filter P) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)) (pure p)
simp_rw₂ :
  HVAdd.hVAdd (α := Filter V) (β := Filter P)
      (map₂ (fun (x1 : k) (x2 : V) ↦ x1 • x2) atTop (map (fun (x : V) ↦ c • x) (𝓝 v))) (pure p) =
    HVAdd.hVAdd (α := Filter V) (β := Filter P) (map₂ (fun (x1 : k) (x2 : V) ↦ x1 • x2) atTop (𝓝 v)) (pure p)
simp_rw₃ :
  HVAdd.hVAdd (α := Filter V) (β := Filter P) (map₂ (fun (a : k) (b : V) ↦ a • c • b) atTop (𝓝 v)) (pure p) =
    HVAdd.hVAdd (α := Filter V) (β := Filter P) (map₂ (fun (x1 : k) (x2 : V) ↦ x1 • x2) atTop (𝓝 v)) (pure p)
simp_rw₄ :
  HVAdd.hVAdd (α := Filter V) (β := Filter P) (map₂ (fun (a : k) (b : V) ↦ (a * c) • b) atTop (𝓝 v)) (pure p) =
    HVAdd.hVAdd (α := Filter V) (β := Filter P) (map₂ (fun (x1 : k) (x2 : V) ↦ x1 • x2) atTop (𝓝 v)) (pure p)
⊢ asymptoticNhds k P (c • v) = asymptoticNhds k P v
have simp_rw₅ : HVAdd.hVAdd (β := Filter P) (map₂.{u_1, u_2, u_2} (α := k) HSMul.hSMul (map (fun (a : k) ↦ a * c) atTop) (𝓝 v))
    (pure p) =
  HVAdd.hVAdd (α := Filter V) (β := Filter P) (map₂ (fun (x1 : k) (x2 : V) ↦ x1 • x2) atTop (𝓝 v)) (pure p)
Tactic: simp_rw [asymptoticNhds_eq_smul_vadd _ p,
    ← show map (c • ·) (𝓝 v) = 𝓝 (c • v) from
      (Homeomorph.smulOfNeZero c hc.ne').map_nhds_eq v,
    ← map₂_smul, map₂_map_right, smul_smul, ← map₂_map_left,
    show map (· * c) atTop = atTop from (OrderIso.mulRight₀ _ hc).map_atTop]
-- 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
⊢ (𝓝 v).bind (asymptoticNhds k P) = asymptoticNhds k P v
have a : (𝓝 v).bind (asymptoticNhds k P) ≤ asymptoticNhds k P v
Tactic: apply le_antisymm
-- 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
a : (𝓝 v).bind (asymptoticNhds k P) ≤ asymptoticNhds k P v
⊢ (𝓝 v).bind (asymptoticNhds k P) = asymptoticNhds k P v
have a₁ : asymptoticNhds k P v ≤ (𝓝 v).bind (asymptoticNhds k P)
Tactic: apply le_antisymm
-- 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
⊢ (𝓝 v).bind (asymptoticNhds k P) ≤ asymptoticNhds k P v
have a : ∀ (p : P), (𝓝 v).bind (asymptoticNhds k P) ≤ asymptoticNhds k P v
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
v : V
p : P
⊢ ((𝓝 v).bind fun (v : V) ↦ asymptoticNhds k P v) ≤ asymptoticNhds k P v
have a : LE.le.{u_3} (α := Filter P)
  ((𝓝 v).bind fun (v : V) ↦ map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
  (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
Tactic: simp_rw [asymptoticNhds_eq_smul_vadd _ p, vadd_pure]
-- 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
⊢ LE.le.{u_3} (α := Filter P)
    ((𝓝 v).bind fun (v : V) ↦ map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
    (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
have a : LE.le.{u_3} (α := Filter P)
  ((𝓝 v).bind fun (v : V) ↦ map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
  (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop ((𝓝 v).bind 𝓝)))
Tactic: nth_rw 2 [← nhds_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
v : V
p : P
⊢ LE.le.{u_3} (α := Filter P)
    ((𝓝 v).bind fun (v : V) ↦ map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
    (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop ((𝓝 v).bind 𝓝)))
have a : ∀ (x : Set P),
  (∃ (s : Set k),
      Membership.mem (γ := Filter k) atTop s ∧
        ∃ (t : Set V),
          (∃ t_1 ∈ 𝓝 v, ∀ x ∈ t_1, t ∈ 𝓝 x) ∧
            Subset (α := Set V) (Set.image2 (fun (x1 : k) (x2 : V) ↦ x1 • x2) s t) ((fun (x : V) ↦ x +ᵥ p) ⁻¹' x)) →
    ∃ t ∈ 𝓝 v,
      ∀ x_1 ∈ t,
        ∃ (s : Set k),
          Membership.mem (γ := Filter k) atTop s ∧
            ∃ t ∈ 𝓝 x_1,
              Subset (α := Set V) (Set.image2 (fun (x1 : k) (x2 : V) ↦ x1 • x2) s t) ((fun (x : V) ↦ x +ᵥ p) ⁻¹' x)
Tactic: simp only [le_def, mem_map, ← map₂_smul, mem_map₂_iff, mem_bind]
-- 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
v : V
⊢ (asymptoticNhds k P v).bind 𝓝 = asymptoticNhds k P v
have refine : ∀ (s : Set P) (h : s ∈ asymptoticNhds k P v), s ∈ (asymptoticNhds k P v).bind 𝓝
Tactic: refine le_antisymm (fun s h => ?_) (bind_mono le_rfl (.of_forall pure_le_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
v : V
s : Set P
h : s ∈ asymptoticNhds k P v
⊢ s ∈ (asymptoticNhds k P v).bind 𝓝
have have : ∀ (p : P), s ∈ (asymptoticNhds k P v).bind 𝓝
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
inst_11 : TopologicalSpace P
inst_12 : IsTopologicalAddTorsor P
v : V
s : Set P
h : s ∈ asymptoticNhds k P v
p : P
⊢ s ∈ (asymptoticNhds k P v).bind 𝓝
have rw : ∀
  (h :
    Membership.mem (γ := Filter P)
      (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v))) s),
  Membership.mem (γ := Filter P)
    (Filter.bind (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v))) 𝓝) s
Tactic: rw [asymptoticNhds_eq_smul_vadd _ p, vadd_pure] at h ⊢
Cleared hypotheses: h
-- 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
inst_11 : TopologicalSpace P
inst_12 : IsTopologicalAddTorsor P
v : V
s : Set P
p : P
h :
  Membership.mem (γ := Filter P) (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
    s
⊢ Membership.mem (γ := Filter P)
    (Filter.bind (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v))) 𝓝) s
have h₁ : Membership.mem (γ := Filter P)
  (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop ((𝓝 v).bind 𝓝))) s
Tactic: rw [← nhds_bind_nhds] 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
inst_11 : TopologicalSpace P
inst_12 : IsTopologicalAddTorsor P
v : V
s : Set P
p : P
h :
  Membership.mem (γ := Filter P)
    (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop ((𝓝 v).bind 𝓝))) s
⊢ 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
have obtain : ∀ (t₁ : Set k) (ht₁ : Membership.mem (γ := Filter k) atTop t₁) (t₂ : Set V) (ht₂ : t₂ ∈ (𝓝 v).bind 𝓝)
  (hs : t₁ • t₂ ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s),
  Membership.mem (γ := Filter P)
    (Filter.bind (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v))) 𝓝) s
Tactic: obtain ⟨t₁, ht₁, t₂, ht₂, hs⟩ := h
Cleared hypotheses: h
-- 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
inst_11 : TopologicalSpace P
inst_12 : IsTopologicalAddTorsor P
v : V
s : Set P
p : P
t₁ : Set k
ht₁ : Membership.mem (γ := Filter k) atTop t₁
t₂ : Set V
ht₂ : t₂ ∈ (𝓝 v).bind 𝓝
hs : t₁ • t₂ ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
⊢ 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
have ht₃ : ∃ t ∈ 𝓝 v, ∀ x ∈ t, t₂ ∈ 𝓝 x
Tactic: rw [mem_bind] at ht₂
Cleared hypotheses: ht₂, 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
inst_11 : TopologicalSpace P
inst_12 : IsTopologicalAddTorsor P
v : V
s : Set P
p : P
t₁ : Set k
ht₁ : Membership.mem (γ := Filter k) atTop t₁
t₂ : Set V
ht₂ : ∃ t ∈ 𝓝 v, ∀ x ∈ t, t₂ ∈ 𝓝 x
hs : t₁ • t₂ ⊆ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s
⊢ 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
have obtain : ∀ (t₃ : Set V) (ht₃ : t₃ ∈ 𝓝 v) (ht₂ : ∀ x ∈ t₃, t₂ ∈ 𝓝 x),
  Membership.mem (γ := Filter P)
    (Filter.bind (map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v))) 𝓝) s
Tactic: obtain ⟨t₃, ht₃, ht₂⟩ := ht₂
Cleared hypotheses: ht₂
-- 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
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
⊢ 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
have 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
Tactic: rw [bind_map, mem_bind]
-- 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
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
have 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
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 => ?_⟩
-- 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
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
⊢ Membership.mem (γ := Filter P) ((𝓝 ∘ fun (x : V) ↦ x +ᵥ p) (c • u)) s
have 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))
Tactic: rw [show s = (· -ᵥ p) ⁻¹' ((· +ᵥ p) ⁻¹' s) by simp [Set.preimage_preimage]]
-- 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
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
⊢ 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))
have a : (fun (x : V) ↦ x +ᵥ p) ⁻¹' s ∈ 𝓝 ((fun (x : V) ↦ x +ᵥ p) (c • u) -ᵥ p)
Tactic: apply tendsto_id.vsub tendsto_const_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
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
⊢ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s ∈ 𝓝 ((fun (x : V) ↦ x +ᵥ p) (c • u) -ᵥ p)
have a : (fun (x : V) ↦ x +ᵥ p) ⁻¹' s ∈ 𝓝 (c • u)
Tactic: rw [vadd_vsub]
-- 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
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
⊢ (fun (x : V) ↦ x +ᵥ p) ⁻¹' s ∈ 𝓝 (c • u)
have h : ∀ a ∈ c • t₂, Membership.mem (γ := Set V) ((fun (x : V) ↦ x +ᵥ p) ⁻¹' s) a
Tactic: filter_upwards [smul_mem_nhds_smul₀ hc₂.ne' (ht₂ u hu)]
-- 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
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 ∈ c • t₂, Membership.mem (γ := Set V) ((fun (x : V) ↦ x +ᵥ p) ⁻¹' s) a
have h : ∀ ⦃x : V⦄, x ∈ t₂ → Membership.mem (γ := Set V) ((fun (x : V) ↦ x +ᵥ p) ⁻¹' s) (c • x)
Tactic: rw [← Set.image_smul, Set.forall_mem_image]
-- 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
⊢ (asymptoticNhds k V v).bind (asymptoticNhds k P) = asymptoticNhds k P v
have 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
Tactic: refine Filter.ext' fun p => ?_
-- 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 : P) in (asymptoticNhds k V v).bind (asymptoticNhds k P), p x) ↔ ∀ᶠ (x : P) in asymptoticNhds k P v, p x
have 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
Tactic: rw [asymptoticNhds_eq_smul, eventually_bind, ← map₂_smul, ← map_prod_eq_map₂, eventually_map,
    ← nhds_bind_asymptoticNhds, eventually_bind]