case intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : IsNilpotent y
n : ℕ
hn : x ^ n = 0
⊢ IsNilpotent (x + y)
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : IsNilpotent x
hy : IsNilpotent y
⊢ IsNilpotent (x + y)
obtain ⟨n, hn⟩ := hx
case intro.intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
⊢ IsNilpotent (x + y)
case intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : IsNilpotent y
n : ℕ
hn : x ^ n = 0
⊢ IsNilpotent (x + y)
obtain ⟨m, hm⟩ := hy
case intro.intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
⊢ (x + y) ^ (n + m - 1) = 0
case intro.intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
⊢ IsNilpotent (x + y)
use n + m - 1
case intro.intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
⊢ (Finset.sum (Finset.Nat.antidiagonal (n + m - 1)) fun m_1 =>
      Nat.choose (n + m - 1) m_1.fst • (x ^ m_1.fst * y ^ m_1.snd)) =
    0
case intro.intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
⊢ (x + y) ^ (n + m - 1) = 0
rw [h_comm.add_pow']
case intro.intro.h
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
⊢ ∀ (x_1 : ℕ × ℕ),
    x_1 ∈ Finset.Nat.antidiagonal (n + m - 1) → Nat.choose (n + m - 1) x_1.fst • (x ^ x_1.fst * y ^ x_1.snd) = 0
case intro.intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
⊢ (Finset.sum (Finset.Nat.antidiagonal (n + m - 1)) fun m_1 =>
      Nat.choose (n + m - 1) m_1.fst • (x ^ m_1.fst * y ^ m_1.snd)) =
    0
apply Finset.sum_eq_zero
case intro.intro.h.mk
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (n + m - 1)
⊢ Nat.choose (n + m - 1) (i, j).fst • (x ^ (i, j).fst * y ^ (i, j).snd) = 0
case intro.intro.h
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
⊢ ∀ (x_1 : ℕ × ℕ),
    x_1 ∈ Finset.Nat.antidiagonal (n + m - 1) → Nat.choose (n + m - 1) x_1.fst • (x ^ x_1.fst * y ^ x_1.snd) = 0
rintro ⟨i, j⟩ hij
case intro.intro.h.mk
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (n + m - 1)
⊢ x ^ i * y ^ j = 0
case intro.intro.h.mk
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (n + m - 1)
⊢ Nat.choose (n + m - 1) (i, j).fst • (x ^ (i, j).fst * y ^ (i, j).snd) = 0
suffices x ^ i * y ^ j = 0 by simp only [this, nsmul_eq_mul, MulZeroClass.mul_zero]
case intro.intro.h.mk.inl
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (n + m - 1)
hi : n ≤ (i, j).fst
⊢ x ^ i * y ^ j = 0

case intro.intro.h.mk.inr
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (n + m - 1)
hj : m ≤ (i, j).snd
⊢ x ^ i * y ^ j = 0
case intro.intro.h.mk
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (n + m - 1)
⊢ x ^ i * y ^ j = 0
cases' Nat.le_or_le_of_add_eq_add_pred (Finset.Nat.mem_antidiagonal.mp hij) with hi hj
no goals
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (n + m - 1)
this : x ^ i * y ^ j = 0
⊢ Nat.choose (n + m - 1) (i, j).fst • (x ^ (i, j).fst * y ^ (i, j).snd) = 0
simp only [this, nsmul_eq_mul, MulZeroClass.mul_zero]
no goals
case intro.intro.h.mk.inl
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (n + m - 1)
hi : n ≤ (i, j).fst
⊢ x ^ i * y ^ j = 0
rw [pow_eq_zero_of_le hi hn, MulZeroClass.zero_mul]
no goals
case intro.intro.h.mk.inr
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (n + m - 1)
hj : m ≤ (i, j).snd
⊢ x ^ i * y ^ j = 0
rw [pow_eq_zero_of_le hj hm, MulZeroClass.mul_zero]