-- Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.lean
theorem adic_basis (I : Ideal R) : SubmodulesRingBasis fun n : ℕ => (I ^ n • ⊤ : Ideal R) :=
  { inter

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i j : ℕ), ∃ k, I ^ k • ⊤ ≤ I ^ i • ⊤ ⊓ I ^ j • ⊤

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

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i j : ℕ), ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
r : R
n : ℕ
⊢ ∃ j, r • I ^ j ≤ I ^ n

Tactic:
use n

Result:
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
r : R
n : ℕ
⊢ r • I ^ n ≤ I ^ n

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ ∃ j, ↑(I ^ j) * ↑(I ^ j) ⊆ ↑(I ^ n)

Tactic:
use n

Result:
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ ↑(I ^ n) * ↑(I ^ n) ⊆ ↑(I ^ n)

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
r : R
n : ℕ
⊢ r • I ^ n ≤ I ^ n

Tactic:
rintro a ⟨x, hx, rfl⟩

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

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

Tactic:
simpa only [smul_top_eq_map, Algebra.id.map_eq_id, map_id] using this

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
i j : ℕ
⊢ ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j

Tactic:
exact ⟨max i j, pow_le_pow_right (le_max_left i j), pow_le_pow_right (le_max_right i j)⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i : ℕ), ∃ j, ↑(I ^ j) * ↑(I ^ j) ⊆ ↑(I ^ i)

Tactic:
intro n

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ ∃ j, ↑(I ^ j) * ↑(I ^ j) ⊆ ↑(I ^ n)

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

Tactic:
exact (I ^ n).smul_mem r hx

Result:
no goals

Proof state:
case h.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
x : R
_hx : x ∈ ↑(I ^ n)
b : R
hb : b ∈ ↑(I ^ n)
⊢ (fun x1 x2 => x1 * x2) x b ∈ ↑(I ^ n)

Tactic:
exact (I ^ n).smul_mem x hb

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
⊢ ↑(I ^ n) * ↑(I ^ n) ⊆ ↑(I ^ n)

Tactic:
rintro a ⟨x, _hx, b, hb, rfl⟩

Result:
case h.intro.intro.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
x : R
_hx : x ∈ ↑(I ^ n)
b : R
hb : b ∈ ↑(I ^ n)
⊢ (fun x1 x2 => x1 * x2) x b ∈ ↑(I ^ n)

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j • ⊤ ≤ I ^ i • ⊤

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

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j ≤ I ^ i

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

Tactic:
simpa only [smul_top_eq_map, Algebra.id.map_eq_id, map_id] using this

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i j : ℕ), ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j

Tactic:
intro i j

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
i j : ℕ
⊢ ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j

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

Tactic:
simpa only [smul_eq_mul, mul_top, Algebra.id.map_eq_id, map_id, le_inf_iff] using this

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (a : R) (i : ℕ), ∃ j, a • I ^ j ≤ I ^ i

Tactic:
intro r n

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
r : R
n : ℕ
⊢ ∃ j, r • I ^ j ≤ I ^ n

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i : ℕ), ∃ j, ↑(I ^ j • ⊤) * ↑(I ^ j • ⊤) ⊆ ↑(I ^ i • ⊤)

Tactic:
suffices ∀ i : ℕ, ∃ j : ℕ, (↑(I ^ j) * ↑(I ^ j) : Set R) ⊆ (↑(I ^ i) : Set R) by
  simpa only [smul_top_eq_map, Algebra.id.map_eq_id, map_id] using this

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i : ℕ), ∃ j, ↑(I ^ j) * ↑(I ^ j) ⊆ ↑(I ^ i)