[GOAL]
A✝ : Type u_1
ι✝ : Type u_2
inst✝¹ : Ring A✝
A : Type u_3
ι : Type u_4
inst✝ : CommRing A
B : ι → AddSubgroup A
inter : ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
mul : ∀ (i : ι), ∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)
leftMul : ∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun y => x * y) ⁻¹' ↑(B i)
⊢ ∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(B i)
[PROOFSTEP]
intro x i
[GOAL]
A✝ : Type u_1
ι✝ : Type u_2
inst✝¹ : Ring A✝
A : Type u_3
ι : Type u_4
inst✝ : CommRing A
B : ι → AddSubgroup A
inter : ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
mul : ∀ (i : ι), ∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)
leftMul : ∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun y => x * y) ⁻¹' ↑(B i)
x : A
i : ι
⊢ ∃ j, ↑(B j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(B i)
[PROOFSTEP]
cases' leftMul x i with j hj
[GOAL]
case intro
A✝ : Type u_1
ι✝ : Type u_2
inst✝¹ : Ring A✝
A : Type u_3
ι : Type u_4
inst✝ : CommRing A
B : ι → AddSubgroup A
inter : ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
mul : ∀ (i : ι), ∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)
leftMul : ∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun y => x * y) ⁻¹' ↑(B i)
x : A
i j : ι
hj : ↑(B j) ⊆ (fun y => x * y) ⁻¹' ↑(B i)
⊢ ∃ j, ↑(B j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(B i)
[PROOFSTEP]
use j
[GOAL]
case h
A✝ : Type u_1
ι✝ : Type u_2
inst✝¹ : Ring A✝
A : Type u_3
ι : Type u_4
inst✝ : CommRing A
B : ι → AddSubgroup A
inter : ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
mul : ∀ (i : ι), ∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)
leftMul : ∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun y => x * y) ⁻¹' ↑(B i)
x : A
i j : ι
hj : ↑(B j) ⊆ (fun y => x * y) ⁻¹' ↑(B i)
⊢ ↑(B j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(B i)
[PROOFSTEP]
simpa [mul_comm] using hj
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ Set.Nonempty {U | ∃ i, U = ↑(B i)}
[PROOFSTEP]
inhabit ι
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
inhabited_h : Inhabited ι
⊢ Set.Nonempty {U | ∃ i, U = ↑(B i)}
[PROOFSTEP]
exact ⟨B default, default, rfl⟩
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ {x y : Set A}, x ∈ {U | ∃ i, U = ↑(B i)} → y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y
[PROOFSTEP]
rintro _ _ ⟨i, rfl⟩ ⟨j, rfl⟩
[GOAL]
case intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i j : ι
⊢ ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ ↑(B i) ∩ ↑(B j)
[PROOFSTEP]
cases' hB.inter i j with k hk
[GOAL]
case intro.intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ ↑(B i) ∩ ↑(B j)
[PROOFSTEP]
use B k
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ↑(B k) ∈ {U | ∃ i, U = ↑(B i)} ∧ ↑(B k) ⊆ ↑(B i) ∩ ↑(B j)
[PROOFSTEP]
constructor
[GOAL]
case h.left
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ↑(B k) ∈ {U | ∃ i, U = ↑(B i)}
[PROOFSTEP]
use k
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ↑(B k) ⊆ ↑(B i) ∩ ↑(B j)
[PROOFSTEP]
exact hk
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ {U : Set A},
    U ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set A},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets →
      0 ∈ U
[PROOFSTEP]
rintro _ ⟨i, rfl⟩
[GOAL]
case intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ 0 ∈ ↑(B i)
[PROOFSTEP]
exact (B i).zero_mem
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ {U : Set A},
    U ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set A},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets →
      ∃ V,
        V ∈
            { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
                inter_sets :=
                  (_ :
                    ∀ {x y : Set A},
                      x ∈ {U | ∃ i, U = ↑(B i)} →
                        y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
          V + V ⊆ U
[PROOFSTEP]
rintro _ ⟨i, rfl⟩
[GOAL]
case intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ∃ V,
    V ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set A},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
      V + V ⊆ ↑(B i)
[PROOFSTEP]
use B i
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ↑(B i) ∈
      { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
          inter_sets :=
            (_ :
              ∀ {x y : Set A},
                x ∈ {U | ∃ i, U = ↑(B i)} →
                  y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
    ↑(B i) + ↑(B i) ⊆ ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ↑(B i) ∈
    { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
        inter_sets :=
          (_ :
            ∀ {x y : Set A},
              x ∈ {U | ∃ i, U = ↑(B i)} → y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets
[PROOFSTEP]
use i
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ↑(B i) + ↑(B i) ⊆ ↑(B i)
[PROOFSTEP]
rintro x ⟨y, z, y_in, z_in, rfl⟩
[GOAL]
case h.right.intro.intro.intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
y z : A
y_in : y ∈ ↑(B i)
z_in : z ∈ ↑(B i)
⊢ (fun x x_1 => x + x_1) y z ∈ ↑(B i)
[PROOFSTEP]
exact (B i).add_mem y_in z_in
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ {U : Set A},
    U ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set A},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets →
      ∃ V,
        V ∈
            { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
                inter_sets :=
                  (_ :
                    ∀ {x y : Set A},
                      x ∈ {U | ∃ i, U = ↑(B i)} →
                        y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
          V ⊆ (fun x => -x) ⁻¹' U
[PROOFSTEP]
rintro _ ⟨i, rfl⟩
[GOAL]
case intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ∃ V,
    V ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set A},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
      V ⊆ (fun x => -x) ⁻¹' ↑(B i)
[PROOFSTEP]
use B i
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ↑(B i) ∈
      { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
          inter_sets :=
            (_ :
              ∀ {x y : Set A},
                x ∈ {U | ∃ i, U = ↑(B i)} →
                  y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
    ↑(B i) ⊆ (fun x => -x) ⁻¹' ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ↑(B i) ∈
    { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
        inter_sets :=
          (_ :
            ∀ {x y : Set A},
              x ∈ {U | ∃ i, U = ↑(B i)} → y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets
[PROOFSTEP]
use i
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ↑(B i) ⊆ (fun x => -x) ⁻¹' ↑(B i)
[PROOFSTEP]
intro x x_in
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x : A
x_in : x ∈ ↑(B i)
⊢ x ∈ (fun x => -x) ⁻¹' ↑(B i)
[PROOFSTEP]
exact (B i).neg_mem x_in
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ (x₀ : A) {U : Set A},
    U ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set A},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets →
      ∃ V,
        V ∈
            { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
                inter_sets :=
                  (_ :
                    ∀ {x y : Set A},
                      x ∈ {U | ∃ i, U = ↑(B i)} →
                        y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
          V ⊆ (fun x => x₀ + x + -x₀) ⁻¹' U
[PROOFSTEP]
rintro x₀ _ ⟨i, rfl⟩
[GOAL]
case intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
⊢ ∃ V,
    V ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set A},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
      V ⊆ (fun x => x₀ + x + -x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
use B i
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
⊢ ↑(B i) ∈
      { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
          inter_sets :=
            (_ :
              ∀ {x y : Set A},
                x ∈ {U | ∃ i, U = ↑(B i)} →
                  y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
    ↑(B i) ⊆ (fun x => x₀ + x + -x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
⊢ ↑(B i) ∈
    { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
        inter_sets :=
          (_ :
            ∀ {x y : Set A},
              x ∈ {U | ∃ i, U = ↑(B i)} → y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets
[PROOFSTEP]
use i
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
⊢ ↑(B i) ⊆ (fun x => x₀ + x + -x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ {U : Set A},
    U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V * V ⊆ U
[PROOFSTEP]
rintro _ ⟨i, rfl⟩
[GOAL]
case intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V * V ⊆ ↑(B i)
[PROOFSTEP]
cases' hB.mul i with k hk
[GOAL]
case intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i k : ι
hk : ↑(B k) * ↑(B k) ⊆ ↑(B i)
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V * V ⊆ ↑(B i)
[PROOFSTEP]
use B k
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i k : ι
hk : ↑(B k) * ↑(B k) ⊆ ↑(B i)
⊢ ↑(B k) ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ ↑(B k) * ↑(B k) ⊆ ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i k : ι
hk : ↑(B k) * ↑(B k) ⊆ ↑(B i)
⊢ ↑(B k) ∈ AddGroupFilterBasis.toFilterBasis.sets
[PROOFSTEP]
use k
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i k : ι
hk : ↑(B k) * ↑(B k) ⊆ ↑(B i)
⊢ ↑(B k) * ↑(B k) ⊆ ↑(B i)
[PROOFSTEP]
exact hk
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ (x₀ : A) {U : Set A},
    U ∈ AddGroupFilterBasis.toFilterBasis.sets →
      ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x₀ * x) ⁻¹' U
[PROOFSTEP]
rintro x₀ _ ⟨i, rfl⟩
[GOAL]
case intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x₀ * x) ⁻¹' ↑(B i)
[PROOFSTEP]
cases' hB.leftMul x₀ i with k hk
[GOAL]
case intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x => x₀ * x) ⁻¹' ↑(B i)
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x₀ * x) ⁻¹' ↑(B i)
[PROOFSTEP]
use B k
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x => x₀ * x) ⁻¹' ↑(B i)
⊢ ↑(B k) ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ ↑(B k) ⊆ (fun x => x₀ * x) ⁻¹' ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x => x₀ * x) ⁻¹' ↑(B i)
⊢ ↑(B k) ∈ AddGroupFilterBasis.toFilterBasis.sets
[PROOFSTEP]
use k
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x => x₀ * x) ⁻¹' ↑(B i)
⊢ ↑(B k) ⊆ (fun x => x₀ * x) ⁻¹' ↑(B i)
[PROOFSTEP]
exact hk
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ (x₀ : A) {U : Set A},
    U ∈ AddGroupFilterBasis.toFilterBasis.sets →
      ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x * x₀) ⁻¹' U
[PROOFSTEP]
rintro x₀ _ ⟨i, rfl⟩
[GOAL]
case intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x * x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
cases' hB.rightMul x₀ i with k hk
[GOAL]
case intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x => x * x₀) ⁻¹' ↑(B i)
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x * x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
use B k
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x => x * x₀) ⁻¹' ↑(B i)
⊢ ↑(B k) ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ ↑(B k) ⊆ (fun x => x * x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x => x * x₀) ⁻¹' ↑(B i)
⊢ ↑(B k) ∈ AddGroupFilterBasis.toFilterBasis.sets
[PROOFSTEP]
use k
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x => x * x₀) ⁻¹' ↑(B i)
⊢ ↑(B k) ⊆ (fun x => x * x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
exact hk
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ (t : Set A), t ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(B i) ⊆ t
[PROOFSTEP]
intro s
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
⊢ s ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(B i) ⊆ s
[PROOFSTEP]
rw [hB.toRingFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff]
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
⊢ (∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ s) ↔ ∃ i, True ∧ ↑(B i) ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
⊢ (∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ s) → ∃ i, True ∧ ↑(B i) ⊆ s
[PROOFSTEP]
rintro ⟨-, ⟨i, rfl⟩, hi⟩
[GOAL]
case mp.intro.intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
i : ι
hi : id ↑(B i) ⊆ s
⊢ ∃ i, True ∧ ↑(B i) ⊆ s
[PROOFSTEP]
exact ⟨i, trivial, hi⟩
[GOAL]
case mpr
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
⊢ (∃ i, True ∧ ↑(B i) ⊆ s) → ∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ s
[PROOFSTEP]
rintro ⟨i, -, hi⟩
[GOAL]
case mpr.intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
i : ι
hi : ↑(B i) ⊆ s
⊢ ∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ s
[PROOFSTEP]
exact ⟨B i, ⟨i, rfl⟩, hi⟩
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
⊢ ∀ (t : Set A), t ∈ 𝓝 a ↔ ∃ i, True ∧ {b | b - a ∈ B i} ⊆ t
[PROOFSTEP]
intro s
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
⊢ s ∈ 𝓝 a ↔ ∃ i, True ∧ {b | b - a ∈ B i} ⊆ s
[PROOFSTEP]
rw [(hB.toRingFilterBasis.toAddGroupFilterBasis.nhds_hasBasis a).mem_iff]
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
⊢ (∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ (fun y => a + y) '' i ⊆ s) ↔ ∃ i, True ∧ {b | b - a ∈ B i} ⊆ s
[PROOFSTEP]
simp only [true_and]
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
⊢ (∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ (fun y => a + y) '' i ⊆ s) ↔ ∃ i, {b | b - a ∈ B i} ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
⊢ (∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ (fun y => a + y) '' i ⊆ s) → ∃ i, {b | b - a ∈ B i} ⊆ s
[PROOFSTEP]
rintro ⟨-, ⟨i, rfl⟩, hi⟩
[GOAL]
case mp.intro.intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y => a + y) '' ↑(B i) ⊆ s
⊢ ∃ i, {b | b - a ∈ B i} ⊆ s
[PROOFSTEP]
use i
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y => a + y) '' ↑(B i) ⊆ s
⊢ {b | b - a ∈ B i} ⊆ s
[PROOFSTEP]
suffices h : {b : A | b - a ∈ B i} = (fun y => a + y) '' ↑(B i)
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y => a + y) '' ↑(B i) ⊆ s
h : {b | b - a ∈ B i} = (fun y => a + y) '' ↑(B i)
⊢ {b | b - a ∈ B i} ⊆ s
[PROOFSTEP]
rw [h]
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y => a + y) '' ↑(B i) ⊆ s
h : {b | b - a ∈ B i} = (fun y => a + y) '' ↑(B i)
⊢ (fun y => a + y) '' ↑(B i) ⊆ s
[PROOFSTEP]
assumption
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y => a + y) '' ↑(B i) ⊆ s
⊢ {b | b - a ∈ B i} = (fun y => a + y) '' ↑(B i)
[PROOFSTEP]
simp only [image_add_left, neg_add_eq_sub]
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y => a + y) '' ↑(B i) ⊆ s
⊢ {b | b - a ∈ B i} = (fun x => x - a) ⁻¹' ↑(B i)
[PROOFSTEP]
ext b
[GOAL]
case h.h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y => a + y) '' ↑(B i) ⊆ s
b : A
⊢ b ∈ {b | b - a ∈ B i} ↔ b ∈ (fun x => x - a) ⁻¹' ↑(B i)
[PROOFSTEP]
simp
[GOAL]
case mpr
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
⊢ (∃ i, {b | b - a ∈ B i} ⊆ s) → ∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ (fun y => a + y) '' i ⊆ s
[PROOFSTEP]
rintro ⟨i, hi⟩
[GOAL]
case mpr.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b | b - a ∈ B i} ⊆ s
⊢ ∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ (fun y => a + y) '' i ⊆ s
[PROOFSTEP]
use B i
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b | b - a ∈ B i} ⊆ s
⊢ ↑(B i) ∈ RingFilterBasis.toAddGroupFilterBasis ∧ (fun y => a + y) '' ↑(B i) ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case h.left
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b | b - a ∈ B i} ⊆ s
⊢ ↑(B i) ∈ RingFilterBasis.toAddGroupFilterBasis
[PROOFSTEP]
use i
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b | b - a ∈ B i} ⊆ s
⊢ (fun y => a + y) '' ↑(B i) ⊆ s
[PROOFSTEP]
rw [image_subset_iff]
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b | b - a ∈ B i} ⊆ s
⊢ ↑(B i) ⊆ (fun y => a + y) ⁻¹' s
[PROOFSTEP]
rintro b b_in
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b | b - a ∈ B i} ⊆ s
b : A
b_in : b ∈ ↑(B i)
⊢ b ∈ (fun y => a + y) ⁻¹' s
[PROOFSTEP]
apply hi
[GOAL]
case h.right.a
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b | b - a ∈ B i} ⊆ s
b : A
b_in : b ∈ ↑(B i)
⊢ (fun y => a + y) b ∈ {b | b - a ∈ B i}
[PROOFSTEP]
simpa using b_in
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x✝ : TopologicalSpace A := topology hB
src✝ : AddSubgroup A := B i
⊢ IsOpen
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rw [isOpen_iff_mem_nhds]
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x✝ : TopologicalSpace A := topology hB
src✝ : AddSubgroup A := B i
⊢ ∀ (a : A),
    a ∈
        { toAddSubmonoid := src✝.toAddSubmonoid,
                neg_mem' :=
                  (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
      { toAddSubmonoid := src✝.toAddSubmonoid,
                neg_mem' :=
                  (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier ∈
        𝓝 a
[PROOFSTEP]
intro a a_in
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x✝ : TopologicalSpace A := topology hB
src✝ : AddSubgroup A := B i
a : A
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' :=
              (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier ∈
    𝓝 a
[PROOFSTEP]
rw [(hB.hasBasis_nhds a).mem_iff]
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x✝ : TopologicalSpace A := topology hB
src✝ : AddSubgroup A := B i
a : A
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ∃ i,
    True ∧
      {b | b - a ∈ B i} ⊆
        { toAddSubmonoid := src✝.toAddSubmonoid,
                neg_mem' :=
                  (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
use i, trivial
[GOAL]
case right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x✝ : TopologicalSpace A := topology hB
src✝ : AddSubgroup A := B i
a : A
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ {b | b - a ∈ B i} ⊆
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rintro b b_in
[GOAL]
case right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x✝ : TopologicalSpace A := topology hB
src✝ : AddSubgroup A := B i
a : A
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
b : A
b_in : b ∈ {b | b - a ∈ B i}
⊢ b ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
simpa using (B i).add_mem a_in b_in
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ NonarchimedeanRing A
[PROOFSTEP]
letI := hB.topology
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := topology hB
⊢ NonarchimedeanRing A
[PROOFSTEP]
constructor
[GOAL]
case is_nonarchimedean
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := topology hB
⊢ ∀ (U : Set A), U ∈ 𝓝 0 → ∃ V, ↑V ⊆ U
[PROOFSTEP]
intro U hU
[GOAL]
case is_nonarchimedean
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := topology hB
U : Set A
hU : U ∈ 𝓝 0
⊢ ∃ V, ↑V ⊆ U
[PROOFSTEP]
obtain ⟨i, -, hi : (B i : Set A) ⊆ U⟩ := hB.hasBasis_nhds_zero.mem_iff.mp hU
[GOAL]
case is_nonarchimedean.intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := topology hB
U : Set A
hU : U ∈ 𝓝 0
i : ι
hi : ↑(B i) ⊆ U
⊢ ∃ V, ↑V ⊆ U
[PROOFSTEP]
exact ⟨hB.openAddSubgroup i, hi⟩
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB✝ hB : SubmodulesRingBasis B
⊢ RingSubgroupsBasis fun i => Submodule.toAddSubgroup (B i)
[PROOFSTEP]
apply RingSubgroupsBasis.of_comm (fun i => (B i).toAddSubgroup) hB.inter hB.mul
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB✝ hB : SubmodulesRingBasis B
⊢ ∀ (x : A) (i : ι), ∃ j, ↑(Submodule.toAddSubgroup (B j)) ⊆ (fun y => x * y) ⁻¹' ↑(Submodule.toAddSubgroup (B i))
[PROOFSTEP]
intro a i
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB✝ hB : SubmodulesRingBasis B
a : A
i : ι
⊢ ∃ j, ↑(Submodule.toAddSubgroup (B j)) ⊆ (fun y => a * y) ⁻¹' ↑(Submodule.toAddSubgroup (B i))
[PROOFSTEP]
rcases hB.leftMul a i with ⟨j, hj⟩
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB✝ hB : SubmodulesRingBasis B
a : A
i j : ι
hj : a • B j ≤ B i
⊢ ∃ j, ↑(Submodule.toAddSubgroup (B j)) ⊆ (fun y => a * y) ⁻¹' ↑(Submodule.toAddSubgroup (B i))
[PROOFSTEP]
use j
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB✝ hB : SubmodulesRingBasis B
a : A
i j : ι
hj : a • B j ≤ B i
⊢ ↑(Submodule.toAddSubgroup (B j)) ⊆ (fun y => a * y) ⁻¹' ↑(Submodule.toAddSubgroup (B i))
[PROOFSTEP]
rintro b (b_in : b ∈ B j)
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB✝ hB : SubmodulesRingBasis B
a : A
i j : ι
hj : a • B j ≤ B i
b : A
b_in : b ∈ B j
⊢ b ∈ (fun y => a * y) ⁻¹' ↑(Submodule.toAddSubgroup (B i))
[PROOFSTEP]
exact hj ⟨b, b_in, rfl⟩
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ Set.Nonempty {U | ∃ i, U = ↑(B i)}
[PROOFSTEP]
inhabit ι
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
inhabited_h : Inhabited ι
⊢ Set.Nonempty {U | ∃ i, U = ↑(B i)}
[PROOFSTEP]
exact ⟨B default, default, rfl⟩
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ {x y : Set M}, x ∈ {U | ∃ i, U = ↑(B i)} → y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y
[PROOFSTEP]
rintro _ _ ⟨i, rfl⟩ ⟨j, rfl⟩
[GOAL]
case intro.intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i j : ι
⊢ ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ ↑(B i) ∩ ↑(B j)
[PROOFSTEP]
cases' hB.inter i j with k hk
[GOAL]
case intro.intro.intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ ↑(B i) ∩ ↑(B j)
[PROOFSTEP]
use B k
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ↑(B k) ∈ {U | ∃ i, U = ↑(B i)} ∧ ↑(B k) ⊆ ↑(B i) ∩ ↑(B j)
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ↑(B k) ∈ {U | ∃ i, U = ↑(B i)}
[PROOFSTEP]
use k
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ↑(B k) ⊆ ↑(B i) ∩ ↑(B j)
[PROOFSTEP]
exact hk
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ {U : Set M},
    U ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set M},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets →
      0 ∈ U
[PROOFSTEP]
rintro _ ⟨i, rfl⟩
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ 0 ∈ ↑(B i)
[PROOFSTEP]
exact (B i).zero_mem
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ {U : Set M},
    U ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set M},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets →
      ∃ V,
        V ∈
            { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
                inter_sets :=
                  (_ :
                    ∀ {x y : Set M},
                      x ∈ {U | ∃ i, U = ↑(B i)} →
                        y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
          V + V ⊆ U
[PROOFSTEP]
rintro _ ⟨i, rfl⟩
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ∃ V,
    V ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set M},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
      V + V ⊆ ↑(B i)
[PROOFSTEP]
use B i
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ∈
      { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
          inter_sets :=
            (_ :
              ∀ {x y : Set M},
                x ∈ {U | ∃ i, U = ↑(B i)} →
                  y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
    ↑(B i) + ↑(B i) ⊆ ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ∈
    { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
        inter_sets :=
          (_ :
            ∀ {x y : Set M},
              x ∈ {U | ∃ i, U = ↑(B i)} → y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets
[PROOFSTEP]
use i
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) + ↑(B i) ⊆ ↑(B i)
[PROOFSTEP]
rintro x ⟨y, z, y_in, z_in, rfl⟩
[GOAL]
case h.right.intro.intro.intro.intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
y z : M
y_in : y ∈ ↑(B i)
z_in : z ∈ ↑(B i)
⊢ (fun x x_1 => x + x_1) y z ∈ ↑(B i)
[PROOFSTEP]
exact (B i).add_mem y_in z_in
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ {U : Set M},
    U ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set M},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets →
      ∃ V,
        V ∈
            { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
                inter_sets :=
                  (_ :
                    ∀ {x y : Set M},
                      x ∈ {U | ∃ i, U = ↑(B i)} →
                        y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
          V ⊆ (fun x => -x) ⁻¹' U
[PROOFSTEP]
rintro _ ⟨i, rfl⟩
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ∃ V,
    V ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set M},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
      V ⊆ (fun x => -x) ⁻¹' ↑(B i)
[PROOFSTEP]
use B i
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ∈
      { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
          inter_sets :=
            (_ :
              ∀ {x y : Set M},
                x ∈ {U | ∃ i, U = ↑(B i)} →
                  y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
    ↑(B i) ⊆ (fun x => -x) ⁻¹' ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ∈
    { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
        inter_sets :=
          (_ :
            ∀ {x y : Set M},
              x ∈ {U | ∃ i, U = ↑(B i)} → y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets
[PROOFSTEP]
use i
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ⊆ (fun x => -x) ⁻¹' ↑(B i)
[PROOFSTEP]
intro x x_in
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x : M
x_in : x ∈ ↑(B i)
⊢ x ∈ (fun x => -x) ⁻¹' ↑(B i)
[PROOFSTEP]
exact (B i).neg_mem x_in
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ (x₀ : M) {U : Set M},
    U ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set M},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets →
      ∃ V,
        V ∈
            { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
                inter_sets :=
                  (_ :
                    ∀ {x y : Set M},
                      x ∈ {U | ∃ i, U = ↑(B i)} →
                        y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
          V ⊆ (fun x => x₀ + x + -x₀) ⁻¹' U
[PROOFSTEP]
rintro x₀ _ ⟨i, rfl⟩
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : M
i : ι
⊢ ∃ V,
    V ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set M},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
      V ⊆ (fun x => x₀ + x + -x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
use B i
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : M
i : ι
⊢ ↑(B i) ∈
      { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
          inter_sets :=
            (_ :
              ∀ {x y : Set M},
                x ∈ {U | ∃ i, U = ↑(B i)} →
                  y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
    ↑(B i) ⊆ (fun x => x₀ + x + -x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : M
i : ι
⊢ ↑(B i) ∈
    { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
        inter_sets :=
          (_ :
            ∀ {x y : Set M},
              x ∈ {U | ∃ i, U = ↑(B i)} → y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets
[PROOFSTEP]
use i
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : M
i : ι
⊢ ↑(B i) ⊆ (fun x => x₀ + x + -x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ {U : Set M},
    U ∈ AddGroupFilterBasis.toFilterBasis.sets →
      ∃ V, V ∈ 𝓝 0 ∧ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V • W ⊆ U
[PROOFSTEP]
rintro _ ⟨i, rfl⟩
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ∃ V, V ∈ 𝓝 0 ∧ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V • W ⊆ ↑(B i)
[PROOFSTEP]
use univ
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ univ ∈ 𝓝 0 ∧ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ univ • W ⊆ ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ univ ∈ 𝓝 0
[PROOFSTEP]
exact univ_mem
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ univ • W ⊆ ↑(B i)
[PROOFSTEP]
use B i
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ univ • ↑(B i) ⊆ ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ∈ AddGroupFilterBasis.toFilterBasis.sets
[PROOFSTEP]
use i
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ univ • ↑(B i) ⊆ ↑(B i)
[PROOFSTEP]
rintro _ ⟨a, m, -, hm, rfl⟩
[GOAL]
case h.right.intro.intro.intro.intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
a : R
m : M
hm : m ∈ ↑(B i)
⊢ (fun x x_1 => x • x_1) a m ∈ ↑(B i)
[PROOFSTEP]
exact (B i).smul_mem _ hm
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ (x₀ : R) {U : Set M},
    U ∈ AddGroupFilterBasis.toFilterBasis.sets →
      ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x₀ • x) ⁻¹' U
[PROOFSTEP]
rintro x₀ _ ⟨i, rfl⟩
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x₀ • x) ⁻¹' ↑(B i)
[PROOFSTEP]
use B i
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
⊢ ↑(B i) ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ ↑(B i) ⊆ (fun x => x₀ • x) ⁻¹' ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
⊢ ↑(B i) ∈ AddGroupFilterBasis.toFilterBasis.sets
[PROOFSTEP]
use i
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
⊢ ↑(B i) ⊆ (fun x => x₀ • x) ⁻¹' ↑(B i)
[PROOFSTEP]
intro m
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
m : M
⊢ m ∈ ↑(B i) → m ∈ (fun x => x₀ • x) ⁻¹' ↑(B i)
[PROOFSTEP]
exact (B i).smul_mem _
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ (m₀ : M) {U : Set M}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U
[PROOFSTEP]
rintro m₀ _ ⟨i, rfl⟩
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
m₀ : M
i : ι
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ ↑(B i)
[PROOFSTEP]
exact hB.smul m₀ i
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := topology hB
src✝ : AddSubgroup M := Submodule.toAddSubgroup (B i)
⊢ IsOpen
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
letI := hB.topology
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := topology hB
src✝ : AddSubgroup M := Submodule.toAddSubgroup (B i)
this : TopologicalSpace M := topology hB
⊢ IsOpen
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rw [isOpen_iff_mem_nhds]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := topology hB
src✝ : AddSubgroup M := Submodule.toAddSubgroup (B i)
this : TopologicalSpace M := topology hB
⊢ ∀ (a : M),
    a ∈
        { toAddSubmonoid := src✝.toAddSubmonoid,
                neg_mem' :=
                  (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
      { toAddSubmonoid := src✝.toAddSubmonoid,
                neg_mem' :=
                  (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier ∈
        𝓝 a
[PROOFSTEP]
intro a a_in
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := topology hB
src✝ : AddSubgroup M := Submodule.toAddSubgroup (B i)
this : TopologicalSpace M := topology hB
a : M
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' :=
              (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier ∈
    𝓝 a
[PROOFSTEP]
rw [(hB.toModuleFilterBasis.toAddGroupFilterBasis.nhds_hasBasis a).mem_iff]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := topology hB
src✝ : AddSubgroup M := Submodule.toAddSubgroup (B i)
this : TopologicalSpace M := topology hB
a : M
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ∃ i,
    i ∈ (toModuleFilterBasis hB).toAddGroupFilterBasis ∧
      (fun y => a + y) '' i ⊆
        { toAddSubmonoid := src✝.toAddSubmonoid,
                neg_mem' :=
                  (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
use B i
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := topology hB
src✝ : AddSubgroup M := Submodule.toAddSubgroup (B i)
this : TopologicalSpace M := topology hB
a : M
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ↑(B i) ∈ (toModuleFilterBasis hB).toAddGroupFilterBasis ∧
    (fun y => a + y) '' ↑(B i) ⊆
      { toAddSubmonoid := src✝.toAddSubmonoid,
              neg_mem' :=
                (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := topology hB
src✝ : AddSubgroup M := Submodule.toAddSubgroup (B i)
this : TopologicalSpace M := topology hB
a : M
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ↑(B i) ∈ (toModuleFilterBasis hB).toAddGroupFilterBasis
[PROOFSTEP]
use i
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := topology hB
src✝ : AddSubgroup M := Submodule.toAddSubgroup (B i)
this : TopologicalSpace M := topology hB
a : M
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ (fun y => a + y) '' ↑(B i) ⊆
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rintro - ⟨b, b_in, rfl⟩
[GOAL]
case h.right.intro.intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := topology hB
src✝ : AddSubgroup M := Submodule.toAddSubgroup (B i)
this : TopologicalSpace M := topology hB
a : M
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
b : M
b_in : b ∈ ↑(B i)
⊢ (fun y => a + y) b ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
exact (B i).add_mem a_in b_in
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
⊢ NonarchimedeanAddGroup M
[PROOFSTEP]
letI := hB.topology
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
this : TopologicalSpace M := topology hB
⊢ NonarchimedeanAddGroup M
[PROOFSTEP]
constructor
[GOAL]
case is_nonarchimedean
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
this : TopologicalSpace M := topology hB
⊢ ∀ (U : Set M), U ∈ 𝓝 0 → ∃ V, ↑V ⊆ U
[PROOFSTEP]
intro U hU
[GOAL]
case is_nonarchimedean
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
this : TopologicalSpace M := topology hB
U : Set M
hU : U ∈ 𝓝 0
⊢ ∃ V, ↑V ⊆ U
[PROOFSTEP]
obtain ⟨-, ⟨i, rfl⟩, hi : (B i : Set M) ⊆ U⟩ :=
  hB.toModuleFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff.mp hU
[GOAL]
case is_nonarchimedean.intro.intro.intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
this : TopologicalSpace M := topology hB
U : Set M
hU : U ∈ 𝓝 0
i : ι
hi : ↑(B i) ⊆ U
⊢ ∃ V, ↑V ⊆ U
[PROOFSTEP]
exact ⟨hB.openAddSubgroup i, hi⟩
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : SubmodulesBasis BR B
x✝ : TopologicalSpace R := topology BR
⊢ ∀ (m : M) (i : ι), ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
[PROOFSTEP]
letI := BR.topology
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : SubmodulesBasis BR B
x✝ : TopologicalSpace R := topology BR
this : TopologicalSpace R := topology BR
⊢ ∀ (m : M) (i : ι), ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
[PROOFSTEP]
intro m i
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : SubmodulesBasis BR B
x✝ : TopologicalSpace R := topology BR
this : TopologicalSpace R := topology BR
m : M
i : ι
⊢ ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
[PROOFSTEP]
rcases hB.smul m i with ⟨V, V_in, hV⟩
[GOAL]
case intro.intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : SubmodulesBasis BR B
x✝ : TopologicalSpace R := topology BR
this : TopologicalSpace R := topology BR
m : M
i : ι
V : Set R
V_in : V ∈ BR
hV : V ⊆ (fun x => x • m) ⁻¹' ↑(B i)
⊢ ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
[PROOFSTEP]
exact mem_of_superset (BR.toAddGroupFilterBasis.mem_nhds_zero V_in) hV
