[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i j : ℕ), ∃ k, I ^ k • ⊤ ≤ I ^ i • ⊤ ⊓ I ^ j • ⊤
[PROOFSTEP]
suffices ∀ i j : ℕ, ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j by
  simpa only [smul_eq_mul, mul_top, Algebra.id.map_eq_id, map_id, le_inf_iff] using this
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
this : ∀ (i j : ℕ), ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j
⊢ ∀ (i j : ℕ), ∃ k, I ^ k • ⊤ ≤ I ^ i • ⊤ ⊓ I ^ j • ⊤
[PROOFSTEP]
simpa only [smul_eq_mul, mul_top, Algebra.id.map_eq_id, map_id, le_inf_iff] using this
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i j : ℕ), ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j
[PROOFSTEP]
intro i j
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
i j : ℕ
⊢ ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j
[PROOFSTEP]
exact ⟨max i j, pow_le_pow (le_max_left i j), pow_le_pow (le_max_right i j)⟩
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j • ⊤ ≤ I ^ i • ⊤
[PROOFSTEP]
suffices ∀ (a : R) (i : ℕ), ∃ j : ℕ, a • I ^ j ≤ I ^ i by
  simpa only [smul_top_eq_map, Algebra.id.map_eq_id, map_id] using this
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
this : ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j ≤ I ^ i
⊢ ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j • ⊤ ≤ I ^ i • ⊤
[PROOFSTEP]
simpa only [smul_top_eq_map, Algebra.id.map_eq_id, map_id] using this
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j ≤ I ^ i
[PROOFSTEP]
intro r n
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
r : R
n : ℕ
⊢ ∃ j, r • I ^ j ≤ I ^ n
[PROOFSTEP]
use n
[GOAL]
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
r : R
n : ℕ
⊢ r • I ^ n ≤ I ^ n
[PROOFSTEP]
rintro a ⟨x, hx, rfl⟩
[GOAL]
case h.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
r : R
n : ℕ
x : R
hx : x ∈ ↑(I ^ n)
⊢ ↑(DistribMulAction.toLinearMap R R r) x ∈ I ^ n
[PROOFSTEP]
exact (I ^ n).smul_mem r hx
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i : ℕ), ∃ j, ↑(I ^ j • ⊤) * ↑(I ^ j • ⊤) ⊆ ↑(I ^ i • ⊤)
[PROOFSTEP]
suffices ∀ i : ℕ, ∃ j : ℕ, (I ^ j : Set R) * (I ^ j : Set R) ⊆ (I ^ i : Set R) by
  simpa only [smul_top_eq_map, Algebra.id.map_eq_id, map_id] using this
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
this : ∀ (i : ℕ), ∃ j, ↑(I ^ j) * ↑(I ^ j) ⊆ ↑(I ^ i)
⊢ ∀ (i : ℕ), ∃ j, ↑(I ^ j • ⊤) * ↑(I ^ j • ⊤) ⊆ ↑(I ^ i • ⊤)
[PROOFSTEP]
simpa only [smul_top_eq_map, Algebra.id.map_eq_id, map_id] using this
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i : ℕ), ∃ j, ↑(I ^ j) * ↑(I ^ j) ⊆ ↑(I ^ i)
[PROOFSTEP]
intro n
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ ∃ j, ↑(I ^ j) * ↑(I ^ j) ⊆ ↑(I ^ n)
[PROOFSTEP]
use n
[GOAL]
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ ↑(I ^ n) * ↑(I ^ n) ⊆ ↑(I ^ n)
[PROOFSTEP]
rintro a ⟨x, b, _hx, hb, rfl⟩
[GOAL]
case h.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
x b : R
_hx : x ∈ ↑(I ^ n)
hb : b ∈ ↑(I ^ n)
⊢ (fun x x_1 => x * x_1) x b ∈ ↑(I ^ n)
[PROOFSTEP]
exact (I ^ n).smul_mem x hb
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (t : Set R), t ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ t
[PROOFSTEP]
intro U
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ U ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ U
[PROOFSTEP]
rw [I.ringFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff]
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
rintro ⟨-, ⟨i, rfl⟩, h⟩
[GOAL]
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
[PROOFSTEP]
replace h : ↑(I ^ i) ⊆ U := by simpa using h
[GOAL]
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
[PROOFSTEP]
simpa using h
[GOAL]
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
[PROOFSTEP]
exact ⟨i, trivial, h⟩
[GOAL]
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
[PROOFSTEP]
rintro ⟨i, -, h⟩
[GOAL]
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
[PROOFSTEP]
exact ⟨(I ^ i : Ideal R), ⟨i, by simp⟩, h⟩
[GOAL]
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)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x : R
⊢ HasBasis (𝓝 x) (fun _n => True) fun n => (fun y => x + y) '' ↑(I ^ n)
[PROOFSTEP]
letI := I.adicTopology
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x : R
this : TopologicalSpace R := adicTopology I
⊢ HasBasis (𝓝 x) (fun _n => True) fun n => (fun y => x + y) '' ↑(I ^ n)
[PROOFSTEP]
have := I.hasBasis_nhds_zero_adic.map fun y => x + y
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x : R
this✝ : TopologicalSpace R := adicTopology I
this : HasBasis (Filter.map (fun y => x + y) (𝓝 0)) (fun _n => True) fun i => (fun y => x + y) '' ↑(I ^ i)
⊢ HasBasis (𝓝 x) (fun _n => True) fun n => (fun y => x + y) '' ↑(I ^ n)
[PROOFSTEP]
rwa [map_add_left_nhds_zero x] at this 
[GOAL]
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
⊢ ↑(I ^ i • ⊤) = ↑((fun i => toAddSubgroup (I ^ i • ⊤)) i)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
a : R
a_in : a ∈ ↑(I ^ i • ⊤)
⊢ a ∈ (fun x => x • m) ⁻¹' ↑(I ^ i • ⊤)
[PROOFSTEP]
replace a_in : a ∈ I ^ i := by simpa [(I ^ i).mul_top] using a_in
[GOAL]
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
a : R
a_in : a ∈ ↑(I ^ i • ⊤)
⊢ a ∈ I ^ i
[PROOFSTEP]
simpa [(I ^ i).mul_top] using a_in
[GOAL]
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
a : R
a_in : a ∈ I ^ i
⊢ a ∈ (fun x => x • m) ⁻¹' ↑(I ^ i • ⊤)
[PROOFSTEP]
exact smul_mem_smul a_in mem_top
[GOAL]
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ OpenAddSubgroup R
[PROOFSTEP]
letI := I.adicTopology
[GOAL]
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
this : TopologicalSpace R := adicTopology I
⊢ OpenAddSubgroup R
[PROOFSTEP]
refine ⟨(I ^ n).toAddSubgroup, ?_⟩
[GOAL]
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
this : TopologicalSpace R := adicTopology I
⊢ IsOpen (toAddSubgroup (I ^ n)).toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
convert (I.adic_basis.toRing_subgroups_basis.openAddSubgroup n).isOpen
[GOAL]
case h.e'_3
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
this : TopologicalSpace R := adicTopology I
⊢ (toAddSubgroup (I ^ n)).toAddSubmonoid.toAddSubsemigroup.carrier =
    ↑(RingSubgroupsBasis.openAddSubgroup (_ : RingSubgroupsBasis fun i => toAddSubgroup (I ^ i • ⊤)) n)
[PROOFSTEP]
change (I ^ n : Set R) = (I ^ n • (⊤ : Ideal R) : Set R)
[GOAL]
case h.e'_3
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
this : TopologicalSpace R := adicTopology I
⊢ ↑(I ^ n) = ↑(I ^ n • ⊤)
[PROOFSTEP]
simp [smul_top_eq_map, Algebra.id.map_eq_id, map_id, restrictScalars_self]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
⊢ IsAdic J ↔ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
⊢ IsAdic J → (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
[PROOFSTEP]
intro H
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H : IsAdic J
⊢ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
[PROOFSTEP]
change _ = _ at H 
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H : top = Ideal.adicTopology J
⊢ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
[PROOFSTEP]
rw [H]
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H : top = Ideal.adicTopology J
⊢ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
[PROOFSTEP]
letI := J.adicTopology
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H : top = Ideal.adicTopology J
this : TopologicalSpace R := Ideal.adicTopology J
⊢ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp.left
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H : top = Ideal.adicTopology J
this : TopologicalSpace R := Ideal.adicTopology J
⊢ ∀ (n : ℕ), IsOpen ↑(J ^ n)
[PROOFSTEP]
intro n
[GOAL]
case mp.left
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H : top = Ideal.adicTopology J
this : TopologicalSpace R := Ideal.adicTopology J
n : ℕ
⊢ IsOpen ↑(J ^ n)
[PROOFSTEP]
exact (J.openAddSubgroup n).isOpen'
[GOAL]
case mp.right
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H : top = Ideal.adicTopology J
this : TopologicalSpace R := Ideal.adicTopology J
⊢ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
[PROOFSTEP]
intro s hs
[GOAL]
case mp.right
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H : top = Ideal.adicTopology J
this : TopologicalSpace R := Ideal.adicTopology J
s : Set R
hs : s ∈ 𝓝 0
⊢ ∃ n, ↑(J ^ n) ⊆ s
[PROOFSTEP]
simpa using J.hasBasis_nhds_zero_adic.mem_iff.mp hs
[GOAL]
case mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
⊢ ((∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s) → IsAdic J
[PROOFSTEP]
rintro ⟨H₁, H₂⟩
[GOAL]
case mpr.intro
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
⊢ IsAdic J
[PROOFSTEP]
apply TopologicalAddGroup.ext
[GOAL]
case mpr.intro.tg
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
⊢ TopologicalAddGroup R
[PROOFSTEP]
apply @TopologicalRing.to_topologicalAddGroup
[GOAL]
case mpr.intro.tg'
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
⊢ TopologicalAddGroup R
[PROOFSTEP]
apply (RingSubgroupsBasis.toRingFilterBasis _).toAddGroupFilterBasis.isTopologicalAddGroup
[GOAL]
case mpr.intro.h
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
⊢ 𝓝 0 = 𝓝 0
[PROOFSTEP]
ext s
[GOAL]
case mpr.intro.h.a
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
s : Set R
⊢ s ∈ 𝓝 0 ↔ s ∈ 𝓝 0
[PROOFSTEP]
letI := Ideal.adic_basis J
[GOAL]
case mpr.intro.h.a
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
⊢ s ∈ 𝓝 0 ↔ s ∈ 𝓝 0
[PROOFSTEP]
rw [J.hasBasis_nhds_zero_adic.mem_iff]
[GOAL]
case mpr.intro.h.a
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), 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
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro.h.a.mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), 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
[PROOFSTEP]
intro H
[GOAL]
case mpr.intro.h.a.mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
⊢ (∃ i, True ∧ ↑(J ^ i) ⊆ s) → s ∈ 𝓝 0
[PROOFSTEP]
intro H
[GOAL]
case mpr.intro.h.a.mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), 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
[PROOFSTEP]
rcases H₂ s H with ⟨n, h⟩
[GOAL]
case mpr.intro.h.a.mp.intro
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), 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
[PROOFSTEP]
exact ⟨n, trivial, h⟩
[GOAL]
case mpr.intro.h.a.mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), 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
[PROOFSTEP]
rcases H with ⟨n, -, hn⟩
[GOAL]
case mpr.intro.h.a.mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), 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
[PROOFSTEP]
rw [mem_nhds_iff]
[GOAL]
case mpr.intro.h.a.mpr.intro.intro
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : TopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen ↑(J ^ n)
H₂ : ∀ (s : Set R), s ∈ 𝓝 0 → ∃ n, ↑(J ^ n) ⊆ s
s : Set R
this : SubmodulesRingBasis fun n => J ^ n • ⊤ := Ideal.adic_basis J
n : ℕ
hn : ↑(J ^ n) ⊆ s
⊢ ∃ t, t ⊆ s ∧ IsOpen t ∧ 0 ∈ t
[PROOFSTEP]
refine' ⟨_, hn, H₁ n, (J ^ n).zero_mem⟩
[GOAL]
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)
[PROOFSTEP]
rw [isAdic_iff] at h ⊢
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
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)
[PROOFSTEP]
intro m
[GOAL]
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)
[PROOFSTEP]
rw [← pow_mul]
[GOAL]
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))
[PROOFSTEP]
apply h.left
[GOAL]
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
[PROOFSTEP]
intro V hV
[GOAL]
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
[PROOFSTEP]
cases' h.right V hV with m hm
[GOAL]
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
[PROOFSTEP]
use m
[GOAL]
case 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
n : ℕ
hn : 0 < n
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
⊢ ↑((J ^ n) ^ m) ⊆ V
[PROOFSTEP]
refine' Set.Subset.trans _ hm
[GOAL]
case 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
n : ℕ
hn : 0 < n
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
⊢ ↑((J ^ n) ^ m) ⊆ ↑(J ^ m)
[PROOFSTEP]
cases n
[GOAL]
case h.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)
[PROOFSTEP]
exfalso
[GOAL]
case h.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
[PROOFSTEP]
exact Nat.not_succ_le_zero 0 hn
[GOAL]
case h.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)
[PROOFSTEP]
rw [← pow_mul, Nat.succ_mul]
[GOAL]
case h.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)
[PROOFSTEP]
apply Ideal.pow_le_pow
[GOAL]
case h.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
[PROOFSTEP]
apply Nat.le_add_left
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
⊢ IsAdic ⊥ ↔ DiscreteTopology A
[PROOFSTEP]
rw [isAdic_iff]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
⊢ ((∀ (n : ℕ), IsOpen ↑(⊥ ^ n)) ∧ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s) ↔ DiscreteTopology A
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
⊢ ((∀ (n : ℕ), IsOpen ↑(⊥ ^ n)) ∧ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s) → DiscreteTopology A
[PROOFSTEP]
rintro ⟨h, _h'⟩
[GOAL]
case mp.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
h : ∀ (n : ℕ), IsOpen ↑(⊥ ^ n)
_h' : ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
⊢ DiscreteTopology A
[PROOFSTEP]
rw [discreteTopology_iff_open_singleton_zero]
[GOAL]
case mp.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
h : ∀ (n : ℕ), IsOpen ↑(⊥ ^ n)
_h' : ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
⊢ IsOpen {0}
[PROOFSTEP]
simpa using h 1
[GOAL]
case mpr
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
⊢ DiscreteTopology A → (∀ (n : ℕ), IsOpen ↑(⊥ ^ n)) ∧ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
[PROOFSTEP]
intros
[GOAL]
case mpr
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
⊢ (∀ (n : ℕ), IsOpen ↑(⊥ ^ n)) ∧ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mpr.left
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
⊢ ∀ (n : ℕ), IsOpen ↑(⊥ ^ n)
[PROOFSTEP]
simp
[GOAL]
case mpr.right
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
⊢ ∀ (s : Set A), s ∈ 𝓝 0 → ∃ n, ↑(⊥ ^ n) ⊆ s
[PROOFSTEP]
intro U U_nhds
[GOAL]
case mpr.right
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
U : Set A
U_nhds : U ∈ 𝓝 0
⊢ ∃ n, ↑(⊥ ^ n) ⊆ U
[PROOFSTEP]
use 1
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalRing A
a✝ : DiscreteTopology A
U : Set A
U_nhds : U ∈ 𝓝 0
⊢ ↑(⊥ ^ 1) ⊆ U
[PROOFSTEP]
simp [mem_of_mem_nhds U_nhds]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : WithIdeal R
⊢ NonarchimedeanRing R
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : WithIdeal R
⊢ TopologicalRing (UniformSpace.Completion R)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
inst✝³ : CommRing R
inst✝² : WithIdeal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ TopologicalAddGroup M
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
inst✝³ : CommRing R
inst✝² : WithIdeal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ContinuousSMul R M
[PROOFSTEP]
infer_instance
