awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.FilterBasis
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 : ∀ U ∈ B', ∃ (V : Set R) (W : Set R), (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U
⊢ ∀ 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:
suffices ∀ U ∈ B', ∃ V W, (V ∈ B' ∧ W ∈ B') ∧ ∀ a b, a ∈ V → b ∈ W → a * b ∈ U by simpa
-- Module: Mathlib.Topology.Algebra.FilterBasis
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'
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
⊢ ∃ (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⟩

Premises used: RingFilterBasis.mul
-- Module: Mathlib.Topology.Algebra.FilterBasis
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

Tactic:
⟨V, V, ⟨V_in, V_in⟩, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
hmul : ∀ (a b : R), a ∈ V → b ∈ V → a * b ∈ U
⊢ ∃ (V : Set R) (W : Set R), (V ∈ B' ∧ W ∈ B') ∧ ∀ (a b : R), a ∈ V → b ∈ W → a * b ∈ U

Tactic:
refine ⟨V, V, ⟨V_in, V_in⟩, ?_⟩
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
a b : R
a_in : a ∈ V
b_in : b ∈ V
⊢ a * b ∈ U

Tactic:
hV <| mul_mem_mul a_in b_in

Premises used: Set.mul_mem_mul
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
a b : R
a_in : a ∈ V
b_in : b ∈ V
⊢ a * b ∈ U

Tactic:
exact hV <| mul_mem_mul a_in b_in

Premises used: Set.mul_mem_mul
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
hmul_left : ∀ ib ∈ B', ∃ ia ∈ B', ∀ x ∈ id ia, x₀ * x ∈ id ib
⊢ Tendsto (β := R) (fun (x : R) ↦ x₀ * x) (𝓝 0) (𝓝 0)

Tactic:
rw [basis.tendsto_iff basis]

Premises used: Filter.HasBasis.tendsto_iff
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
U : Set R
⊢ U ∈ B' → ∃ ia ∈ B', ∀ x ∈ id ia, x₀ * x ∈ id U

Tactic:
simpa using B.mul_left x₀

Premises used: RingFilterBasis.mul_left
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
hmul_right : ∀ ib ∈ B', ∃ ia ∈ B', ∀ x ∈ id ia, x * x₀ ∈ id ib
⊢ Tendsto (β := R) (fun (x : R) ↦ x * x₀) (𝓝 0) (𝓝 0)

Tactic:
rw [basis.tendsto_iff basis]

Premises used: Filter.HasBasis.tendsto_iff
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
U : Set R
⊢ U ∈ B' → ∃ ia ∈ B', ∀ x ∈ id ia, x * x₀ ∈ id U

Tactic:
simpa using B.mul_right x₀

Premises used: RingFilterBasis.mul_right
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
U : Set M
hU : U ∈ B
⊢ ∃ (V : Set R), Membership.mem (γ := Filter R) (𝓝 0) V ∧ ∃ W ∈ B, V • W ⊆ U

Tactic:
B.smul' hU

Premises used: ModuleFilterBasis.smul'
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
x₀ : R
U : Set M
hU : U ∈ B
⊢ ∃ V ∈ B, V ⊆ (fun (x : M) ↦ x₀ • x) ⁻¹' U

Tactic:
B.smul_left' x₀ hU

Premises used: ModuleFilterBasis.smul_left'
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
m₀ : M
U : Set M
hU : U ∈ B
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U

Tactic:
B.smul_right' m₀ hU

Premises used: ModuleFilterBasis.smul_right'
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
right : HSMul.hSMul.{u_1, u_2, u_2} (α := Set R) (β := Set M) univ {0} ⊆ {0}
⊢ ∃ (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}

Tactic:
use univ, univ_mem, {0}, rfl

Premises used: Set.univ, Filter.univ_mem, rfl
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
⊢ Membership.mem (γ := Set M) {0} ((fun (x1 : R) (x2 : M) ↦ x1 • x2) x 0)

Tactic:
simp only [smul_zero, mem_singleton_iff]

Premises used: smul_zero, Set.mem_singleton_iff
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
⊢ U = {0}

Tactic:
rw [mem_singleton_iff] at h

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Topology.Algebra.FilterBasis
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}
right : Subset (α := Set M) {0} ((fun (x : M) ↦ x₀ • x) ⁻¹' U)
⊢ ∃ (V : Set M),
    Membership.mem (γ := Set (Set M))
        (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) V ∧
      V ⊆ (fun (x : M) ↦ x₀ • x) ⁻¹' U

Tactic:
use {0}, rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.FilterBasis
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}
⊢ Subset (α := Set M) {0} ((fun (x : M) ↦ x₀ • x) ⁻¹' U)

Tactic:
simp [h]
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
⊢ U = 0

Tactic:
rw [Set.mem_zero] at h

Premises used: Set.mem_zero
-- Module: Mathlib.Topology.Algebra.FilterBasis
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 : U = 0
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U

Tactic:
simp [h, nhds_discrete]

Premises used: nhds_discrete
-- Module: Mathlib.Topology.Algebra.FilterBasis
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)
hmulright : ∀ (a : R), Tendsto (β := M) (fun (m : M) ↦ a • m) (𝓝 0) (𝓝 0)
⊢ ContinuousSMul R M

Tactic:
apply ContinuousSMul.of_nhds_zero

Premises used: ContinuousSMul.of_nhds_zero
-- Module: Mathlib.Topology.Algebra.FilterBasis
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 : ∀ (i : ι), p i → ∀ᶠ (x : R × M) in SProd.sprod (α := Filter R) (β := Filter M) (𝓝 0) (𝓝 0), x.1 • x.2 ∈ b i
⊢ Tendsto (β := M) (fun (p : R × M) ↦ p.1 • p.2) (SProd.sprod (α := Filter R) (β := Filter M) (𝓝 0) (𝓝 0)) (𝓝 0)

Tactic:
rw [h.tendsto_right_iff]

Premises used: Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
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
⊢ ∀ᶠ (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⟩
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
hmul : V ×ˢ b j ⊆ {x : R × M | (fun (x : R × M) ↦ x.1 • x.2 ∈ b i) x}
⊢ ∀ᶠ (x : R × M) in SProd.sprod (α := Filter R) (β := Filter M) (𝓝 0) (𝓝 0), x.1 • x.2 ∈ b i

Tactic:
apply mem_of_superset (prod_mem_prod V_in <| h.mem_of_mem hj)

Premises used: Filter.prod_mem_prod, Filter.HasBasis.mem_of_mem, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
v : R
w : M
v_in : v ∈ V
w_in : w ∈ b j
⊢ Membership.mem (γ := Set (R × M)) {x : R × M | (fun (x : R × M) ↦ x.1 • x.2 ∈ b i) x} (v, w)

Tactic:
hVj (Set.smul_mem_smul v_in w_in)

Premises used: Set.Mem, Set.smul_mem_smul, setOf
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
v : R
w : M
v_in : v ∈ V
w_in : w ∈ b j
⊢ Membership.mem (γ := Set (R × M)) {x : R × M | (fun (x : R × M) ↦ x.1 • x.2 ∈ b i) x} (v, w)

Tactic:
exact hVj (Set.smul_mem_smul v_in w_in)

Premises used: Set.smul_mem_smul
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
hmulleft : ∀ (i : ι), p i → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i
⊢ Tendsto.{u_1, u_2} (β := M) (fun (a : R) ↦ a • m₀) (𝓝 0) (𝓝 0)

Tactic:
rw [h.tendsto_right_iff]

Premises used: Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
i : ι
hi : p i
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i

Tactic:
hsmul_right m₀ hi

Premises used: Set.Mem
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
i : ι
hi : p i
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ b i

Tactic:
exact hsmul_right m₀ hi
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
hmulright : ∀ (i : ι), p i → ∀ᶠ (x : M) in 𝓝 0, x₀ • x ∈ b i
⊢ Tendsto (β := M) (fun (m : M) ↦ x₀ • m) (𝓝 0) (𝓝 0)

Tactic:
rw [h.tendsto_right_iff]

Premises used: Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
hmulright : ∀ (j : ι) (hj : p j) (hji : MapsTo (fun (x : M) ↦ x₀ • x) (b j) (b i)), ∀ᶠ (x : M) in 𝓝 0, x₀ • x ∈ b i
⊢ ∀ᶠ (x : M) in 𝓝 0, x₀ • x ∈ b i

Tactic:
rcases hsmul_left x₀ hi with ⟨j, hj, hji⟩
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
j : ι
hj : p j
hji : MapsTo (fun (x : M) ↦ x₀ • x) (b j) (b i)
⊢ ∀ᶠ (x : M) in 𝓝 0, x₀ • x ∈ b i

Tactic:
mem_of_superset (h.mem_of_mem hj) hji

Premises used: Filter.Eventually, Filter.HasBasis.mem_of_mem, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
j : ι
hj : p j
hji : MapsTo (fun (x : M) ↦ x₀ • x) (b j) (b i)
⊢ ∀ᶠ (x : M) in 𝓝 0, x₀ • x ∈ b i

Tactic:
exact mem_of_superset (h.mem_of_mem hj) hji

Premises used: Filter.HasBasis.mem_of_mem, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
⊢ IsTopologicalAddGroup M

Tactic:
have _ := B'.isTopologicalAddGroup
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
h : IsTopologicalAddGroup M
x_1 : Set M
⊢ x_1 ∈ B' → ∃ (V : Set R), Membership.mem (γ := Filter R) (𝓝 0) V ∧ ∃ j ∈ B', V • id j ⊆ id x_1

Tactic:
simpa using B.smul

Premises used: ModuleFilterBasis.smul
-- Module: Mathlib.Topology.Algebra.FilterBasis
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
h : IsTopologicalAddGroup M
⊢ ∀ (x₀ : R) {i : Set M}, i ∈ B' → ∃ j ∈ B', MapsTo (fun (x : M) ↦ x₀ • x) (id j) (id i)

Tactic:
simpa using B.smul_left

Premises used: ModuleFilterBasis.smul_left