σ : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : DecidableEq σ
n : σ →₀ ℕ
a : R
φ : MvPowerSeries σ R
⊢ (if n = 0 then a
    else -a * ∑ x in antidiagonal n, if x_1 : x.snd < n then ↑(coeff R x.fst) φ * inv.aux a φ x.snd else 0) =
    if n = 0 then a
    else -a * ∑ x in antidiagonal n, if x.snd < n then ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (inv.aux a φ) else 0
σ : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : DecidableEq σ
n : σ →₀ ℕ
a : R
φ : MvPowerSeries σ R
⊢ inv.aux a φ n =
    if n = 0 then a
    else -a * ∑ x in antidiagonal n, if x.snd < n then ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (inv.aux a φ) else 0
rw [inv.aux]
no goals
σ : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : DecidableEq σ
n : σ →₀ ℕ
a : R
φ : MvPowerSeries σ R
⊢ (if n = 0 then a
    else -a * ∑ x in antidiagonal n, if x_1 : x.snd < n then ↑(coeff R x.fst) φ * inv.aux a φ x.snd else 0) =
    if n = 0 then a
    else -a * ∑ x in antidiagonal n, if x.snd < n then ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (inv.aux a φ) else 0
convert rfl