-- Mathlib/RingTheory/AdicCompletion/Basic.lean
theorem isAdicCauchy_iff (f : ℕ → M) :
    IsAdicCauchy I M f ↔ ∀ n, f n ≡ f (n + 1) [SMOD (I ^ n • ⊤ : Submodule R M)]

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n✝ n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD I ^ m • ⊤]
⊢ f n ≡ f (n + 1) [SMOD I ^ m • ⊤]

Tactic:
refine SModEq.mono (smul_mono (Ideal.pow_le_pow_right hmn) (by rfl)) (h n)

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n✝ n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD I ^ m • ⊤]
⊢ ⊤ ≤ ⊤

Tactic:
rfl

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
⊢ (∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]) → IsAdicCauchy I M f

Tactic:
intro h m n hmn

Result:
case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n : ℕ
hmn : m ≤ n
⊢ f m ≡ f n [SMOD I ^ m • ⊤]

Proof state:
case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
⊢ IsAdicCauchy I M f → ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]

Tactic:
intro h n

Result:
case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : IsAdicCauchy I M f
n : ℕ
⊢ f n ≡ f (n + 1) [SMOD I ^ n • ⊤]

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n✝ n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD I ^ m • ⊤]
⊢ f m ≡ ?m.351446 [SMOD I ^ m • ⊤]

Tactic:
exact ih

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : IsAdicCauchy I M f
n : ℕ
⊢ f n ≡ f (n + 1) [SMOD I ^ n • ⊤]

Tactic:
exact h (Nat.le_succ n)

Result:
no goals

Proof state:
case mpr.base
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n : ℕ
⊢ f m ≡ f m [SMOD I ^ m • ⊤]

Tactic:
rfl

Result:
no goals

Proof state:
case mpr.succ
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n✝ n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD I ^ m • ⊤]
⊢ f m ≡ f (n + 1) [SMOD I ^ m • ⊤]

Tactic:
trans

Result:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n✝ n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD I ^ m • ⊤]
⊢ f m ≡ ?m.351446 [SMOD I ^ m • ⊤]

R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n✝ n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD I ^ m • ⊤]
⊢ ?m.351446 ≡ f (n + 1) [SMOD I ^ m • ⊤]

R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
m n✝ n : ℕ
hmn : m ≤ n
ih : f m ≡ f n [SMOD I ^ m • ⊤]
⊢ M

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
⊢ IsAdicCauchy I M f ↔ ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
⊢ IsAdicCauchy I M f → ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]

case mpr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → M
⊢ (∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]) → IsAdicCauchy I M f