σ : Type u_1
τ : Type ?u.155224
R : Type u_2
S : Type ?u.155230
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
d : σ →₀ ℕ
hd : ∑ i in d.support, ↑d i ≠ n
aux : ¬coeff d φ ≠ 0
⊢ coeff d φ = 0
σ : Type u_1
τ : Type ?u.155224
R : Type u_2
S : Type ?u.155230
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
d : σ →₀ ℕ
hd : ∑ i in d.support, ↑d i ≠ n
⊢ coeff d φ = 0
have aux := mt (@hφ d) hd
no goals
σ : Type u_1
τ : Type ?u.155224
R : Type u_2
S : Type ?u.155230
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
d : σ →₀ ℕ
hd : ∑ i in d.support, ↑d i ≠ n
aux : ¬coeff d φ ≠ 0
⊢ coeff d φ = 0
classical
rwa [Classical.not_not] at aux
no goals
σ : Type u_1
τ : Type ?u.155224
R : Type u_2
S : Type ?u.155230
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
d : σ →₀ ℕ
hd : ∑ i in d.support, ↑d i ≠ n
aux : ¬coeff d φ ≠ 0
⊢ coeff d φ = 0
rwa [Classical.not_not] at aux