no goals
σ : Type u_1
R : Type ?u.1886295
k✝ : Type u_2
inst✝ : Field k✝
φ₁ φ₂ φ₃ : MvPowerSeries σ k✝
h : ↑(constantCoeff σ k✝) φ₃ ≠ 0
k : φ₁ = φ₂ * φ₃⁻¹
⊢ φ₁ * φ₃ = φ₂
simp [k, mul_assoc, MvPowerSeries.inv_mul_cancel _ h]
no goals
σ : Type u_1
R : Type ?u.1886295
k✝ : Type u_2
inst✝ : Field k✝
φ₁ φ₂ φ₃ : MvPowerSeries σ k✝
h : ↑(constantCoeff σ k✝) φ₃ ≠ 0
k : φ₁ * φ₃ = φ₂
⊢ φ₁ = φ₂ * φ₃⁻¹
simp [← k, mul_assoc, MvPowerSeries.mul_inv_cancel _ h]