-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem mk_one_pow_eq_mk_choose_add :
    (mk 1 : S⟦X⟧) ^ (d + 1) = (mk fun n => Nat.choose (d + n) d : S⟦X⟧)

Proof state:
case succ.h
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
hd : mk 1 ^ (d + 1) = mk fun n => ↑((d + n).choose d)
n : ℕ
⊢ ↑(∑ x ∈ Finset.antidiagonal n, (d + x.2).choose d) = ↑((d + 1 + n).choose (d + 1))

Tactic:
rw [Finset.sum_antidiagonal_choose_add, add_right_comm]

Result:
no goals

Proof state:
case succ.h
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
hd : mk 1 ^ (d + 1) = mk fun n => ↑((d + n).choose d)
n : ℕ
⊢ (coeff S n) (mk 1 ^ (d + 1 + 1)) = (coeff S n) (mk fun n => ↑((d + 1 + n).choose (d + 1)))

Tactic:
rw [pow_add, hd, pow_one, mul_comm, coeff_mul]

Result:
case succ.h
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
hd : mk 1 ^ (d + 1) = mk fun n => ↑((d + n).choose d)
n : ℕ
⊢ ∑ p ∈ Finset.antidiagonal n, (coeff S p.1) (mk 1) * (coeff S p.2) (mk fun n => ↑((d + n).choose d)) =
    (coeff S n) (mk fun n => ↑((d + 1 + n).choose (d + 1)))

Proof state:
case succ.h
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
hd : mk 1 ^ (d + 1) = mk fun n => ↑((d + n).choose d)
n : ℕ
⊢ ∑ x ∈ Finset.antidiagonal n, ↑((d + x.2).choose d) = ↑((d + 1 + n).choose (d + 1))

Tactic:
norm_cast

Result:
case succ.h
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
hd : mk 1 ^ (d + 1) = mk fun n => ↑((d + n).choose d)
n : ℕ
⊢ ↑(∑ x ∈ Finset.antidiagonal n, (d + x.2).choose d) = ↑((d + 1 + n).choose (d + 1))

Proof state:
case zero.h
S : Type u_1
inst✝ : CommRing S
d n✝ : ℕ
⊢ (coeff S n✝) (mk 1 ^ (0 + 1)) = (coeff S n✝) (mk fun n => ↑((0 + n).choose 0))

Tactic:
simp

Result:
no goals

Proof state:
case succ
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
hd : mk 1 ^ (d + 1) = mk fun n => ↑((d + n).choose d)
⊢ mk 1 ^ (d + 1 + 1) = mk fun n => ↑((d + 1 + n).choose (d + 1))

Tactic:
ext n

Result:
case succ.h
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
hd : mk 1 ^ (d + 1) = mk fun n => ↑((d + n).choose d)
n : ℕ
⊢ (coeff S n) (mk 1 ^ (d + 1 + 1)) = (coeff S n) (mk fun n => ↑((d + 1 + n).choose (d + 1)))

Proof state:
S : Type u_1
inst✝ : CommRing S
d : ℕ
⊢ mk 1 ^ (d + 1) = mk fun n => ↑((d + n).choose d)

Tactic:
induction d with
| zero => ext; simp
| succ d hd =>
    ext n
    rw [pow_add, hd, pow_one, mul_comm, coeff_mul]
    simp_rw [coeff_mk, Pi.one_apply, one_mul]
    norm_cast
    rw [Finset.sum_antidiagonal_choose_add, add_right_comm]

Result:
no goals

Proof state:
case zero
S : Type u_1
inst✝ : CommRing S
d : ℕ
⊢ mk 1 ^ (0 + 1) = mk fun n => ↑((0 + n).choose 0)

Tactic:
ext

Result:
case zero.h
S : Type u_1
inst✝ : CommRing S
d n✝ : ℕ
⊢ (coeff S n✝) (mk 1 ^ (0 + 1)) = (coeff S n✝) (mk fun n => ↑((0 + n).choose 0))

Proof state:
case succ.h
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
hd : mk 1 ^ (d + 1) = mk fun n => ↑((d + n).choose d)
n : ℕ
⊢ ∑ p ∈ Finset.antidiagonal n, (coeff S p.1) (mk 1) * (coeff S p.2) (mk fun n => ↑((d + n).choose d)) =
    (coeff S n) (mk fun n => ↑((d + 1 + n).choose (d + 1)))

Tactic:
simp_rw [coeff_mk, Pi.one_apply, one_mul]

Result:
case succ.h
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
hd : mk 1 ^ (d + 1) = mk fun n => ↑((d + n).choose d)
n : ℕ
⊢ ∑ x ∈ Finset.antidiagonal n, ↑((d + x.2).choose d) = ↑((d + 1 + n).choose (d + 1))