-- Mathlib/RingTheory/Idempotents.lean
theorem eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute {e₁ e₂ : R}
    (he₁ : IsIdempotentElem e₁) (he₂ : IsIdempotentElem e₂) (H : IsNilpotent (e₁ - e₂))
    (H' : Commute e₁ e₂) :
    e₁ = e₂

Proof state:
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : (e₁ - e₂) ^ 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
⊢ (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂

Tactic:
clear hn

Result:
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : (e₁ - e₂) ^ 3 = e₁ - e₂
n : ℕ
⊢ (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂

Proof state:
case intro
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : (e₁ - e₂) ^ 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
⊢ e₁ = e₂

Tactic:
have : (e₁ - e₂) ^ (2 * n + 1) = (e₁ - e₂) := by
  clear hn; induction n <;> simp [mul_add, add_assoc, pow_add _ (2 * _) 3, this, ← pow_succ, *]

Result:
case intro
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this✝ : (e₁ - e₂) ^ 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
this : (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂
⊢ e₁ = e₂

Proof state:
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : (e₁ - e₂) ^ 3 = e₁ - e₂
n : ℕ
⊢ (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂

Tactic:
induction n <;> simp [mul_add, add_assoc, pow_add _ (2 * _) 3, this, ← pow_succ, *]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
⊢ e₁ - e₂ * e₁ - (e₂ * e₁ - e₂ * e₁) - (e₂ * e₁ - e₂ * e₁ - (e₂ * e₁ - e₂)) = e₁ - e₂

Tactic:
abel

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
⊢ (e₁ - e₂) ^ 3 = e₁ - e₂

Tactic:
simp only [pow_succ, pow_zero, mul_sub, one_mul, sub_mul, he₁.eq, he₂.eq,
  H'.eq, mul_assoc]

Result:
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
⊢ e₁ - e₂ * e₁ - (e₂ * e₁ - e₂ * e₁) - (e₂ * e₁ - e₂ * (e₂ * e₁) - (e₂ * (e₂ * e₁) - e₂)) = e₁ - e₂

Proof state:
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
this : (e₁ - e₂) ^ 3 = e₁ - e₂
⊢ e₁ = e₂

Tactic:
obtain ⟨n, hn⟩ := H

Result:
case intro
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : (e₁ - e₂) ^ 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
⊢ e₁ = e₂

Proof state:
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
⊢ e₁ - e₂ * e₁ - (e₂ * e₁ - e₂ * e₁) - (e₂ * e₁ - e₂ * (e₂ * e₁) - (e₂ * (e₂ * e₁) - e₂)) = e₁ - e₂

Tactic:
simp only [← mul_assoc, he₁.eq, he₂.eq]

Result:
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
⊢ e₁ - e₂ * e₁ - (e₂ * e₁ - e₂ * e₁) - (e₂ * e₁ - e₂ * e₁ - (e₂ * e₁ - e₂)) = e₁ - e₂

Proof state:
case intro
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this✝ : (e₁ - e₂) ^ 3 = e₁ - e₂
n : ℕ
hn : (e₁ - e₂) ^ n = 0
this : (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂
⊢ e₁ = e₂

Tactic:
rwa [pow_succ, two_mul, pow_add, hn, zero_mul, zero_mul, eq_comm, sub_eq_zero] at this

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
⊢ e₁ = e₂

Tactic:
have : (e₁ - e₂) ^ 3 = (e₁ - e₂) := by
  simp only [pow_succ, pow_zero, mul_sub, one_mul, sub_mul, he₁.eq, he₂.eq,
    H'.eq, mul_assoc]
  simp only [← mul_assoc, he₁.eq, he₂.eq]
  abel

Result:
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
this : (e₁ - e₂) ^ 3 = e₁ - e₂
⊢ e₁ = e₂