no goals
σ : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
u : Rˣ
⊢ ↑(coeff R n) (invOfUnit φ u) =
    if n = 0 then ↑u⁻¹
    else -↑u⁻¹ * ∑ x in antidiagonal n, if x.snd < n then ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (invOfUnit φ u) else 0
convert coeff_inv_aux n (↑u⁻¹) φ