awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
inhabited_h : Inhabited ι
⊢ Set.Nonempty.{u_4} (α := Set M) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)}

Tactic:
exact ⟨B default, default, rfl⟩
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i j : ι
obtain :
  ∀ (k : ι) (hk : B k ≤ B i ⊓ B j),
    ∃ (z : Set M),
      Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} z ∧
        z ⊆ (↑(B i) : Set M) ∩ (↑(B j) : Set M)
⊢ ∃ (z : Set M),
    Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} z ∧
      z ⊆ (↑(B i) : Set M) ∩ (↑(B j) : Set M)

Tactic:
obtain ⟨k, hk⟩ := hB.inter i j

Premises used: SubmodulesBasis.inter
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
h :
  Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B k) : Set M) ∧
    (↑(B k) : Set M) ⊆ (↑(B i) : Set M) ∩ (↑(B j) : Set M)
⊢ ∃ (z : Set M),
    Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} z ∧
      z ⊆ (↑(B i) : Set M) ∩ (↑(B j) : Set M)

Tactic:
use B k
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
h : Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B k) : Set M)
h₁ : (↑(B k) : Set M) ⊆ (↑(B i) : Set M) ∩ (↑(B j) : Set M)
⊢ Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B k) : Set M) ∧
    (↑(B k) : Set M) ⊆ (↑(B i) : Set M) ∩ (↑(B j) : Set M)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
w : ι
h : (↑(B k) : Set M) = (↑(B k) : Set M)
⊢ Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B k) : Set M)

Tactic:
use k
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ (↑(B k) : Set M) ⊆ (↑(B i) : Set M) ∩ (↑(B j) : Set M)

Tactic:
hk

Premises used: Set.Mem, setOf, Set.inter, Set.Subset
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ (↑(B k) : Set M) ⊆ (↑(B i) : Set M) ∩ (↑(B j) : Set M)

Tactic:
exact hk
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ 0 ∈ (↑(B i) : Set M)

Tactic:
(B i).zero_mem

Premises used: Set.Mem, Submodule.zero_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ 0 ∈ (↑(B i) : Set M)

Tactic:
exact (B i).zero_mem

Premises used: Submodule.zero_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
h :
  Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M) ∧
    (↑(B i) : Set M) + (↑(B i) : Set M) ⊆ (↑(B i) : Set M)
⊢ ∃ (V : Set M),
    Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} V ∧ V + V ⊆ (↑(B i) : Set M)

Tactic:
use B i
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
h : Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M)
h₁ : (↑(B i) : Set M) + (↑(B i) : Set M) ⊆ (↑(B i) : Set M)
⊢ Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M) ∧
    (↑(B i) : Set M) + (↑(B i) : Set M) ⊆ (↑(B i) : Set M)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i w : ι
h : (↑(B i) : Set M) = (↑(B i) : Set M)
⊢ Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M)

Tactic:
use i
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
y : M
y_in : y ∈ (↑(B i) : Set M)
z : M
z_in : z ∈ (↑(B i) : Set M)
⊢ (fun (x1 x2 : M) ↦ x1 + x2) y z ∈ (↑(B i) : Set M)

Tactic:
(B i).add_mem y_in z_in

Premises used: Set.Mem, Submodule.add_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
y : M
y_in : y ∈ (↑(B i) : Set M)
z : M
z_in : z ∈ (↑(B i) : Set M)
⊢ (fun (x1 x2 : M) ↦ x1 + x2) y z ∈ (↑(B i) : Set M)

Tactic:
exact (B i).add_mem y_in z_in

Premises used: Submodule.add_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
h :
  Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M) ∧
    (↑(B i) : Set M) ⊆ (fun (x : M) ↦ -x) ⁻¹' (↑(B i) : Set M)
⊢ ∃ (V : Set M),
    Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} V ∧
      V ⊆ (fun (x : M) ↦ -x) ⁻¹' (↑(B i) : Set M)

Tactic:
use B i
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
h : Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M)
h₁ : (↑(B i) : Set M) ⊆ (fun (x : M) ↦ -x) ⁻¹' (↑(B i) : Set M)
⊢ Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M) ∧
    (↑(B i) : Set M) ⊆ (fun (x : M) ↦ -x) ⁻¹' (↑(B i) : Set M)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x : M
x_in : x ∈ (↑(B i) : Set M)
⊢ Membership.mem (γ := Set M) ((fun (x : M) ↦ -x) ⁻¹' (↑(B i) : Set M)) x

Tactic:
(B i).neg_mem x_in

Premises used: Set.Mem, setOf, Submodule.neg_mem, Set.preimage
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x : M
x_in : x ∈ (↑(B i) : Set M)
⊢ Membership.mem (γ := Set M) ((fun (x : M) ↦ -x) ⁻¹' (↑(B i) : Set M)) x

Tactic:
exact (B i).neg_mem x_in

Premises used: Submodule.neg_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : M
i : ι
h :
  Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M) ∧
    (↑(B i) : Set M) ⊆ (fun (x : M) ↦ x₀ + x + -x₀) ⁻¹' (↑(B i) : Set M)
⊢ ∃ (V : Set M),
    Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} V ∧
      V ⊆ (fun (x : M) ↦ x₀ + x + -x₀) ⁻¹' (↑(B i) : Set M)

Tactic:
use B i
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : M
i : ι
h : Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M)
h₁ : (↑(B i) : Set M) ⊆ (fun (x : M) ↦ x₀ + x + -x₀) ⁻¹' (↑(B i) : Set M)
⊢ Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M) ∧
    (↑(B i) : Set M) ⊆ (fun (x : M) ↦ x₀ + x + -x₀) ⁻¹' (↑(B i) : Set M)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : M
i w : ι
h : (↑(B i) : Set M) = (↑(B i) : Set M)
⊢ Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M)

Tactic:
use i
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : M
i : ι
⊢ (↑(B i) : Set M) ⊆ (fun (x : M) ↦ x₀ + x + -x₀) ⁻¹' (↑(B i) : Set M)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
h :
  Membership.mem (γ := Filter R) (𝓝 0) univ ∧
    ∃ (W : Set M),
      Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} W ∧
        HSMul.hSMul.{u_2, u_4, u_4} (α := Set R) univ W ⊆ (↑(B i) : Set M)
⊢ ∃ (V : Set R),
    Membership.mem (γ := Filter R) (𝓝 0) V ∧
      ∃ (W : Set M),
        Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} W ∧ V • W ⊆ (↑(B i) : Set M)

Tactic:
use univ

Premises used: Set.univ
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
h : Membership.mem (γ := Filter R) (𝓝 0) univ
h₁ :
  ∃ (W : Set M),
    Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} W ∧
      HSMul.hSMul.{u_2, u_4, u_4} (α := Set R) univ W ⊆ (↑(B i) : Set M)
⊢ Membership.mem (γ := Filter R) (𝓝 0) univ ∧
    ∃ (W : Set M),
      Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} W ∧
        HSMul.hSMul.{u_2, u_4, u_4} (α := Set R) univ W ⊆ (↑(B i) : Set M)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ Membership.mem (γ := Filter R) (𝓝 0) univ

Tactic:
univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ Membership.mem (γ := Filter R) (𝓝 0) univ

Tactic:
exact univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
h :
  Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M) ∧
    HSMul.hSMul.{u_2, u_4, u_4} (α := Set R) univ (↑(B i) : Set M) ⊆ (↑(B i) : Set M)
⊢ ∃ (W : Set M),
    Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} W ∧
      HSMul.hSMul.{u_2, u_4, u_4} (α := Set R) univ W ⊆ (↑(B i) : Set M)

Tactic:
use B i
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
h : Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M)
h₁ : HSMul.hSMul.{u_2, u_4, u_4} (α := Set R) univ (↑(B i) : Set M) ⊆ (↑(B i) : Set M)
⊢ Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M) ∧
    HSMul.hSMul.{u_2, u_4, u_4} (α := Set R) univ (↑(B i) : Set M) ⊆ (↑(B i) : Set M)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
a : R
m : M
hm : m ∈ (↑(B i) : Set M)
⊢ (fun (x1 : R) (x2 : M) ↦ x1 • x2) a m ∈ (↑(B i) : Set M)

Tactic:
(B i).smul_mem _ hm

Premises used: Set.Mem, Submodule.smul_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
a : R
m : M
hm : m ∈ (↑(B i) : Set M)
⊢ (fun (x1 : R) (x2 : M) ↦ x1 • x2) a m ∈ (↑(B i) : Set M)

Tactic:
exact (B i).smul_mem _ hm

Premises used: Submodule.smul_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
h :
  Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M) ∧
    (↑(B i) : Set M) ⊆ (fun (x : M) ↦ x₀ • x) ⁻¹' (↑(B i) : Set M)
⊢ ∃ (V : Set M),
    Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} V ∧
      V ⊆ (fun (x : M) ↦ x₀ • x) ⁻¹' (↑(B i) : Set M)

Tactic:
use B i
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
h : Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M)
h₁ : (↑(B i) : Set M) ⊆ (fun (x : M) ↦ x₀ • x) ⁻¹' (↑(B i) : Set M)
⊢ Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M) ∧
    (↑(B i) : Set M) ⊆ (fun (x : M) ↦ x₀ • x) ⁻¹' (↑(B i) : Set M)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i w : ι
h : (↑(B i) : Set M) = (↑(B i) : Set M)
⊢ Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M)

Tactic:
use i
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
m : M
⊢ m ∈ (↑(B i) : Set M) → Membership.mem (γ := Set M) ((fun (x : M) ↦ x₀ • x) ⁻¹' (↑(B i) : Set M)) m

Tactic:
(B i).smul_mem _

Premises used: Set.Mem, setOf, Set.preimage, Submodule.smul_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
m : M
⊢ m ∈ (↑(B i) : Set M) → Membership.mem (γ := Set M) ((fun (x : M) ↦ x₀ • x) ⁻¹' (↑(B i) : Set M)) m

Tactic:
exact (B i).smul_mem _

Premises used: Submodule.smul_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
m₀ : M
i : ι
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ (↑(B i) : Set M)

Tactic:
hB.smul m₀ i

Premises used: SubmodulesBasis.smul
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
m₀ : M
i : ι
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ (↑(B i) : Set M)

Tactic:
exact hB.smul m₀ i

Premises used: SubmodulesBasis.smul
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x : TopologicalSpace M := hB.topology
this : TopologicalSpace M := hB.topology
rw : ∀ x ∈ (B i).toAddSubgroup.carrier, (B i).toAddSubgroup.carrier ∈ 𝓝 x
⊢ IsOpen[hB.topology] (B i).toAddSubgroup.carrier

Tactic:
rw [isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x : TopologicalSpace M := hB.topology
this : TopologicalSpace M := hB.topology
a : M
a_in : a ∈ (B i).toAddSubgroup.carrier
rw : ∃ i_1 ∈ hB.toModuleFilterBasis.toAddGroupFilterBasis, (fun (y : M) ↦ a + y) '' i_1 ⊆ (B i).toAddSubgroup.carrier
⊢ (B i).toAddSubgroup.carrier ∈ 𝓝 a

Tactic:
rw [(hB.toModuleFilterBasis.toAddGroupFilterBasis.nhds_hasBasis a).mem_iff]

Premises used: AddGroupFilterBasis.nhds_hasBasis, Filter.HasBasis.mem_iff, ModuleFilterBasis.toAddGroupFilterBasis, SubmodulesBasis.toModuleFilterBasis
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x : TopologicalSpace M := hB.topology
this : TopologicalSpace M := hB.topology
a : M
a_in : a ∈ (B i).toAddSubgroup.carrier
h :
  (↑(B i) : Set M) ∈ hB.toModuleFilterBasis.toAddGroupFilterBasis ∧
    (fun (y : M) ↦ a + y) '' (↑(B i) : Set M) ⊆ (B i).toAddSubgroup.carrier
⊢ ∃ i_1 ∈ hB.toModuleFilterBasis.toAddGroupFilterBasis, (fun (y : M) ↦ a + y) '' i_1 ⊆ (B i).toAddSubgroup.carrier

Tactic:
use B i
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x : TopologicalSpace M := hB.topology
this : TopologicalSpace M := hB.topology
a : M
a_in : a ∈ (B i).toAddSubgroup.carrier
h : (↑(B i) : Set M) ∈ hB.toModuleFilterBasis.toAddGroupFilterBasis
h₁ : (fun (y : M) ↦ a + y) '' (↑(B i) : Set M) ⊆ (B i).toAddSubgroup.carrier
⊢ (↑(B i) : Set M) ∈ hB.toModuleFilterBasis.toAddGroupFilterBasis ∧
    (fun (y : M) ↦ a + y) '' (↑(B i) : Set M) ⊆ (B i).toAddSubgroup.carrier

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace R
inst_6 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x : TopologicalSpace M := hB.topology
this : TopologicalSpace M := hB.topology
a : M
a_in : a ∈ (B i).toAddSubgroup.carrier
w : ι
h : (↑(B i) : Set M) = (↑(B i) : Set M)
⊢ (↑(B i) : Set M) ∈ hB.toModuleFilterBasis.toAddGroupFilterBasis

Tactic:
use i