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
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
intro s
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
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
rw [(hB.toRingFilterBasis.toAddGroupFilterBasis.nhds_hasBasis a).mem_iff]
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
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
simp only [true_and]
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

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
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
constructor
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
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
rintro ⟨-, ⟨i, rfl⟩, hi⟩
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
⊢ {b | b - a ∈ B i} ⊆ s
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
use i
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
h : {b | b - a ∈ B i} = (fun y => a + y) '' ↑(B i)
⊢ {b | b - a ∈ B i} ⊆ s

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)
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
⊢ {b | b - a ∈ B i} ⊆ s
suffices h : { b : A | b - a ∈ B i } = (fun y => a + y) '' ↑(B i)
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)
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)
simp only [image_add_left, neg_add_eq_sub]
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)
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)
ext b
no goals
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)
simp
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
h : {b | b - a ∈ B i} = (fun y => a + y) '' ↑(B i)
⊢ (fun y => a + y) '' ↑(B i) ⊆ s
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
h : {b | b - a ∈ B i} = (fun y => a + y) '' ↑(B i)
⊢ {b | b - a ∈ B i} ⊆ s
rw [h]
no goals
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
h : {b | b - a ∈ B i} = (fun y => a + y) '' ↑(B i)
⊢ (fun y => a + y) '' ↑(B i) ⊆ s
assumption
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
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
rintro ⟨i, hi⟩
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
⊢ ↑(B i) ∈ RingFilterBasis.toAddGroupFilterBasis ∧ (fun y => a + y) '' ↑(B i) ⊆ s
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
use B i
case mpr.intro.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 mpr.intro.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
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
⊢ ↑(B i) ∈ RingFilterBasis.toAddGroupFilterBasis ∧ (fun y => a + y) '' ↑(B i) ⊆ s
constructor
no goals
case mpr.intro.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
use i
case mpr.intro.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
case mpr.intro.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
rw [image_subset_iff]
case mpr.intro.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
case mpr.intro.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
rintro b b_in
case mpr.intro.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}
case mpr.intro.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
apply hi
no goals
case mpr.intro.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}
simpa using b_in