-- 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
⊢ inv * r - 1 ≡ 0 [SMOD m ^ n • ⊤]

Tactic:
apply SModEq.sub_mem.mpr

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 ∈ m ^ n • ⊤

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

Tactic:
exact sub_eq_zero.mp <| IsHausdorff.haus IsAdicComplete.toIsHausdorff (inv * r - 1) eq

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:
rw [SModEq.sub_mem, ← eq_zero_iff_mem, map_sub, ← (mapu apos).mul_right_inj,
  mul_zero, mul_sub]

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

Proof state:
case refine_1
R : Type u_1
inst✝¹ : CommRing R
m : Ideal R
hmax : m.IsMaximal
inst✝ : IsAdicComplete m R
r : R
h : IsUnit r
⊢ r ∉ m

Tactic:
by_contra mem

Result:
case refine_1
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
⊢ False

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 : ℕ
npos : 0 < n
⊢ IsUnit ((mk (m ^ n)) r)

Tactic:
induction' n with n ih

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
⊢ IsUnit ((mk (m ^ 0)) r)

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)

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
⊢ ¬0 < 0

Tactic:
exact Nat.not_lt_zero 0

Result:
no goals

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⟩
a b : ℕ
le : a ≤ b
⊢ invSeries a ≡ invSeries b [SMOD m ^ a • ⊤]

Tactic:
by_cases apos : 0 < a

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 • ⊤]

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⟩
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⟩
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 * r - 1) = 0

Tactic:
rw [map_sub, map_one, _root_.map_mul, ← sub_add_cancel inv (invSeries n), map_add]

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