-- Mathlib/RingTheory/DualNumber.lean
lemma isUnit_or_isNilpotent_of_isMaximal_isNilpotent [CommSemiring R] [AddCommGroup M]
    [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M]
    (h : ∀ I : Ideal R, I.IsMaximal → IsNilpotent I)
    (a : TrivSqZeroExt R M) :
    IsUnit a ∨ IsNilpotent a

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I
a : TrivSqZeroExt R M
ha : ¬IsUnit a.fst
I : Ideal R
hI : I.IsMaximal
haI : a.fst ∈ I
n : ℕ
hn : I ^ n = 0
⊢ a.fst ^ n = 0

Tactic:
exact hn.le (Ideal.pow_mem_pow haI _)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I
a : TrivSqZeroExt R M
⊢ IsUnit a.fst ∨ IsNilpotent a.fst

Tactic:
refine (em _).imp_right fun ha ↦ ?_

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I
a : TrivSqZeroExt R M
ha : ¬IsUnit a.fst
⊢ IsNilpotent a.fst

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I
a : TrivSqZeroExt R M
⊢ IsUnit a ∨ IsNilpotent a

Tactic:
rw [isUnit_iff_isUnit_fst, isNilpotent_iff_isNilpotent_fst]

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I
a : TrivSqZeroExt R M
⊢ IsUnit a.fst ∨ IsNilpotent a.fst

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I
a : TrivSqZeroExt R M
ha : ¬IsUnit a.fst
I : Ideal R
hI : I.IsMaximal
haI : a.fst ∈ I
⊢ IsNilpotent a.fst

Tactic:
refine (h _ hI).imp fun n hn ↦ ?_

Result:
case intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I
a : TrivSqZeroExt R M
ha : ¬IsUnit a.fst
I : Ideal R
hI : I.IsMaximal
haI : a.fst ∈ I
n : ℕ
hn : I ^ n = 0
⊢ a.fst ^ n = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I
a : TrivSqZeroExt R M
ha : ¬IsUnit a.fst
⊢ IsNilpotent a.fst

Tactic:
obtain ⟨I, hI, haI⟩ := exists_max_ideal_of_mem_nonunits (mem_nonunits_iff.mpr ha)

Result:
case intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
h : ∀ (I : Ideal R), I.IsMaximal → IsNilpotent I
a : TrivSqZeroExt R M
ha : ¬IsUnit a.fst
I : Ideal R
hI : I.IsMaximal
haI : a.fst ∈ I
⊢ IsNilpotent a.fst