-- Mathlib/RingTheory/Nilpotent/Basic.lean
theorem add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero (h_comm : Commute x y) {m n k : ℕ}
    (hx : x ^ m = 0) (hy : y ^ n = 0) (h : m + n ≤ k + 1) :
    (x + y) ^ k = 0

Proof state:
case neg
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
hi : ¬m ≤ i
⊢ x ^ i * y ^ j = 0

Tactic:
rw [pow_eq_zero_of_le ?_ hy, mul_zero]

Result:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
hi : ¬m ≤ i
⊢ n ≤ j

Proof state:
case h.mk
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
⊢ k.choose (i, j).1 • (x ^ (i, j).1 * y ^ (i, j).2) = 0

Tactic:
suffices x ^ i * y ^ j = 0 by simp only [this, nsmul_eq_mul, mul_zero]

Result:
case h.mk
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
⊢ x ^ i * y ^ j = 0

Proof state:
case h.mk
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
⊢ x ^ i * y ^ j = 0

Tactic:
by_cases hi : m ≤ i

Result:
case pos
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
hi : m ≤ i
⊢ x ^ i * y ^ j = 0

case neg
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
hi : ¬m ≤ i
⊢ x ^ i * y ^ j = 0

Proof state:
case h
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
⊢ ∀ x_1 ∈ Finset.antidiagonal k, k.choose x_1.1 • (x ^ x_1.1 * y ^ x_1.2) = 0

Tactic:
rintro ⟨i, j⟩ hij

Result:
case h.mk
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
⊢ k.choose (i, j).1 • (x ^ (i, j).1 * y ^ (i, j).2) = 0

Proof state:
case pos
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
hi : m ≤ i
⊢ x ^ i * y ^ j = 0

Tactic:
rw [pow_eq_zero_of_le hi hx, zero_mul]

Result:
no goals

Proof state:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
⊢ (x + y) ^ k = 0

Tactic:
rw [h_comm.add_pow']

Result:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
⊢ ∑ m ∈ Finset.antidiagonal k, k.choose m.1 • (x ^ m.1 * y ^ m.2) = 0

Proof state:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
⊢ ∑ m ∈ Finset.antidiagonal k, k.choose m.1 • (x ^ m.1 * y ^ m.2) = 0

Tactic:
apply Finset.sum_eq_zero

Result:
case h
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
⊢ ∀ x_1 ∈ Finset.antidiagonal k, k.choose x_1.1 • (x ^ x_1.1 * y ^ x_1.2) = 0

Proof state:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
hi : ¬m ≤ i
⊢ n ≤ j

Tactic:
linarith [Finset.mem_antidiagonal.mp hij]

Result:
no goals

Proof state:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n k : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
h : m + n ≤ k + 1
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal k
this : x ^ i * y ^ j = 0
⊢ k.choose (i, j).1 • (x ^ (i, j).1 * y ^ (i, j).2) = 0

Tactic:
simp only [this, nsmul_eq_mul, mul_zero]

Result:
no goals