R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ U ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ U
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (t : Set R), t ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ t
intro U
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ U) ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ U
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ U ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ U
rw [I.ringFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff]
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ U) → ∃ i, True ∧ ↑(I ^ i) ⊆ U

case mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i, True ∧ ↑(I ^ i) ⊆ U) → ∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ U
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ U) ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ U
constructor
case mp.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : id ↑((fun i => toAddSubgroup (I ^ i • ⊤)) i) ⊆ U
⊢ ∃ i, True ∧ ↑(I ^ i) ⊆ U
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ U) → ∃ i, True ∧ ↑(I ^ i) ⊆ U
rintro ⟨-, ⟨i, rfl⟩, h⟩
case mp.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : ↑(I ^ i) ⊆ U
⊢ ∃ i, True ∧ ↑(I ^ i) ⊆ U
case mp.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : id ↑((fun i => toAddSubgroup (I ^ i • ⊤)) i) ⊆ U
⊢ ∃ i, True ∧ ↑(I ^ i) ⊆ U
replace h : ↑(I ^ i) ⊆ U := by simpa using h
no goals
case mp.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : ↑(I ^ i) ⊆ U
⊢ ∃ i, True ∧ ↑(I ^ i) ⊆ U
exact ⟨i, trivial, h⟩
no goals
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : id ↑((fun i => toAddSubgroup (I ^ i • ⊤)) i) ⊆ U
⊢ ↑(I ^ i) ⊆ U
simpa using h
case mpr.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : ↑(I ^ i) ⊆ U
⊢ ∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ U
case mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i, True ∧ ↑(I ^ i) ⊆ U) → ∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ U
rintro ⟨i, -, h⟩
no goals
case mpr.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : ↑(I ^ i) ⊆ U
⊢ ∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ U
exact ⟨(I ^ i : Ideal R), ⟨i, by simp⟩, h⟩
no goals
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : ↑(I ^ i) ⊆ U
⊢ ↑(I ^ i) = ↑((fun i => toAddSubgroup (I ^ i • ⊤)) i)
simp