∀ {R : Type u_2} [inst : CommSemiring R] (k n : ℕ) (φ : PowerSeries R),
  (PowerSeries.coeff n) (φ ^ k) =
    ∑ l ∈ (Finset.range k).finsuppAntidiag n, ∏ i ∈ Finset.range k, (PowerSeries.coeff (l i)) φ