case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ ψ x y : MvPolynomial σ R
h : Coe.coe x = Coe.coe y
m✝ : σ →₀ ℕ
⊢ coeff m✝ x = coeff m✝ y
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ ψ x y : MvPolynomial σ R
h : Coe.coe x = Coe.coe y
⊢ x = y
ext
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ ψ x y : MvPolynomial σ R
h : Coe.coe x = Coe.coe y
m✝ : σ →₀ ℕ
⊢ ↑(MvPowerSeries.coeff R m✝) ↑x = ↑(MvPowerSeries.coeff R m✝) ↑y
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ ψ x y : MvPolynomial σ R
h : Coe.coe x = Coe.coe y
m✝ : σ →₀ ℕ
⊢ coeff m✝ x = coeff m✝ y
simp_rw [← coeff_coe]
no goals
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
φ ψ x y : MvPolynomial σ R
h : Coe.coe x = Coe.coe y
m✝ : σ →₀ ℕ
⊢ ↑(MvPowerSeries.coeff R m✝) ↑x = ↑(MvPowerSeries.coeff R m✝) ↑y
congr