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

Proof state:
case succ
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
⊢ IsUnit ((mk (m ^ (n + 1))) r)

Tactic:
by_cases neq0 : n = 0

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
n : ℕ
ih : 0 < n → IsUnit ((mk (m ^ n)) r)
npos : 0 < n + 1
neq0 : n = 0
⊢ IsUnit ((mk (m ^ (n + 1))) r)

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 ((mk (m ^ (n + 1))) r)

Proof state:
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 • ⊤]
eq : ∀ (n : ℕ), inv * r - 1 ≡ 0 [SMOD m ^ n • ⊤]
⊢ IsUnit r

Tactic:
apply isUnit_iff_exists_inv'.mpr

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 • ⊤]
eq : ∀ (n : ℕ), inv * r - 1 ≡ 0 [SMOD m ^ n • ⊤]
⊢ ∃ b, b * r = 1

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) - (factor ⋯) ((mk (m ^ b)) r) * (factor ⋯) ((mk (m ^ b)) (invSeries b)) =
    0

Tactic:
simp only [invSeries_spec apos, invSeries_spec (Nat.lt_of_lt_of_le apos 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 * invSeries' ⟨a, apos⟩ - (factor ⋯) ((mk (m ^ b)) r) * (factor ⋯) (invSeries' ⟨b, ⋯⟩) = 0

Proof state:
case zero
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
r : R
h : r ∉ m
npos : 0 < 0
⊢ IsUnit ((mk (m ^ 0)) r)

Tactic:
absurd npos

Result:
case zero
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
r : R
h : r ∉ m
npos : 0 < 0
⊢ ¬0 < 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 ((mk (m ^ (n + 1))) r)

Tactic:
apply factorPowSucc.isUnit_of_isUnit_image (Nat.zero_lt_of_ne_zero neq0)

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

Proof state:
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 • ⊤]
eq : ∀ (n : ℕ), inv * r - 1 ≡ 0 [SMOD m ^ n • ⊤]
⊢ ∃ b, b * r = 1

Tactic:
use inv

Result:
case h
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 • ⊤]
eq : ∀ (n : ℕ), inv * r - 1 ≡ 0 [SMOD m ^ n • ⊤]
⊢ inv * r = 1

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

Tactic:
let invSeries : ℕ → R := fun n ↦ if h : n = 0 then 0 else Classical.choose <|
  Ideal.Quotient.mk_surjective <| invSeries' ⟨n, (Nat.zero_lt_of_ne_zero h)⟩

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
invSeries : ℕ → R := fun n => if h : n = 0 then 0 else Classical.choose ⋯
⊢ IsUnit r