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

Tactic:
simp only [smul_eq_mul, Ideal.mul_top, sub_zero, ← eq_zero_iff_mem]

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 * r - 1) = 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
mem : r ∈ m
⊢ False

Tactic:
rcases IsUnit.exists_left_inv h with ⟨s, hs⟩

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
⊢ False

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

Tactic:
have invSeries_spec {n : ℕ} (npos : 0 < n): (Ideal.Quotient.mk (m ^ n)) (invSeries n) =
  invSeries' ⟨n, npos⟩ := by
  simpa only [Nat.not_eq_zero_of_lt npos, invSeries]
  using Classical.choose_spec (Ideal.Quotient.mk_surjective (invSeries' ⟨n, npos⟩))

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 ⋯
invSeries_spec : ∀ {n : ℕ} (npos : 0 < n), (mk (m ^ n)) (invSeries n) = invSeries' ⟨n, npos⟩
⊢ IsUnit r

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
n : ℕ
ih : 0 < n → IsUnit ((mk (m ^ n)) r)
npos : 0 < n + 1
neq0 : n = 0
max' : (m ^ (n + 1)).IsMaximal :=
  Eq.mpr
    (id
      (congrArg IsMaximal
        (Eq.trans (congrArg (HPow.hPow m) (Eq.trans (congrArg (fun x => x + 1) neq0) (zero_add 1))) (pow_one m))))
    hmax
⊢ IsUnit ((mk (m ^ (n + 1))) r)

Tactic:
let hField : Field (R ⧸ m ^ (n + 1)) := Ideal.Quotient.field (m ^ (n + 1))

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
max' : (m ^ (n + 1)).IsMaximal :=
  Eq.mpr
    (id
      (congrArg IsMaximal
        (Eq.trans (congrArg (HPow.hPow m) (Eq.trans (congrArg (fun x => x + 1) neq0) (zero_add 1))) (pow_one m))))
    hmax
hField : Field (R ⧸ m ^ (n + 1)) := Quotient.field (m ^ (n + 1))
⊢ IsUnit ((mk (m ^ (n + 1))) r)

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

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

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
⊢ r ∉ m

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

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
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:
simp [Nat.eq_zero_of_not_pos npos]

Result:
no goals

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
⊢ 1 ∈ m

Tactic:
simp [← hs, Ideal.mul_mem_left m s mem]

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
n : ℕ
ih : 0 < n → IsUnit ((mk (m ^ n)) r)
npos : 0 < n + 1
neq0 : n = 0
max' : (m ^ (n + 1)).IsMaximal :=
  Eq.mpr
    (id
      (congrArg IsMaximal
        (Eq.trans (congrArg (HPow.hPow m) (Eq.trans (congrArg (fun x => x + 1) neq0) (zero_add 1))) (pow_one m))))
    hmax
hField : Field (R ⧸ m ^ (n + 1)) := Quotient.field (m ^ (n + 1))
⊢ IsUnit ((mk (m ^ (n + 1))) r)

Tactic:
simpa [isUnit_iff_ne_zero, ne_eq, Ideal.Quotient.eq_zero_iff_mem.not, neq0] using h

Result:
no goals

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
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 [Nat.eq_zero_of_not_pos apos]

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

Tactic:
let max' : (m ^ (n + 1)).IsMaximal := by simpa only [neq0, zero_add, pow_one] using hmax

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
max' : (m ^ (n + 1)).IsMaximal :=
  Eq.mpr
    (id
      (congrArg IsMaximal
        (Eq.trans (congrArg (HPow.hPow m) (Eq.trans (congrArg (fun x => x + 1) neq0) (zero_add 1))) (pow_one m))))
    hmax
⊢ IsUnit ((mk (m ^ (n + 1))) r)