-- Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.lean
theorem isAdic_iff [top : TopologicalSpace R] [IsTopologicalRing R] {J : Ideal R} :
    IsAdic J ↔
      (∀ n : ℕ, IsOpen ((J ^ n : Ideal R) : Set R)) ∧
        ∀ s ∈ 𝓝 (0 : R), ∃ n : ℕ, ((J ^ n : Ideal R) : Set R) ⊆ s

Proof state:
case mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : IsAdic J
⊢ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s

Tactic:
change _ = _ at H

Result:
case mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : top = J.adicTopology
⊢ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s

Proof state:
case mpr.intro.h
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
⊢ 𝓝 0 = 𝓝 0

Tactic:
ext s

Result:
case mpr.intro.h.h
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
⊢ s ∈ 𝓝 0 ↔ s ∈ 𝓝 0

Proof state:
case mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
⊢ ((∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s) → IsAdic J

Tactic:
rintro ⟨H₁, H₂⟩

Result:
case mpr.intro
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
⊢ IsAdic J

Proof state:
case mpr.intro.h.h
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
⊢ s ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(J ^ i) ⊆ s

Tactic:
constructor <;> intro H

Result:
case mpr.intro.h.h.mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
H : s ∈ 𝓝 0
⊢ ∃ i, True ∧ ↑(J ^ i) ⊆ s

case mpr.intro.h.h.mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
H : ∃ i, True ∧ ↑(J ^ i) ⊆ s
⊢ s ∈ 𝓝 0

Proof state:
case mpr.intro.tg
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
⊢ IsTopologicalAddGroup R

Tactic:
apply @IsTopologicalRing.to_topologicalAddGroup

Result:
no goals

Proof state:
case mpr.intro
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
⊢ IsAdic J

Tactic:
apply IsTopologicalAddGroup.ext

Result:
case mpr.intro.tg
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
⊢ IsTopologicalAddGroup R

case mpr.intro.tg'
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
⊢ IsTopologicalAddGroup R

case mpr.intro.h
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
⊢ 𝓝 0 = 𝓝 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
⊢ IsAdic J ↔ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
⊢ IsAdic J → (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s

case mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
⊢ ((∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s) → IsAdic J

Proof state:
case mp.left
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : top = J.adicTopology
this : TopologicalSpace R := J.adicTopology
n : ℕ
⊢ IsOpen ↑(J ^ n)

Tactic:
exact (J.openAddSubgroup n).isOpen'

Result:
no goals

Proof state:
case mpr.intro.h.h.mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
H : ∃ i, True ∧ ↑(J ^ i) ⊆ s
⊢ s ∈ 𝓝 0

Tactic:
rcases H with ⟨n, -, hn⟩

Result:
case mpr.intro.h.h.mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
n : ℕ
hn : ↑(J ^ n) ⊆ s
⊢ s ∈ 𝓝 0

Proof state:
case mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : top = J.adicTopology
⊢ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s

Tactic:
letI := J.adicTopology

Result:
case mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : top = J.adicTopology
this : TopologicalSpace R := J.adicTopology
⊢ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s

Proof state:
case mpr.intro.h.h
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
⊢ s ∈ 𝓝 0 ↔ s ∈ 𝓝 0

Tactic:
letI := Ideal.adic_basis J

Result:
case mpr.intro.h.h
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
⊢ s ∈ 𝓝 0 ↔ s ∈ 𝓝 0

Proof state:
case mpr.intro.h.h.mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
H : s ∈ 𝓝 0
⊢ ∃ i, True ∧ ↑(J ^ i) ⊆ s

Tactic:
rcases H₂ s H with ⟨n, h⟩

Result:
case mpr.intro.h.h.mp.intro
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
H : s ∈ 𝓝 0
n : ℕ
h : ↑(J ^ n) ⊆ s
⊢ ∃ i, True ∧ ↑(J ^ i) ⊆ s

Proof state:
case mp.left
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : top = J.adicTopology
this : TopologicalSpace R := J.adicTopology
⊢ ∀ (n : ℕ), IsOpen ↑(J ^ n)

Tactic:
intro n

Result:
case mp.left
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : top = J.adicTopology
this : TopologicalSpace R := J.adicTopology
n : ℕ
⊢ IsOpen ↑(J ^ n)

Proof state:
case mpr.intro.h.h.mp.intro
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
H : s ∈ 𝓝 0
n : ℕ
h : ↑(J ^ n) ⊆ s
⊢ ∃ i, True ∧ ↑(J ^ i) ⊆ s

Tactic:
exact ⟨n, trivial, h⟩

Result:
no goals