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
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
intro s
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
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
rw [hB.toRingFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff]
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

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
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
constructor
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
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
rintro ⟨-, ⟨i, rfl⟩, hi⟩
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
s : Set A
i : ι
hi : id ↑(B i) ⊆ s
⊢ ∃ i, True ∧ ↑(B i) ⊆ s
exact ⟨i, trivial, hi⟩
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
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
rintro ⟨i, -, hi⟩
no goals
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
exact ⟨B i, ⟨i, rfl⟩, hi⟩