awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R_1 : Type u
inst : Ring R_1
B_1 : RingFilterBasis R_1
R : Type u
inst_1 : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this_1 : TopologicalSpace R := B'.topology
basis : HasBasis (𝓝 0) (fun (V : Set R) ↦ V ∈ B') id
basis' :
  (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)).HasBasis (fun (i : Set R × Set R) ↦ i.1 ∈ B' ∧ i.2 ∈ B')
    fun (i : Set R × Set R) ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
hmul :
  Tendsto (β := R) (uncurry fun (x1 x2 : R) ↦ x1 * x2) (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x₀ * x) (𝓝 0) (𝓝 0)
⊢ IsTopologicalRing R
have hmul_right : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x * x₀) (𝓝 0) (𝓝 0)
Tactic: apply IsTopologicalRing.of_addGroup_of_nhds_zero
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R_1 : Type u
inst : Ring R_1
B_1 : RingFilterBasis R_1
R : Type u
inst_1 : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this_1 : TopologicalSpace R := B'.topology
basis : HasBasis (𝓝 0) (fun (V : Set R) ↦ V ∈ B') id
basis' :
  (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)).HasBasis (fun (i : Set R × Set R) ↦ i.1 ∈ B' ∧ i.2 ∈ B')
    fun (i : Set R × Set R) ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ Tendsto (β := R) (uncurry fun (x1 x2 : R) ↦ x1 * x2) (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)
have hmul : ∀ ib ∈ B',
  ∃ (ia : Set R × Set R),
    (ia.1 ∈ B' ∧ ia.2 ∈ B') ∧ ∀ x ∈ id ia.1 ×ˢ id ia.2, uncurry (fun (x1 x2 : R) ↦ x1 * x2) x ∈ id ib
Tactic: rw [basis'.tendsto_iff basis]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R_1 : Type u
inst : Ring R_1
B_1 : RingFilterBasis R_1
R : Type u
inst_1 : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this_1 : TopologicalSpace R := B'.topology
basis : HasBasis (𝓝 0) (fun (V : Set R) ↦ V ∈ B') id
basis' :
  (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)).HasBasis (fun (i : Set R × Set R) ↦ i.1 ∈ B' ∧ i.2 ∈ B')
    fun (i : Set R × Set R) ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
⊢ ∀ ib ∈ B',
    ∃ (ia : Set R × Set R),
      (ia.1 ∈ B' ∧ ia.2 ∈ B') ∧ ∀ x ∈ id ia.1 ×ˢ id ia.2, uncurry (fun (x1 x2 : R) ↦ x1 * x2) x ∈ id ib
have hmul : ∀ U ∈ B', ∃ (V : Set R) (W : Set R), (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U
Tactic: suffices ∀ U ∈ B', ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ a b, a ∈ V → b ∈ W → a * b ∈ U by simpa
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R_1 : Type u
inst : Ring R_1
B_1 : RingFilterBasis R_1
R : Type u
inst_1 : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this_1 : TopologicalSpace R := B'.topology
basis : HasBasis (𝓝 0) (fun (V : Set R) ↦ V ∈ B') id
basis' :
  (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)).HasBasis (fun (i : Set R × Set R) ↦ i.1 ∈ B' ∧ i.2 ∈ B')
    fun (i : Set R × Set R) ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
U : Set R
U_in : U ∈ B'
⊢ ∃ (V : Set R) (W : Set R), (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U
have hmul : ∀ (V : Set R) (V_in : V ∈ B) (hV : V * V ⊆ U),
  ∃ (V : Set R) (W : Set R), (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U
Tactic: rcases B.mul U_in with ⟨V, V_in, hV⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R_1 : Type u
inst : Ring R_1
B_1 : RingFilterBasis R_1
R : Type u
inst_1 : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this_1 : TopologicalSpace R := B'.topology
basis : HasBasis (𝓝 0) (fun (V : Set R) ↦ V ∈ B') id
basis' :
  (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)).HasBasis (fun (i : Set R × Set R) ↦ i.1 ∈ B' ∧ i.2 ∈ B')
    fun (i : Set R × Set R) ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
U : Set R
U_in : U ∈ B'
V : Set R
V_in : V ∈ B
hV : V * V ⊆ U
⊢ ∃ (V : Set R) (W : Set R), (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U
have hmul : ∀ (a b : R), a ∈ V → b ∈ V → a * b ∈ U
Tactic: refine ⟨V, V, ⟨V_in, V_in⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R_1 : Type u
inst : Ring R_1
B_1 : RingFilterBasis R_1
R : Type u
inst_1 : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this_1 : TopologicalSpace R := B'.topology
basis : HasBasis (𝓝 0) (fun (V : Set R) ↦ V ∈ B') id
basis' :
  (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)).HasBasis (fun (i : Set R × Set R) ↦ i.1 ∈ B' ∧ i.2 ∈ B')
    fun (i : Set R × Set R) ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
x₀ : R
⊢ Tendsto (β := R) (fun (x : R) ↦ x₀ * x) (𝓝 0) (𝓝 0)
have hmul_left : ∀ ib ∈ B', ∃ ia ∈ B', ∀ x ∈ id ia, x₀ * x ∈ id ib
Tactic: rw [basis.tendsto_iff basis]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R_1 : Type u
inst : Ring R_1
B_1 : RingFilterBasis R_1
R : Type u
inst_1 : Ring R
B : RingFilterBasis R
B' : AddGroupFilterBasis R := toAddGroupFilterBasis
this_1 : TopologicalSpace R := B'.topology
basis : HasBasis (𝓝 0) (fun (V : Set R) ↦ V ∈ B') id
basis' :
  (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)).HasBasis (fun (i : Set R × Set R) ↦ i.1 ∈ B' ∧ i.2 ∈ B')
    fun (i : Set R × Set R) ↦ id i.1 ×ˢ id i.2
this : IsTopologicalAddGroup R
x₀ : R
⊢ Tendsto (β := R) (fun (x : R) ↦ x * x₀) (𝓝 0) (𝓝 0)
have hmul_right : ∀ ib ∈ B', ∃ ia ∈ B', ∀ x ∈ id ia, x * x₀ ∈ id ib
Tactic: rw [basis.tendsto_iff basis]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
B : ModuleFilterBasis R M
inst_4 : DiscreteTopology R
⊢ ∃ (V : Set R),
    Membership.mem (γ := Filter R) (𝓝 0) V ∧
      ∃ (W : Set M),
        Membership.mem (γ := Set (Set M))
            (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) W ∧
          V • W ⊆ {0}
have right : HSMul.hSMul.{u_1, u_2, u_2} (α := Set R) (β := Set M) univ {0} ⊆ {0}
Tactic: use univ, univ_mem, {0}, rfl
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
B : ModuleFilterBasis R M
inst_4 : DiscreteTopology R
x₀ : R
U : Set M
h : Membership.mem (γ := Set (Set M)) {{0}} U
⊢ ∃ (V : Set M),
    Membership.mem (γ := Set (Set M))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (x : M) ↦ x₀ • x) ⁻¹' U
have h₁ : U = {0}
Tactic: rw [mem_singleton_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
B : ModuleFilterBasis R M
inst_4 : DiscreteTopology R
x₀ : R
U : Set M
h : U = {0}
⊢ ∃ (V : Set M),
    Membership.mem (γ := Set (Set M))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (x : M) ↦ x₀ • x) ⁻¹' U
have right : Subset (α := Set M) {0} ((fun (x : M) ↦ x₀ • x) ⁻¹' U)
Tactic: use {0}, rfl
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
B : ModuleFilterBasis R M
inst_4 : DiscreteTopology R
m₀ : M
U : Set M
h : Membership.mem (γ := Set (Set M)) 0 U
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U
have h₁ : U = 0
Tactic: rw [Set.mem_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
ι : Type u_3
inst_4 : IsTopologicalRing R
inst_5 : TopologicalSpace M
inst_6 : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ (V : Set R), Membership.mem (γ := Filter R) (𝓝 0) V ∧ ∃ (j : ι), p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ (j : ι), p j ∧ MapsTo (fun (x : M) ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ ContinuousSMul R M
have hmul : Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (SProd.sprod (α := Filter R) (β := Filter M) (𝓝 0) (𝓝 0)) (𝓝 0)
Tactic: apply ContinuousSMul.of_nhds_zero
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
ι : Type u_3
inst_4 : IsTopologicalRing R
inst_5 : TopologicalSpace M
inst_6 : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ (V : Set R), Membership.mem (γ := Filter R) (𝓝 0) V ∧ ∃ (j : ι), p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ (j : ι), p j ∧ MapsTo (fun (x : M) ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
hmul : Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (SProd.sprod (α := Filter R) (β := Filter M) (𝓝 0) (𝓝 0)) (𝓝 0)
⊢ ContinuousSMul R M
have hmulleft : ∀ (m : M), Tendsto.{u_1, u_2} (β := M) (fun (a : R) ↦ a • m) (𝓝 0) (𝓝 0)
Tactic: apply ContinuousSMul.of_nhds_zero
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
ι : Type u_3
inst_4 : IsTopologicalRing R
inst_5 : TopologicalSpace M
inst_6 : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ (V : Set R), Membership.mem (γ := Filter R) (𝓝 0) V ∧ ∃ (j : ι), p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ (j : ι), p j ∧ MapsTo (fun (x : M) ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
hmul : Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (SProd.sprod (α := Filter R) (β := Filter M) (𝓝 0) (𝓝 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto.{u_1, u_2} (β := M) (fun (a : R) ↦ a • m) (𝓝 0) (𝓝 0)
⊢ ContinuousSMul R M
have hmulright : ∀ (a : R), Tendsto (β := M) (fun (m : M) ↦ a • m) (𝓝 0) (𝓝 0)
Tactic: apply ContinuousSMul.of_nhds_zero
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
ι : Type u_3
inst_4 : IsTopologicalRing R
inst_5 : TopologicalSpace M
inst_6 : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ (V : Set R), Membership.mem (γ := Filter R) (𝓝 0) V ∧ ∃ (j : ι), p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ (j : ι), p j ∧ MapsTo (fun (x : M) ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (SProd.sprod (α := Filter R) (β := Filter M) (𝓝 0) (𝓝 0)) (𝓝 0)
have hmul : ∀ (i : ι), p i → ∀ᶠ (x : R × M) in SProd.sprod (α := Filter R) (β := Filter M) (𝓝 0) (𝓝 0), x.1 • x.2 ∈ b i
Tactic: rw [h.tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
ι : Type u_3
inst_4 : IsTopologicalRing R
inst_5 : TopologicalSpace M
inst_6 : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ (V : Set R), Membership.mem (γ := Filter R) (𝓝 0) V ∧ ∃ (j : ι), p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ (j : ι), p j ∧ MapsTo (fun (x : M) ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
i : ι
hi : p i
⊢ ∀ᶠ (x : R × M) in SProd.sprod (α := Filter R) (β := Filter M) (𝓝 0) (𝓝 0), x.1 • x.2 ∈ b i
have hmul : ∀ (V : Set R) (V_in : Membership.mem (γ := Filter R) (𝓝 0) V) (j : ι) (hj : p j) (hVj : V • b j ⊆ b i),
  ∀ᶠ (x : R × M) in SProd.sprod (α := Filter R) (β := Filter M) (𝓝 0) (𝓝 0), x.1 • x.2 ∈ b i
Tactic: rcases hsmul hi with ⟨V, V_in, j, hj, hVj⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
ι : Type u_3
inst_4 : IsTopologicalRing R
inst_5 : TopologicalSpace M
inst_6 : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ (V : Set R), Membership.mem (γ := Filter R) (𝓝 0) V ∧ ∃ (j : ι), p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ (j : ι), p j ∧ MapsTo (fun (x : M) ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
i : ι
hi : p i
V : Set R
V_in : Membership.mem (γ := Filter R) (𝓝 0) V
j : ι
hj : p j
hVj : V • b j ⊆ b i
⊢ ∀ᶠ (x : R × M) in SProd.sprod (α := Filter R) (β := Filter M) (𝓝 0) (𝓝 0), x.1 • x.2 ∈ b i
have hmul : V ×ˢ b j ⊆ {x : R × M | (fun (x : R × M) ↦ x.1 • x.2 ∈ b i) x}
Tactic: apply mem_of_superset (prod_mem_prod V_in <| h.mem_of_mem hj)
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
ι : Type u_3
inst_4 : IsTopologicalRing R
inst_5 : TopologicalSpace M
inst_6 : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ (V : Set R), Membership.mem (γ := Filter R) (𝓝 0) V ∧ ∃ (j : ι), p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ (j : ι), p j ∧ MapsTo (fun (x : M) ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
m₀ : M
⊢ Tendsto.{u_1, u_2} (β := M) (fun (a : R) ↦ a • m₀) (𝓝 0) (𝓝 0)
have hmulleft : ∀ (i : ι), p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
Tactic: rw [h.tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
ι : Type u_3
inst_4 : IsTopologicalRing R
inst_5 : TopologicalSpace M
inst_6 : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ (V : Set R), Membership.mem (γ := Filter R) (𝓝 0) V ∧ ∃ (j : ι), p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ (j : ι), p j ∧ MapsTo (fun (x : M) ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
x₀ : R
⊢ Tendsto (β := M) (fun (m : M) ↦ x₀ • m) (𝓝 0) (𝓝 0)
have hmulright : ∀ (i : ι), p i → ∀ᶠ (x : M) in 𝓝 0, x₀ • x ∈ b i
Tactic: rw [h.tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
ι : Type u_3
inst_4 : IsTopologicalRing R
inst_5 : TopologicalSpace M
inst_6 : IsTopologicalAddGroup M
p : ι → Prop
b : ι → Set M
h : HasBasis (𝓝 0) p b
hsmul : ∀ {i : ι}, p i → ∃ (V : Set R), Membership.mem (γ := Filter R) (𝓝 0) V ∧ ∃ (j : ι), p j ∧ V • b j ⊆ b i
hsmul_left : ∀ (x₀ : R) {i : ι}, p i → ∃ (j : ι), p j ∧ MapsTo (fun (x : M) ↦ x₀ • x) (b j) (b i)
hsmul_right : ∀ (m₀ : M) {i : ι}, p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
x₀ : R
i : ι
hi : p i
⊢ ∀ᶠ (x : M) in 𝓝 0, x₀ • x ∈ b i
have hmulright : ∀ (j : ι) (hj : p j) (hji : MapsTo (fun (x : M) ↦ x₀ • x) (b j) (b i)), ∀ᶠ (x : M) in 𝓝 0, x₀ • x ∈ b i
Tactic: rcases hsmul_left x₀ hi with ⟨j, hj, hji⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
B : ModuleFilterBasis R M
inst_4 : IsTopologicalRing R
B' : AddGroupFilterBasis M := B.toAddGroupFilterBasis
x : TopologicalSpace M := B'.topology
⊢ ContinuousSMul R M
have x : IsTopologicalAddGroup M
Tactic: have _ := B'.isTopologicalAddGroup
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
inst : CommRing R_1
inst_1 : TopologicalSpace R_1
inst_2 : AddCommGroup M_1
inst_3 : Module R_1 M_1
B : ModuleFilterBasis R_1 M_1
R : Type u_3
M : Type u_4
inst_4 : CommRing R
inst_5 : AddCommGroup M
inst_6 : Module R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun (x : M) ↦ x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun (x : R) ↦ x • m₀) ⁻¹' U
x : TopologicalSpace R := BR.topology
U : Set M
U_in :
  Membership.mem (γ := Set (Set M)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    U
⊢ ∃ (V : Set R),
    Membership.mem (γ := Filter R) (𝓝 0) V ∧
      ∃ (W : Set M),
        Membership.mem (γ := Set (Set M))
            (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) W ∧
          V • W ⊆ U
have rcases : ∀ (V : Set R) (V_in : V ∈ BR) (W : Set M) (W_in : W ∈ BM) (H : V • W ⊆ U),
  ∃ (V : Set R),
    Membership.mem (γ := Filter R) (𝓝 0) V ∧
      ∃ (W : Set M),
        Membership.mem (γ := Set (Set M))
            (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) W ∧
          V • W ⊆ U
Tactic: rcases smul U_in with ⟨V, V_in, W, W_in, H⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.FilterBasis (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
inst : CommRing R_1
inst_1 : TopologicalSpace R_1
inst_2 : AddCommGroup M_1
inst_3 : Module R_1 M_1
B : ModuleFilterBasis R_1 M_1
R : Type u_3
M : Type u_4
inst_4 : CommRing R
inst_5 : AddCommGroup M
inst_6 : Module R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun (x : M) ↦ x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun (x : R) ↦ x • m₀) ⁻¹' U
x : TopologicalSpace R := BR.topology
m₀ : M
U : Set M
U_in :
  Membership.mem (γ := Set (Set M)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    U
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U
have rcases : ∀ (V : Set R) (V_in : V ∈ BR) (H : V ⊆ (fun (x : R) ↦ x • m₀) ⁻¹' U), ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U
Tactic: rcases smul_right m₀ U_in with ⟨V, V_in, H⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : V × V) ↦ p.1 + p.2
have have : ∀ (p : P), Continuous[instTopologicalSpaceProd, inst_1] fun (p : V × V) ↦ p.1 + p.2
Tactic: have ⟨p⟩ : Nonempty P := inferInstance
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
| Continuous[instTopologicalSpaceProd, inst_1] fun (p : V × V) ↦ p.1 + p.2
have h : ∀ (x : V × V), x.1 + x.2
Tactic: enter [1, x]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
x : V × V
⊢ x.1 + x.2 = (x.1 +ᵥ x.2 +ᵥ p) -ᵥ p
have h : x.1 + x.2 = ((x.1 + x.2) +ᵥ p) -ᵥ p
Tactic: rw [vadd_vadd, vadd_vsub]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
x : V × V
h : x.1 + x.2 = ((x.1 + x.2) +ᵥ p) -ᵥ p
⊢ x.1 + x.2 = (x.1 +ᵥ x.2 +ᵥ p) -ᵥ p
have h₁ : x.1 + x.2 = x.1 + x.2
Tactic: rw [vadd_vadd, vadd_vsub]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
| Continuous[instTopologicalSpaceProd, inst_1] fun (p : V × V) ↦ p.1 + p.2
have enter : fun (p : V × V) ↦ p.1 + p.2
Tactic: enter [1, x]
      equals (x.1 +ᵥ x.2 +ᵥ p) -ᵥ p => rw [vadd_vadd, vadd_vsub]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
enter : fun (p : V × V) ↦ p.1 + p.2
| Continuous[instTopologicalSpaceProd, inst_1] fun (p : V × V) ↦ p.1 + p.2
have h : ∀ (x : V × V), x.1 + x.2
Tactic: enter [1, x]
      equals (x.1 +ᵥ x.2 +ᵥ p) -ᵥ p => rw [vadd_vadd, vadd_vsub]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : V × V) ↦ p.1 + p.2
have conv : Continuous[instTopologicalSpaceProd, inst_1] fun (x : V × V) ↦ (x.1 +ᵥ x.2 +ᵥ p) -ᵥ p
Tactic: conv =>
      enter [1, x]
      equals (x.1 +ᵥ x.2 +ᵥ p) -ᵥ p => rw [vadd_vadd, vadd_vsub]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
⊢ Continuous[inst_1, inst_1] fun (a : V) ↦ -a
have have : ∀ (p : P), Continuous[inst_1, inst_1] fun (a : V) ↦ -a
Tactic: have ⟨p⟩ : Nonempty P := inferInstance
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
| Continuous[inst_1, inst_1] fun (a : V) ↦ -a
have h : ∀ (v : V), -v
Tactic: enter [1, v]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
v : V
⊢ -v = p -ᵥ (v +ᵥ p)
have h : -v = p -ᵥ p - v
Tactic: rw [vsub_vadd_eq_vsub_sub, vsub_self, zero_sub]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
v : V
h : -v = p -ᵥ p - v
⊢ -v = p -ᵥ (v +ᵥ p)
have h₁ : -v = 0 - v
Tactic: rw [vsub_vadd_eq_vsub_sub, vsub_self, zero_sub]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
v : V
h : -v = p -ᵥ p - v
h₁ : -v = 0 - v
⊢ -v = p -ᵥ (v +ᵥ p)
have h₂ : -v = -v
Tactic: rw [vsub_vadd_eq_vsub_sub, vsub_self, zero_sub]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
| Continuous[inst_1, inst_1] fun (a : V) ↦ -a
have enter : fun (a : V) ↦ -a
Tactic: enter [1, v]
      equals p -ᵥ (v +ᵥ p) => rw [vsub_vadd_eq_vsub_sub, vsub_self, zero_sub]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.AddTorsor (goal)
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
enter : fun (a : V) ↦ -a
| Continuous[inst_1, inst_1] fun (a : V) ↦ -a
have h : ∀ (v : V), -v
Tactic: enter [1, v]
      equals p -ᵥ (v +ᵥ p) => rw [vsub_vadd_eq_vsub_sub, vsub_self, zero_sub]