R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ ψ : MvPolynomial σ R
m n : M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : ↑(weightedDegree' w) d ≠ n
aux : ¬coeff d φ ≠ 0
⊢ coeff d φ = 0
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ ψ : MvPolynomial σ R
m n : M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : ↑(weightedDegree' w) d ≠ n
⊢ coeff d φ = 0
have aux := mt (@hφ d) hd
no goals
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
φ ψ : MvPolynomial σ R
m n : M
w : σ → M
hφ : IsWeightedHomogeneous w φ n
d : σ →₀ ℕ
hd : ↑(weightedDegree' w) d ≠ n
aux : ¬coeff d φ ≠ 0
⊢ coeff d φ = 0
rwa [Classical.not_not] at aux