no goals
σ : Type u_1
R : Type ?u.1677822
k : Type u_2
inst✝ : Field k
φ : MvPowerSeries σ k
⊢ ↑(constantCoeff σ k) φ⁻¹ = (↑(constantCoeff σ k) φ)⁻¹
rw [← coeff_zero_eq_constantCoeff_apply, coeff_inv, if_pos rfl]