-- Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.lean
theorem hasBasis_nhds_zero_adic (I : Ideal R) :
    HasBasis (@nhds R I.adicTopology (0 : R)) (fun _n : ℕ => True) fun n =>
      ((I ^ n : Ideal R) : Set R) :=
  ⟨by
    intro U
    rw [I.ringFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff]
    constructor
    · rintro ⟨-, ⟨i, rfl⟩, h⟩
      replace h : ↑(I ^ i) ⊆ U

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

Tactic:
exact ⟨i, trivial, h⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (t : Set R), t ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ t

Tactic:
intro U

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ U ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ U

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i ∈ RingFilterBasis.toAddGroupFilterBasis, id i ⊆ U) ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ U

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ 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 ∈ RingFilterBasis.toAddGroupFilterBasis, id i ⊆ U

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

Tactic:
simpa using h

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i, True ∧ ↑(I ^ i) ⊆ U) → ∃ i ∈ RingFilterBasis.toAddGroupFilterBasis, id i ⊆ U

Tactic:
rintro ⟨i, -, h⟩

Result:
case mpr.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : ↑(I ^ i) ⊆ U
⊢ ∃ i ∈ RingFilterBasis.toAddGroupFilterBasis, id i ⊆ U

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ U ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ U

Tactic:
rw [I.ringFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff]

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i ∈ RingFilterBasis.toAddGroupFilterBasis, id i ⊆ U) ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ U

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

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : ↑(I ^ i) ⊆ U
⊢ ∃ i ∈ RingFilterBasis.toAddGroupFilterBasis, id i ⊆ U

Tactic:
exact ⟨(I ^ i : Ideal R), ⟨i, by simp⟩, h⟩

Result:
no goals

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

Tactic:
replace h : ↑(I ^ i) ⊆ U := by simpa using h

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

Proof state:
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i ∈ RingFilterBasis.toAddGroupFilterBasis, id i ⊆ U) → ∃ i, True ∧ ↑(I ^ i) ⊆ U

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

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