-- Mathlib/RingTheory/Nilpotent/Basic.lean
lemma NoZeroSMulDivisors.isReduced (R M : Type*)
    [MonoidWithZero R] [Zero M] [MulActionWithZero R M] [Nontrivial M] [NoZeroSMulDivisors R M] :
    IsReduced R

Proof state:
case succ.intro.inr
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
x : R
x✝ : IsNilpotent x
k : ℕ
ih : x ^ k = 0 → x = 0
hk : x ^ (k + 1) = 0
m : M
hm : m ≠ 0
this : x • x ^ k • m = 0
hx : x ^ k • m = 0
⊢ x = 0

Tactic:
exact ih <| (eq_zero_or_eq_zero_of_smul_eq_zero hx).resolve_right hm

Result:
no goals

Proof state:
case zero
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
x : R
x✝ : IsNilpotent x
hk : x ^ 0 = 0
⊢ x = 0

Tactic:
rw [pow_zero] at hk

Result:
case zero
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
x : R
x✝ : IsNilpotent x
hk : 1 = 0
⊢ x = 0

Proof state:
case succ.intro
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
x : R
x✝ : IsNilpotent x
k : ℕ
ih : x ^ k = 0 → x = 0
hk : x ^ (k + 1) = 0
m : M
hm : m ≠ 0
this : x • x ^ k • m = 0
⊢ x = 0

Tactic:
rcases eq_zero_or_eq_zero_of_smul_eq_zero this with rfl | hx

Result:
case succ.intro.inl
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
k : ℕ
m : M
hm : m ≠ 0
x✝ : IsNilpotent 0
ih : 0 ^ k = 0 → 0 = 0
hk : 0 ^ (k + 1) = 0
this : 0 • 0 ^ k • m = 0
⊢ 0 = 0

case succ.intro.inr
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
x : R
x✝ : IsNilpotent x
k : ℕ
ih : x ^ k = 0 → x = 0
hk : x ^ (k + 1) = 0
m : M
hm : m ≠ 0
this : x • x ^ k • m = 0
hx : x ^ k • m = 0
⊢ x = 0

Proof state:
case succ
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
x : R
x✝ : IsNilpotent x
k : ℕ
ih : x ^ k = 0 → x = 0
hk : x ^ (k + 1) = 0
⊢ x = 0

Tactic:
obtain ⟨m : M, hm : m ≠ 0⟩ := exists_ne (0 : M)

Result:
case succ.intro
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
x : R
x✝ : IsNilpotent x
k : ℕ
ih : x ^ k = 0 → x = 0
hk : x ^ (k + 1) = 0
m : M
hm : m ≠ 0
⊢ x = 0

Proof state:
case zero
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
x : R
x✝ : IsNilpotent x
hk : 1 = 0
⊢ x = 0

Tactic:
exact eq_zero_of_zero_eq_one hk.symm x

Result:
no goals

Proof state:
case succ.intro.inl
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
k : ℕ
m : M
hm : m ≠ 0
x✝ : IsNilpotent 0
ih : 0 ^ k = 0 → 0 = 0
hk : 0 ^ (k + 1) = 0
this : 0 • 0 ^ k • m = 0
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
x : R
x✝ : IsNilpotent x
k : ℕ
ih : x ^ k = 0 → x = 0
hk : x ^ (k + 1) = 0
m : M
hm : m ≠ 0
⊢ x ^ (k + 1) • m = 0

Tactic:
simp only [hk, zero_smul]

Result:
no goals

Proof state:
case succ.intro
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
x : R
x✝ : IsNilpotent x
k : ℕ
ih : x ^ k = 0 → x = 0
hk : x ^ (k + 1) = 0
m : M
hm : m ≠ 0
⊢ x = 0

Tactic:
have : x ^ (k + 1) • m = 0 := by simp only [hk, zero_smul]

Result:
case succ.intro
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
x : R
x✝ : IsNilpotent x
k : ℕ
ih : x ^ k = 0 → x = 0
hk : x ^ (k + 1) = 0
m : M
hm : m ≠ 0
this : x ^ (k + 1) • m = 0
⊢ x = 0

Proof state:
case succ.intro
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
x : R
x✝ : IsNilpotent x
k : ℕ
ih : x ^ k = 0 → x = 0
hk : x ^ (k + 1) = 0
m : M
hm : m ≠ 0
this : x ^ (k + 1) • m = 0
⊢ x = 0

Tactic:
rw [pow_succ', mul_smul] at this

Result:
case succ.intro
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
x : R
x✝ : IsNilpotent x
k : ℕ
ih : x ^ k = 0 → x = 0
hk : x ^ (k + 1) = 0
m : M
hm : m ≠ 0
this : x • x ^ k • m = 0
⊢ x = 0

Proof state:
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
⊢ IsReduced R

Tactic:
refine ⟨fun x ⟨k, hk⟩ ↦ ?_⟩

Result:
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
x : R
x✝ : IsNilpotent x
k : ℕ
hk : x ^ k = 0
⊢ x = 0

Proof state:
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
x : R
x✝ : IsNilpotent x
k : ℕ
hk : x ^ k = 0
⊢ x = 0

Tactic:
induction' k with k ih

Result:
case zero
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
x : R
x✝ : IsNilpotent x
hk : x ^ 0 = 0
⊢ x = 0

case succ
R : Type u_3
M : Type u_4
inst✝⁴ : MonoidWithZero R
inst✝³ : Zero M
inst✝² : MulActionWithZero R M
inst✝¹ : Nontrivial M
inst✝ : NoZeroSMulDivisors R M
x : R
x✝ : IsNilpotent x
k : ℕ
ih : x ^ k = 0 → x = 0
hk : x ^ (k + 1) = 0
⊢ x = 0