-- Mathlib/Algebra/Ring/Divisibility/Lemmas.lean
lemma pow_dvd_add_pow_of_pow_eq_zero_right (hp : n + m ≤ p + 1) (h_comm : Commute x y)
    (hy : y ^ n = 0) : x ^ m ∣ (x + y) ^ p

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

Tactic:
replace hij : i + j = p := by simpa using hij

Result:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x✝ : ℕ × ℕ
i j : ℕ
hij : i + j = p
⊢ x ^ m ∣ p.choose (i, j).1 • (x ^ (i, j).1 * y ^ (i, j).2)

Proof state:
case h.inr
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x✝ : ℕ × ℕ
i j : ℕ
hij : i + j = p
hi : i + 1 ≤ m
⊢ x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2

Tactic:
simp [pow_eq_zero_of_le (by omega : n ≤ j) hy]

Result:
no goals

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

Tactic:
rw [h_comm.add_pow']

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

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

Tactic:
refine Finset.dvd_sum fun ⟨i, j⟩ hij ↦ ?_

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

Proof state:
case h
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x✝ : ℕ × ℕ
i j : ℕ
hij : i + j = p
⊢ x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2

Tactic:
rcases le_or_lt m i with (hi : m ≤ i) | (hi : i + 1 ≤ m)

Result:
case h.inl
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x✝ : ℕ × ℕ
i j : ℕ
hij : i + j = p
hi : m ≤ i
⊢ x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2

case h.inr
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x✝ : ℕ × ℕ
i j : ℕ
hij : i + j = p
hi : i + 1 ≤ m
⊢ x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2

Proof state:
case h.inl
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x✝ : ℕ × ℕ
i j : ℕ
hij : i + j = p
hi : m ≤ i
⊢ x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2

Tactic:
exact dvd_mul_of_dvd_left (pow_dvd_pow x hi) _

Result:
no goals

Proof state:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x✝ : ℕ × ℕ
i j : ℕ
hij : i + j = p
⊢ x ^ m ∣ p.choose (i, j).1 • (x ^ (i, j).1 * y ^ (i, j).2)

Tactic:
apply dvd_nsmul_of_dvd

Result:
case h
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x✝ : ℕ × ℕ
i j : ℕ
hij : i + j = p
⊢ x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2

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

Tactic:
simpa using hij

Result:
no goals

Proof state:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Semiring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hy : y ^ n = 0
x✝ : ℕ × ℕ
i j : ℕ
hij : i + j = p
hi : i + 1 ≤ m
⊢ n ≤ j

Tactic:
omega

Result:
no goals