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

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⟩
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
this : inv - invSeries n ∈ m ^ n • ⊤
⊢ ((mk (m ^ n)) (inv - invSeries n) + (mk (m ^ n)) (invSeries n)) * (mk (m ^ n)) r - 1 = 0

Tactic:
simp only [smul_eq_mul, Ideal.mul_top] at this

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
this : inv - invSeries n ∈ m ^ n
⊢ ((mk (m ^ n)) (inv - invSeries n) + (mk (m ^ n)) (invSeries n)) * (mk (m ^ n)) r - 1 = 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
n : ℕ
ih : 0 < n → IsUnit ((mk (m ^ n)) r)
npos : 0 < n + 1
neq0 : n = 0
⊢ (m ^ (n + 1)).IsMaximal

Tactic:
simpa only [neq0, zero_add, pow_one] using hmax

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⟩
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
⊢ ((mk (m ^ n)) (inv - invSeries n) + (mk (m ^ n)) (invSeries n)) * (mk (m ^ n)) r - 1 = 0

Tactic:
have := SModEq.sub_mem.mp (hinv n).symm

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
this : inv - invSeries n ∈ m ^ n • ⊤
⊢ ((mk (m ^ n)) (inv - invSeries n) + (mk (m ^ n)) (invSeries n)) * (mk (m ^ n)) r - 1 = 0

Proof state:
case neg
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
r : R
h : r ∉ m
n : ℕ
ih : 0 < n → IsUnit ((mk (m ^ n)) r)
npos : 0 < n + 1
neq0 : ¬n = 0
⊢ IsUnit ((factorPow m ⋯) ((mk (m ^ (n + 1))) r))

Tactic:
simpa using (ih (Nat.zero_lt_of_ne_zero neq0))

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⟩
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
this : inv - invSeries n ∈ m ^ n
⊢ ((mk (m ^ n)) (inv - invSeries n) + (mk (m ^ n)) (invSeries n)) * (mk (m ^ n)) r - 1 = 0

Tactic:
simp [Ideal.Quotient.eq_zero_iff_mem.mpr this, invSeries_spec npos, invSeries_spec']

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)
⊢ IsUnit r

Tactic:
choose invSeries' invSeries_spec' using fun (n : {n : ℕ // 0 < n}) ↦
  (IsUnit.exists_left_inv (mapu n.2))

Result:
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
⊢ IsUnit r

Proof state:
case refine_1.intro
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
r : R
h : IsUnit r
mem : r ∈ m
s : R
hs : s * r = 1
⊢ False

Tactic:
absurd m.ne_top_iff_one.mp (Ideal.IsMaximal.ne_top hmax)

Result:
case refine_1.intro
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
r : R
h : IsUnit r
mem : r ∈ m
s : R
hs : s * r = 1
⊢ 1 ∈ m