-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_X_pow_mul (p : R⟦X⟧) (n d : ℕ) :
    coeff R (d + n) (X ^ n * p) = coeff R d p

Proof state:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).1)
h2 : (i, j) ≠ ((i, j).1, d)
⊢ False

Tactic:
apply h2

Result:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).1)
h2 : (i, j) ≠ ((i, j).1, d)
⊢ (i, j) = ((i, j).1, d)

Proof state:
case h₀.mk
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (n, d)
⊢ (coeff R (i, j).1) (X ^ n) * (coeff R (i, j).2) p = 0

Tactic:
rw [coeff_X_pow, if_neg, zero_mul]

Result:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (n, d)
⊢ ¬(i, j).1 = n

Proof state:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (n, d)
⊢ ¬(i, j).1 = n

Tactic:
rintro rfl

Result:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).1)
h2 : (i, j) ≠ ((i, j).1, d)
⊢ False

Proof state:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j).2 = d
h2 : (i, j) ≠ ((i, j).1, d)
⊢ (i, j) = ((i, j).1, d)

Tactic:
subst h1

Result:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
i j : ℕ
h2 : (i, j) ≠ ((i, j).1, (i, j).2)
⊢ (i, j) = ((i, j).1, (i, j).2)

Proof state:
case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (n, d) → (coeff R b.1) (X ^ n) * (coeff R b.2) p = 0

Tactic:
rintro ⟨i, j⟩ h1 h2

Result:
case h₀.mk
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (n, d)
⊢ (coeff R (i, j).1) (X ^ n) * (coeff R (i, j).2) p = 0

Proof state:
case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (n, d) ∉ antidiagonal (n + d) → (coeff R (n, d).1) (X ^ n) * (coeff R (n, d).2) p = 0

Tactic:
exact fun h1 => (h1 (mem_antidiagonal.2 rfl)).elim

Result:
no goals

Proof state:
case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (n, d) ∉ antidiagonal (d + n) → (coeff R (n, d).1) (X ^ n) * (coeff R (n, d).2) p = 0

Tactic:
rw [add_comm]

Result:
case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (n, d) ∉ antidiagonal (n + d) → (coeff R (n, d).1) (X ^ n) * (coeff R (n, d).2) p = 0

Proof state:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
i j : ℕ
h2 : (i, j) ≠ ((i, j).1, (i, j).2)
⊢ (i, j) = ((i, j).1, (i, j).2)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (coeff R (d + n)) (X ^ n * p) = (coeff R d) p

Tactic:
rw [coeff_mul, Finset.sum_eq_single (n, d), coeff_X_pow, if_pos rfl, one_mul]

Result:
case h₀
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (n, d) → (coeff R b.1) (X ^ n) * (coeff R b.2) p = 0

case h₁
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (n, d) ∉ antidiagonal (d + n) → (coeff R (n, d).1) (X ^ n) * (coeff R (n, d).2) p = 0

Proof state:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).1)
h2 : (i, j) ≠ ((i, j).1, d)
⊢ (i, j) = ((i, j).1, d)

Tactic:
rw [mem_antidiagonal, add_comm, add_right_cancel_iff] at h1

Result:
case h₀.mk.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
d i j : ℕ
h1 : (i, j).2 = d
h2 : (i, j) ≠ ((i, j).1, d)
⊢ (i, j) = ((i, j).1, d)