no goals
R : Type ?u.3760552
k : Type u_1
inst✝ : Field k
n : ℕ
φ : PowerSeries k
⊢ ↑(coeff k n) φ⁻¹ =
    if n = 0 then (↑(constantCoeff k) φ)⁻¹
    else
      -(↑(constantCoeff k) φ)⁻¹ *
        ∑ x in Finset.Nat.antidiagonal n, if x.snd < n then ↑(coeff k x.fst) φ * ↑(coeff k x.snd) φ⁻¹ else 0
rw [inv_eq_inv_aux, coeff_inv_aux n (constantCoeff k φ)⁻¹ φ]