awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : ι → Submodule R A
hB : SubmodulesRingBasis B
⊢ RingSubgroupsBasis.{u_3, u_1} (A := A) fun (i : ι) ↦ (B i).toAddSubgroup
have apply : ∀ (x : A) (i : ι),
  ∃ (j : ι),
    (↑((B j).toAddSubgroup : AddSubgroup A) : Set A) ⊆
      (fun (y : A) ↦ x * y) ⁻¹' (↑((B i).toAddSubgroup : AddSubgroup A) : Set A)
Tactic: apply RingSubgroupsBasis.of_comm (fun i => (B i).toAddSubgroup) hB.inter hB.mul
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : ι → Submodule R A
hB : SubmodulesRingBasis B
a : A
i : ι
⊢ ∃ (j : ι),
    (↑((B j).toAddSubgroup : AddSubgroup A) : Set A) ⊆
      (fun (y : A) ↦ a * y) ⁻¹' (↑((B i).toAddSubgroup : AddSubgroup A) : Set A)
have rcases : ∀ (j : ι) (hj : a • B j ≤ B i),
  ∃ (j : ι),
    (↑((B j).toAddSubgroup : AddSubgroup A) : Set A) ⊆
      (fun (y : A) ↦ a * y) ⁻¹' (↑((B i).toAddSubgroup : AddSubgroup A) : Set A)
Tactic: rcases hB.leftMul a i with ⟨j, hj⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
ι : Type u_1
R : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : ι → Submodule R A
hB : SubmodulesRingBasis B
a : A
i j : ι
hj : a • B j ≤ B i
⊢ ∃ (j : ι),
    (↑((B j).toAddSubgroup : AddSubgroup A) : Set A) ⊆
      (fun (y : A) ↦ a * y) ⁻¹' (↑((B i).toAddSubgroup : AddSubgroup A) : Set A)
have h : (↑((B j).toAddSubgroup : AddSubgroup A) : Set A) ⊆
  (fun (y : A) ↦ a * y) ⁻¹' (↑((B i).toAddSubgroup : AddSubgroup A) : Set A)
Tactic: use j
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ Set.Nonempty.{u_4} (α := Set M) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)}
have inhabit : ∀ (inhabited_h : Inhabited ι), Set.Nonempty.{u_4} (α := Set M) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)}
Tactic: inhabit ι
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : ι
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨k, hk⟩ := hB.inter i j
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ ∃ (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)
have 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)
Tactic: use B k
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ 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)
have h : Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B k) : Set M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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)
⊢ 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)
have h₁ : (↑(B k) : Set M) ⊆ (↑(B i) : Set M) ∩ (↑(B j) : Set M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : ι
⊢ Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B k) : Set M)
have h : (↑(B k) : Set M) = (↑(B k) : Set M)
Tactic: use k
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : ι
⊢ ∃ (V : Set M),
    Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} V ∧ V + V ⊆ (↑(B i) : Set M)
have 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)
Tactic: use B i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 (γ := 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)
have h : Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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)
⊢ 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)
have h₁ : (↑(B i) : Set M) + (↑(B i) : Set M) ⊆ (↑(B i) : Set M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : ι
⊢ Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M)
have h : (↑(B i) : Set M) = (↑(B i) : Set M)
Tactic: use i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : ι
⊢ ∃ (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)
have 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)
Tactic: use B i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 (γ := 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)
have h : Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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)
⊢ 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)
have h₁ : (↑(B i) : Set M) ⊆ (fun (x : M) ↦ -x) ⁻¹' (↑(B i) : Set M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : ι
⊢ ∃ (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)
have 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)
Tactic: use B i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : ι
⊢ 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)
have h : Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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)
⊢ 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)
have h₁ : (↑(B i) : Set M) ⊆ (fun (x : M) ↦ x₀ + x + -x₀) ⁻¹' (↑(B i) : Set M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : ι
⊢ Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M)
have h : (↑(B i) : Set M) = (↑(B i) : Set M)
Tactic: use i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : ι
⊢ ∃ (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)
have 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)
Tactic: use univ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 ∧
    ∃ (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)
have h : Membership.mem (γ := Filter R) (𝓝 0) univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : 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)
have 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)
Tactic: use B i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 (γ := 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)
have h : Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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)
⊢ 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)
have h₁ : HSMul.hSMul.{u_2, u_4, u_4} (α := Set R) univ (↑(B i) : Set M) ⊆ (↑(B i) : Set M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : ι
⊢ ∃ (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)
have 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)
Tactic: use B i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : ι
⊢ 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)
have h : Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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)
⊢ 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)
have h₁ : (↑(B i) : Set M) ⊆ (fun (x : M) ↦ x₀ • x) ⁻¹' (↑(B i) : Set M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : ι
⊢ Membership.mem (γ := Set (Set M)) {U : Set M | ∃ (i : ι), U = (↑(B i) : Set M)} (↑(B i) : Set M)
have h : (↑(B i) : Set M) = (↑(B i) : Set M)
Tactic: use i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ IsOpen[hB.topology] (B i).toAddSubgroup.carrier
have rw : ∀ x ∈ (B i).toAddSubgroup.carrier, (B i).toAddSubgroup.carrier ∈ 𝓝 x
Tactic: rw [isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ (B i).toAddSubgroup.carrier ∈ 𝓝 a
have rw : ∃ i_1 ∈ hB.toModuleFilterBasis.toAddGroupFilterBasis, (fun (y : M) ↦ a + y) '' i_1 ⊆ (B i).toAddSubgroup.carrier
Tactic: rw [(hB.toModuleFilterBasis.toAddGroupFilterBasis.nhds_hasBasis a).mem_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ ∃ i_1 ∈ hB.toModuleFilterBasis.toAddGroupFilterBasis, (fun (y : M) ↦ a + y) '' i_1 ⊆ (B i).toAddSubgroup.carrier
have h : (↑(B i) : Set M) ∈ hB.toModuleFilterBasis.toAddGroupFilterBasis ∧
  (fun (y : M) ↦ a + y) '' (↑(B i) : Set M) ⊆ (B i).toAddSubgroup.carrier
Tactic: use B i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ (↑(B i) : Set M) ∈ hB.toModuleFilterBasis.toAddGroupFilterBasis ∧
    (fun (y : M) ↦ a + y) '' (↑(B i) : Set M) ⊆ (B i).toAddSubgroup.carrier
have h : (↑(B i) : Set M) ∈ hB.toModuleFilterBasis.toAddGroupFilterBasis
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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
⊢ (↑(B i) : Set M) ∈ hB.toModuleFilterBasis.toAddGroupFilterBasis ∧
    (fun (y : M) ↦ a + y) '' (↑(B i) : Set M) ⊆ (B i).toAddSubgroup.carrier
have h₁ : (fun (y : M) ↦ a + y) '' (↑(B i) : Set M) ⊆ (B i).toAddSubgroup.carrier
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
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 : ι
⊢ (↑(B i) : Set M) ∈ hB.toModuleFilterBasis.toAddGroupFilterBasis
have h : (↑(B i) : Set M) = (↑(B i) : Set M)
Tactic: use i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.Bases (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace R
inst_4 : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
this : TopologicalSpace M := hB.topology
⊢ NonarchimedeanAddGroup M
have is_nonarchimedean : ∀ (U : Set M), Membership.mem (γ := Filter M) (𝓝 0) U → ∃ (V : OpenAddSubgroup M), (↑V : Set M) ⊆ U
Tactic: constructor