-- Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean
theorem hasBasis_nhds (a : A) :
    HasBasis (@nhds A hB.topology a) (fun _ => True) fun i => { b | b - a ∈ B i } :=
  ⟨by
    intro s
    rw [(hB.toRingFilterBasis.toAddGroupFilterBasis.nhds_hasBasis a).mem_iff]
    simp only [true_and]
    constructor
    · rintro ⟨-, ⟨i, rfl⟩, hi⟩
      use i
      suffices h : { b : A | b - a ∈ B i } = (fun y => a + y) '' ↑(B i) by
        rw [h]
        assumption
      simp only [image_add_left, neg_add_eq_sub]
      ext b
      simp
    · rintro ⟨i, hi⟩
      use B i
      constructor
      · use i
      · rw [image_subset_iff]
        rintro b b_in
        apply hi
        simpa using b_in⟩

Proof state:
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

Tactic:
assumption

Result:
no goals

Proof state:
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

Tactic:
rw [image_subset_iff]

Result:
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

Proof state:
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

Tactic:
rintro b b_in

Result:
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

Proof state:
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

Tactic:
suffices h : { b : A | b - a ∈ B i } = (fun y => a + y) '' ↑(B i) by
  rw [h]
  assumption

Result:
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)

Proof state:
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
⊢ (∃ i ∈ RingFilterBasis.toAddGroupFilterBasis, (fun y => a + y) '' i ⊆ s) ↔ ∃ i, True ∧ {b | b - a ∈ B i} ⊆ s

Tactic:
simp only [true_and]

Result:
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
⊢ (∃ i ∈ RingFilterBasis.toAddGroupFilterBasis, (fun y => a + y) '' i ⊆ s) ↔ ∃ i, {b | b - a ∈ B i} ⊆ s

Proof state:
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)

Tactic:
ext b

Result:
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)

Proof state:
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

Tactic:
rw [h]

Result:
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

Proof state:
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 ∈ RingFilterBasis.toAddGroupFilterBasis, (fun y => a + y) '' i ⊆ s) → ∃ i, {b | b - a ∈ B i} ⊆ s

Tactic:
rintro ⟨-, ⟨i, rfl⟩, hi⟩

Result:
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

Proof state:
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

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

Result:
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
⊢ (∃ i ∈ RingFilterBasis.toAddGroupFilterBasis, (fun y => a + y) '' i ⊆ s) ↔ ∃ i, True ∧ {b | b - a ∈ B i} ⊆ s

Proof state:
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

Tactic:
intro s

Result:
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

Proof state:
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)

Tactic:
simp

Result:
no goals

Proof state:
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

Tactic:
apply hi

Result:
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}

Proof state:
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

Tactic:
constructor

Result:
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

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

Proof state:
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
⊢ (∃ i ∈ RingFilterBasis.toAddGroupFilterBasis, (fun y => a + y) '' i ⊆ s) ↔ ∃ i, {b | b - a ∈ B i} ⊆ s

Tactic:
constructor

Result:
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 ∈ RingFilterBasis.toAddGroupFilterBasis, (fun y => a + y) '' i ⊆ s) → ∃ i, {b | b - a ∈ B i} ⊆ s

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 ∈ RingFilterBasis.toAddGroupFilterBasis, (fun y => a + y) '' i ⊆ s