-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem weightedHomogeneousComponent_zero [CanonicallyOrderedAdd M] [NoZeroSMulDivisors ℕ M]
    (hw : ∀ i : σ, w i ≠ 0) :
    weightedHomogeneousComponent w 0 φ = C (coeff 0 φ)

Proof state:
case a.inl
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : OrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
⊢ coeff 0 ((weightedHomogeneousComponent w 0) φ) = coeff 0 (C (coeff 0 φ))

Tactic:
simp only [coeff_weightedHomogeneousComponent, if_pos, map_zero, coeff_zero_C]

Result:
no goals

Proof state:
case a
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : OrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
⊢ coeff d ((weightedHomogeneousComponent w 0) φ) = coeff d (C (coeff 0 φ))

Tactic:
rcases Classical.em (d = 0) with (rfl | hd)

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

case a.inr
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : OrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ coeff d ((weightedHomogeneousComponent w 0) φ) = coeff d (C (coeff 0 φ))

Proof state:
case a.inr.hnc
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : OrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ¬(weight w) d = 0

Tactic:
simp only [weight, LinearMap.toAddMonoidHom_coe, Finsupp.linearCombination_apply, Finsupp.sum,
  sum_eq_zero_iff, Finsupp.mem_support_iff, Ne, smul_eq_zero, not_forall, not_or,
  and_self_left, exists_prop]

Result:
case a.inr.hnc
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : OrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ∃ x, ¬d x = 0 ∧ ¬w x = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : OrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
⊢ (weightedHomogeneousComponent w 0) φ = C (coeff 0 φ)

Tactic:
ext1 d

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

Proof state:
case a.inr.hnc
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : OrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ∃ x, ¬d x = 0
⊢ ∃ x, ¬d x = 0 ∧ ¬w x = 0

Tactic:
obtain ⟨i, hi⟩ := hd

Result:
case a.inr.hnc.intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : OrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
i : σ
hi : ¬d i = 0
⊢ ∃ x, ¬d x = 0 ∧ ¬w x = 0

Proof state:
case a.inr.hnc
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : OrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ∃ x, ¬d x = 0 ∧ ¬w x = 0

Tactic:
simp only [DFunLike.ext_iff, Finsupp.coe_zero, Pi.zero_apply, not_forall] at hd

Result:
case a.inr.hnc
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : OrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ∃ x, ¬d x = 0
⊢ ∃ x, ¬d x = 0 ∧ ¬w x = 0

Proof state:
case a.inr.hnc.intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : OrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
i : σ
hi : ¬d i = 0
⊢ ∃ x, ¬d x = 0 ∧ ¬w x = 0

Tactic:
exact ⟨i, hi, hw i⟩

Result:
no goals

Proof state:
case a.inr
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : OrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ coeff d ((weightedHomogeneousComponent w 0) φ) = coeff d (C (coeff 0 φ))

Tactic:
rw [coeff_weightedHomogeneousComponent, if_neg, coeff_C, if_neg (Ne.symm hd)]

Result:
case a.inr.hnc
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : OrderedAddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
inst✝¹ : CanonicallyOrderedAdd M
inst✝ : NoZeroSMulDivisors ℕ M
hw : ∀ (i : σ), w i ≠ 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ ¬(weight w) d = 0