-- Mathlib/RingTheory/AdicCompletion/LocalRing.lean
lemma isUnit_iff_nmem_of_isAdicComplete_maximal [IsAdicComplete m R] (r : R) :
    IsUnit r ↔ r ∉ m

Proof state:
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
r : R
h : r ∉ m
mapu : ∀ {n : ℕ}, 0 < n → IsUnit ((mk (m ^ n)) r)
invSeries' : (n : { n // 0 < n }) → R ⧸ m ^ ↑n
invSeries_spec' : ∀ (n : { n // 0 < n }), invSeries' n * (mk (m ^ ↑n)) r = 1
invSeries : ℕ → R := fun n => if h : n = 0 then 0 else Classical.choose ⋯
invSeries_spec : ∀ {n : ℕ} (npos : 0 < n), (mk (m ^ n)) (invSeries n) = invSeries' ⟨n, npos⟩
mod : ∀ {a b : ℕ}, a ≤ b → invSeries a ≡ invSeries b [SMOD m ^ a • ⊤]
inv : R
hinv : ∀ (n : ℕ), invSeries n ≡ inv [SMOD m ^ n • ⊤]
n : ℕ
⊢ inv * r - 1 ≡ 0 [SMOD m ^ n • ⊤]

Tactic:
by_cases npos : 0 < n

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
r : R
h : r ∉ m
mapu : ∀ {n : ℕ}, 0 < n → IsUnit ((mk (m ^ n)) r)
invSeries' : (n : { n // 0 < n }) → R ⧸ m ^ ↑n
invSeries_spec' : ∀ (n : { n // 0 < n }), invSeries' n * (mk (m ^ ↑n)) r = 1
invSeries : ℕ → R := fun n => if h : n = 0 then 0 else Classical.choose ⋯
invSeries_spec : ∀ {n : ℕ} (npos : 0 < n), (mk (m ^ n)) (invSeries n) = invSeries' ⟨n, npos⟩
mod : ∀ {a b : ℕ}, a ≤ b → invSeries a ≡ invSeries b [SMOD m ^ a • ⊤]
inv : R
hinv : ∀ (n : ℕ), invSeries n ≡ inv [SMOD m ^ n • ⊤]
n : ℕ
npos : 0 < n
⊢ inv * r - 1 ≡ 0 [SMOD m ^ n • ⊤]

case neg
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
r : R
h : r ∉ m
mapu : ∀ {n : ℕ}, 0 < n → IsUnit ((mk (m ^ n)) r)
invSeries' : (n : { n // 0 < n }) → R ⧸ m ^ ↑n
invSeries_spec' : ∀ (n : { n // 0 < n }), invSeries' n * (mk (m ^ ↑n)) r = 1
invSeries : ℕ → R := fun n => if h : n = 0 then 0 else Classical.choose ⋯
invSeries_spec : ∀ {n : ℕ} (npos : 0 < n), (mk (m ^ n)) (invSeries n) = invSeries' ⟨n, npos⟩
mod : ∀ {a b : ℕ}, a ≤ b → invSeries a ≡ invSeries b [SMOD m ^ a • ⊤]
inv : R
hinv : ∀ (n : ℕ), invSeries n ≡ inv [SMOD m ^ n • ⊤]
n : ℕ
npos : ¬0 < n
⊢ inv * r - 1 ≡ 0 [SMOD m ^ n • ⊤]

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
r : R
h : r ∉ m
mapu : ∀ {n : ℕ}, 0 < n → IsUnit ((mk (m ^ n)) r)
invSeries' : (n : { n // 0 < n }) → R ⧸ m ^ ↑n
invSeries_spec' : ∀ (n : { n // 0 < n }), invSeries' n * (mk (m ^ ↑n)) r = 1
invSeries : ℕ → R := fun n => if h : n = 0 then 0 else Classical.choose ⋯
invSeries_spec : ∀ {n : ℕ} (npos : 0 < n), (mk (m ^ n)) (invSeries n) = invSeries' ⟨n, npos⟩
a b : ℕ
le : a ≤ b
apos : 0 < a
⊢ (mk (m ^ a)) r * (mk (m ^ a)) (invSeries a) - (mk (m ^ a)) r * (mk (m ^ a)) (invSeries b) = 0

Tactic:
nth_rw 3 [← factor_mk (pow_le_pow_right le), ← factor_mk (pow_le_pow_right le)]

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
r : R
h : r ∉ m
mapu : ∀ {n : ℕ}, 0 < n → IsUnit ((mk (m ^ n)) r)
invSeries' : (n : { n // 0 < n }) → R ⧸ m ^ ↑n
invSeries_spec' : ∀ (n : { n // 0 < n }), invSeries' n * (mk (m ^ ↑n)) r = 1
invSeries : ℕ → R := fun n => if h : n = 0 then 0 else Classical.choose ⋯
invSeries_spec : ∀ {n : ℕ} (npos : 0 < n), (mk (m ^ n)) (invSeries n) = invSeries' ⟨n, npos⟩
a b : ℕ
le : a ≤ b
apos : 0 < a
⊢ (mk (m ^ a)) r * (mk (m ^ a)) (invSeries a) - (factor ⋯) ((mk (m ^ b)) r) * (factor ⋯) ((mk (m ^ b)) (invSeries b)) =
    0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
r : R
h : r ∉ m
mapu : ∀ {n : ℕ}, 0 < n → IsUnit ((mk (m ^ n)) r)
invSeries' : (n : { n // 0 < n }) → R ⧸ m ^ ↑n
invSeries_spec' : ∀ (n : { n // 0 < n }), invSeries' n * (mk (m ^ ↑n)) r = 1
invSeries : ℕ → R := fun n => if h : n = 0 then 0 else Classical.choose ⋯
n : ℕ
npos : 0 < n
⊢ (mk (m ^ n)) (invSeries n) = invSeries' ⟨n, npos⟩

Tactic:
simpa only [Nat.not_eq_zero_of_lt npos, invSeries]
using Classical.choose_spec (Ideal.Quotient.mk_surjective (invSeries' ⟨n, npos⟩))

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
r : R
h : r ∉ m
mapu : ∀ {n : ℕ}, 0 < n → IsUnit ((mk (m ^ n)) r)
invSeries' : (n : { n // 0 < n }) → R ⧸ m ^ ↑n
invSeries_spec' : ∀ (n : { n // 0 < n }), invSeries' n * (mk (m ^ ↑n)) r = 1
invSeries : ℕ → R := fun n => if h : n = 0 then 0 else Classical.choose ⋯
invSeries_spec : ∀ {n : ℕ} (npos : 0 < n), (mk (m ^ n)) (invSeries n) = invSeries' ⟨n, npos⟩
a b : ℕ
le : a ≤ b
apos : 0 < a
⊢ invSeries a ≡ invSeries b [SMOD m ^ a • ⊤]

Tactic:
simp only [smul_eq_mul, Ideal.mul_top]

Result:
case pos
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
r : R
h : r ∉ m
mapu : ∀ {n : ℕ}, 0 < n → IsUnit ((mk (m ^ n)) r)
invSeries' : (n : { n // 0 < n }) → R ⧸ m ^ ↑n
invSeries_spec' : ∀ (n : { n // 0 < n }), invSeries' n * (mk (m ^ ↑n)) r = 1
invSeries : ℕ → R := fun n => if h : n = 0 then 0 else Classical.choose ⋯
invSeries_spec : ∀ {n : ℕ} (npos : 0 < n), (mk (m ^ n)) (invSeries n) = invSeries' ⟨n, npos⟩
a b : ℕ
le : a ≤ b
apos : 0 < a
⊢ invSeries a ≡ invSeries b [SMOD m ^ a]

Proof state:
case pos
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
r : R
h : r ∉ m
mapu : ∀ {n : ℕ}, 0 < n → IsUnit ((mk (m ^ n)) r)
invSeries' : (n : { n // 0 < n }) → R ⧸ m ^ ↑n
invSeries_spec' : ∀ (n : { n // 0 < n }), invSeries' n * (mk (m ^ ↑n)) r = 1
invSeries : ℕ → R := fun n => if h : n = 0 then 0 else Classical.choose ⋯
invSeries_spec : ∀ {n : ℕ} (npos : 0 < n), (mk (m ^ n)) (invSeries n) = invSeries' ⟨n, npos⟩
a b : ℕ
le : a ≤ b
apos : 0 < a
⊢ (mk (m ^ a)) r * invSeries' ⟨a, apos⟩ - (factor ⋯) ((mk (m ^ b)) r) * (factor ⋯) (invSeries' ⟨b, ⋯⟩) = 0

Tactic:
rw [← _root_.map_mul, mul_comm, invSeries_spec', mul_comm, invSeries_spec',
  map_one, sub_self]

Result:
no goals

Proof state:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
r : R
h : r ∉ m
mapu : ∀ {n : ℕ}, 0 < n → IsUnit ((mk (m ^ n)) r)
invSeries' : (n : { n // 0 < n }) → R ⧸ m ^ ↑n
invSeries_spec' : ∀ (n : { n // 0 < n }), invSeries' n * (mk (m ^ ↑n)) r = 1
invSeries : ℕ → R := fun n => if h : n = 0 then 0 else Classical.choose ⋯
invSeries_spec : ∀ {n : ℕ} (npos : 0 < n), (mk (m ^ n)) (invSeries n) = invSeries' ⟨n, npos⟩
mod : ∀ {a b : ℕ}, a ≤ b → invSeries a ≡ invSeries b [SMOD m ^ a • ⊤]
⊢ IsUnit r

Tactic:
rcases IsAdicComplete.toIsPrecomplete.prec mod with ⟨inv, hinv⟩

Result:
case refine_2.intro
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
r : R
h : r ∉ m
mapu : ∀ {n : ℕ}, 0 < n → IsUnit ((mk (m ^ n)) r)
invSeries' : (n : { n // 0 < n }) → R ⧸ m ^ ↑n
invSeries_spec' : ∀ (n : { n // 0 < n }), invSeries' n * (mk (m ^ ↑n)) r = 1
invSeries : ℕ → R := fun n => if h : n = 0 then 0 else Classical.choose ⋯
invSeries_spec : ∀ {n : ℕ} (npos : 0 < n), (mk (m ^ n)) (invSeries n) = invSeries' ⟨n, npos⟩
mod : ∀ {a b : ℕ}, a ≤ b → invSeries a ≡ invSeries b [SMOD m ^ a • ⊤]
inv : R
hinv : ∀ (n : ℕ), invSeries n ≡ inv [SMOD m ^ n • ⊤]
⊢ IsUnit r