case a
σ : Type u_1
τ : Type ?u.182889
R : Type u_2
S : Type ?u.182895
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d (↑(homogeneousComponent 0) φ) = coeff d (↑C (coeff 0 φ))
σ : Type u_1
τ : Type ?u.182889
R : Type u_2
S : Type ?u.182895
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
⊢ ↑(homogeneousComponent 0) φ = ↑C (coeff 0 φ)
ext1 d
case a.inl
σ : Type u_1
τ : Type ?u.182889
R : Type u_2
S : Type ?u.182895
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
⊢ coeff 0 (↑(homogeneousComponent 0) φ) = coeff 0 (↑C (coeff 0 φ))

case a.inr
σ : Type u_1
τ : Type ?u.182889
R : Type u_2
S : Type ?u.182895
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : ¬d = 0
⊢ coeff d (↑(homogeneousComponent 0) φ) = coeff d (↑C (coeff 0 φ))
case a
σ : Type u_1
τ : Type ?u.182889
R : Type u_2
S : Type ?u.182895
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d (↑(homogeneousComponent 0) φ) = coeff d (↑C (coeff 0 φ))
rcases em (d = 0) with (rfl | hd)
no goals
case a.inl
σ : Type u_1
τ : Type ?u.182889
R : Type u_2
S : Type ?u.182895
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
⊢ coeff 0 (↑(homogeneousComponent 0) φ) = coeff 0 (↑C (coeff 0 φ))
simp only [coeff_homogeneousComponent, sum_eq_zero_iff, Finsupp.zero_apply, if_true, coeff_C,
  eq_self_iff_true, forall_true_iff]
case a.inr.hnc
σ : Type u_1
τ : Type ?u.182889
R : Type u_2
S : Type ?u.182895
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ¬∑ i in d.support, ↑d i = 0
case a.inr
σ : Type u_1
τ : Type ?u.182889
R : Type u_2
S : Type ?u.182895
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : ¬d = 0
⊢ coeff d (↑(homogeneousComponent 0) φ) = coeff d (↑C (coeff 0 φ))
rw [coeff_homogeneousComponent, if_neg, coeff_C, if_neg (Ne.symm hd)]
case a.inr.hnc
σ : Type u_1
τ : Type ?u.182889
R : Type u_2
S : Type ?u.182895
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : ¬∀ (x : σ), ↑d x = 0
⊢ ¬∑ i in d.support, ↑d i = 0
case a.inr.hnc
σ : Type u_1
τ : Type ?u.182889
R : Type u_2
S : Type ?u.182895
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ¬∑ i in d.support, ↑d i = 0
simp only [FunLike.ext_iff, Finsupp.zero_apply] at hd
no goals
case a.inr.hnc
σ : Type u_1
τ : Type ?u.182889
R : Type u_2
S : Type ?u.182895
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : ¬∀ (x : σ), ↑d x = 0
⊢ ¬∑ i in d.support, ↑d i = 0
simp [hd]