R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
⊢ (∀ (n_1 : ℕ), IsOpen ↑((J ^ n) ^ n_1)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ s
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : IsAdic J
n : ℕ
hn : 0 < n
⊢ IsAdic (J ^ n)
rw [isAdic_iff] at h⊢
case left
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
⊢ ∀ (n_1 : ℕ), IsOpen ↑((J ^ n) ^ n_1)

case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
⊢ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ s
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
⊢ (∀ (n_1 : ℕ), IsOpen ↑((J ^ n) ^ n_1)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ s
constructor
case left
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
m : ℕ
⊢ IsOpen ↑((J ^ n) ^ m)
case left
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
⊢ ∀ (n_1 : ℕ), IsOpen ↑((J ^ n) ^ n_1)
intro m
case left
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
m : ℕ
⊢ IsOpen ↑(J ^ (n * m))
case left
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
m : ℕ
⊢ IsOpen ↑((J ^ n) ^ m)
rw [← pow_mul]
no goals
case left
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
m : ℕ
⊢ IsOpen ↑(J ^ (n * m))
apply h.left
case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
V : Set R
hV : V ∈ 𝓝 0
⊢ ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ V
case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
⊢ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ s
intro V hV
case right.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
⊢ ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ V
case right
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
V : Set R
hV : V ∈ 𝓝 0
⊢ ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ V
cases' h.right V hV with m hm
case right.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
⊢ ↑((J ^ n) ^ m) ⊆ V
case right.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
⊢ ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ V
use m
case right.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
⊢ ↑((J ^ n) ^ m) ⊆ ↑(J ^ m)
case right.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
⊢ ↑((J ^ n) ^ m) ⊆ V
refine' Set.Subset.trans _ hm
case right.intro.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
hn : 0 < Nat.zero
⊢ ↑((J ^ Nat.zero) ^ m) ⊆ ↑(J ^ m)

case right.intro.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
n✝ : ℕ
hn : 0 < Nat.succ n✝
⊢ ↑((J ^ Nat.succ n✝) ^ m) ⊆ ↑(J ^ m)
case right.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
⊢ ↑((J ^ n) ^ m) ⊆ ↑(J ^ m)
cases n
case right.intro.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
n✝ : ℕ
hn : 0 < Nat.succ n✝
⊢ ↑(J ^ (n✝ * m + m)) ⊆ ↑(J ^ m)
case right.intro.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
n✝ : ℕ
hn : 0 < Nat.succ n✝
⊢ ↑((J ^ Nat.succ n✝) ^ m) ⊆ ↑(J ^ m)
rw [← pow_mul, Nat.succ_mul]
case right.intro.succ.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
n✝ : ℕ
hn : 0 < Nat.succ n✝
⊢ m ≤ n✝ * m + m
case right.intro.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
n✝ : ℕ
hn : 0 < Nat.succ n✝
⊢ ↑(J ^ (n✝ * m + m)) ⊆ ↑(J ^ m)
apply Ideal.pow_le_pow
no goals
case right.intro.succ.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
n✝ : ℕ
hn : 0 < Nat.succ n✝
⊢ m ≤ n✝ * m + m
apply Nat.le_add_left
case right.intro.zero.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
hn : 0 < Nat.zero
⊢ False
case right.intro.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
hn : 0 < Nat.zero
⊢ ↑((J ^ Nat.zero) ^ m) ⊆ ↑(J ^ m)
exfalso
no goals
case right.intro.zero.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
hn : 0 < Nat.zero
⊢ False
exact Nat.not_succ_le_zero 0 hn