case a
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : CanonicallyOrderedAddMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
⊢ coeff d (↑(weightedHomogeneousComponent w 0) φ) = coeff d (↑C (coeff 0 φ))
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : CanonicallyOrderedAddMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
⊢ ↑(weightedHomogeneousComponent w 0) φ = ↑C (coeff 0 φ)
ext1 d
case a.inl
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : CanonicallyOrderedAddMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
⊢ coeff 0 (↑(weightedHomogeneousComponent w 0) φ) = coeff 0 (↑C (coeff 0 φ))

case a.inr
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : CanonicallyOrderedAddMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ coeff d (↑(weightedHomogeneousComponent w 0) φ) = coeff d (↑C (coeff 0 φ))
case a
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : CanonicallyOrderedAddMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
⊢ coeff d (↑(weightedHomogeneousComponent w 0) φ) = coeff d (↑C (coeff 0 φ))
rcases Classical.em (d = 0) with (rfl | hd)
no goals
case a.inl
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : CanonicallyOrderedAddMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
⊢ coeff 0 (↑(weightedHomogeneousComponent w 0) φ) = coeff 0 (↑C (coeff 0 φ))
simp only [coeff_weightedHomogeneousComponent, if_pos, map_zero, coeff_zero_C]
case a.inr.hnc
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : CanonicallyOrderedAddMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ¬↑(weightedDegree' w) d = 0
case a.inr
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : CanonicallyOrderedAddMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ coeff d (↑(weightedHomogeneousComponent w 0) φ) = coeff d (↑C (coeff 0 φ))
rw [coeff_weightedHomogeneousComponent, if_neg, coeff_C, if_neg (Ne.symm hd)]
case a.inr.hnc
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : CanonicallyOrderedAddMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ∃ x, ¬↑d x = 0 ∧ ¬w x = 0
case a.inr.hnc
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : CanonicallyOrderedAddMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ¬↑(weightedDegree' w) d = 0
simp only [weightedDegree', LinearMap.toAddMonoidHom_coe, Finsupp.total_apply, Finsupp.sum,
  sum_eq_zero_iff, Finsupp.mem_support_iff, Ne.def, smul_eq_zero, not_forall, not_or,
  and_self_left, exists_prop]
case a.inr.hnc
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : CanonicallyOrderedAddMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ∃ x, ¬↑d x = 0
⊢ ∃ x, ¬↑d x = 0 ∧ ¬w x = 0
case a.inr.hnc
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : CanonicallyOrderedAddMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ∃ x, ¬↑d x = 0 ∧ ¬w x = 0
simp only [FunLike.ext_iff, Finsupp.coe_zero, Pi.zero_apply, not_forall] at hd
case a.inr.hnc.intro
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : CanonicallyOrderedAddMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
i : σ
hi : ¬↑d i = 0
⊢ ∃ x, ¬↑d x = 0 ∧ ¬w x = 0
case a.inr.hnc
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : CanonicallyOrderedAddMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ∃ x, ¬↑d x = 0
⊢ ∃ x, ¬↑d x = 0 ∧ ¬w x = 0
obtain ⟨i, hi⟩ := hd
no goals
case a.inr.hnc.intro
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : CanonicallyOrderedAddMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
i : σ
hi : ¬↑d i = 0
⊢ ∃ x, ¬↑d x = 0 ∧ ¬w x = 0
exact ⟨i, hi, hw i⟩