case intro
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
φ ψ : MvPolynomial σ R
m n : M
w : σ → M
hφ : φ ≠ 0
hm : IsWeightedHomogeneous w φ m
hn : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ m = n
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
φ ψ : MvPolynomial σ R
m n : M
w : σ → M
hφ : φ ≠ 0
hm : IsWeightedHomogeneous w φ m
hn : IsWeightedHomogeneous w φ n
⊢ m = n
obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero hφ
no goals
case intro
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
φ ψ : MvPolynomial σ R
m n : M
w : σ → M
hφ : φ ≠ 0
hm : IsWeightedHomogeneous w φ m
hn : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ m = n
rw [← hm hd, ← hn hd]