-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem sum_weightedHomogeneousComponent :
    (finsum fun m => weightedHomogeneousComponent w m φ) = φ

Proof state:
case a.h₀
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
m : M
a✝ : m ∈ ⋯.toFinset
hm' : m ≠ (weight w) d
⊢ (if (weight w) d = m then coeff d φ else 0) = 0

Tactic:
rw [if_neg hm'.symm]

Result:
no goals

Proof state:
case a.h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hm : (weight w) d ∉ ⋯.toFinset
⊢ (if (weight w) d = (weight w) d then coeff d φ else 0) = 0

Tactic:
rw [if_pos rfl]

Result:
case a.h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hm : (weight w) d ∉ ⋯.toFinset
⊢ coeff d φ = 0

Proof state:
case a.h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hm : (weightedHomogeneousComponent w ((weight w) d)) φ = 0
⊢ coeff d φ = 0

Tactic:
have := coeff_weightedHomogeneousComponent (w := w) (weight w d) φ d

Result:
case a.h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hm : (weightedHomogeneousComponent w ((weight w) d)) φ = 0
this :
  coeff d ((weightedHomogeneousComponent w ((weight w) d)) φ) = if (weight w) d = (weight w) d then coeff d φ else 0
⊢ coeff d φ = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
⊢ ∑ᶠ (m : M), (weightedHomogeneousComponent w m) φ = φ

Tactic:
rw [finsum_eq_sum _ (weightedHomogeneousComponent_finsupp φ)]

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
⊢ ∑ i ∈ ⋯.toFinset, (weightedHomogeneousComponent w i) φ = φ

Proof state:
case a
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d (∑ i ∈ ⋯.toFinset, (weightedHomogeneousComponent w i) φ) = coeff d φ

Tactic:
simp only [coeff_sum, coeff_weightedHomogeneousComponent]

Result:
case a
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (∑ x ∈ ⋯.toFinset, if (weight w) d = x then coeff d φ else 0) = coeff d φ

Proof state:
case a
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (if (weight w) d = (weight w) d then coeff d φ else 0) = coeff d φ

Tactic:
rw [if_pos rfl]

Result:
no goals

Proof state:
case a.h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hm : (weight w) d ∉ ⋯.toFinset
⊢ coeff d φ = 0

Tactic:
simp only [Finite.mem_toFinset, mem_support, Ne, Classical.not_not] at hm

Result:
case a.h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hm : (weightedHomogeneousComponent w ((weight w) d)) φ = 0
⊢ coeff d φ = 0

Proof state:
case a.h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (weight w) d ∉ ⋯.toFinset → (if (weight w) d = (weight w) d then coeff d φ else 0) = 0

Tactic:
intro hm

Result:
case a.h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hm : (weight w) d ∉ ⋯.toFinset
⊢ (if (weight w) d = (weight w) d then coeff d φ else 0) = 0

Proof state:
case a.h₀
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ ∀ b ∈ ⋯.toFinset, b ≠ (weight w) d → (if (weight w) d = b then coeff d φ else 0) = 0

Tactic:
intro m _ hm'

Result:
case a.h₀
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
m : M
a✝ : m ∈ ⋯.toFinset
hm' : m ≠ (weight w) d
⊢ (if (weight w) d = m then coeff d φ else 0) = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
⊢ ∑ i ∈ ⋯.toFinset, (weightedHomogeneousComponent w i) φ = φ

Tactic:
ext1 d

Result:
case a
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d (∑ i ∈ ⋯.toFinset, (weightedHomogeneousComponent w i) φ) = coeff d φ

Proof state:
case a
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (∑ x ∈ ⋯.toFinset, if (weight w) d = x then coeff d φ else 0) = coeff d φ

Tactic:
rw [Finset.sum_eq_single (weight w d)]

Result:
case a
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (if (weight w) d = (weight w) d then coeff d φ else 0) = coeff d φ

case a.h₀
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ ∀ b ∈ ⋯.toFinset, b ≠ (weight w) d → (if (weight w) d = b then coeff d φ else 0) = 0

case a.h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (weight w) d ∉ ⋯.toFinset → (if (weight w) d = (weight w) d then coeff d φ else 0) = 0

Proof state:
case a.h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hm : (weightedHomogeneousComponent w ((weight w) d)) φ = 0
this : 0 = coeff d φ
⊢ coeff d φ = 0

Tactic:
exact this.symm

Result:
no goals

Proof state:
case a.h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hm : (weightedHomogeneousComponent w ((weight w) d)) φ = 0
this :
  coeff d ((weightedHomogeneousComponent w ((weight w) d)) φ) = if (weight w) d = (weight w) d then coeff d φ else 0
⊢ coeff d φ = 0

Tactic:
rw [hm, if_pos rfl, coeff_zero] at this

Result:
case a.h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hm : (weightedHomogeneousComponent w ((weight w) d)) φ = 0
this : 0 = coeff d φ
⊢ coeff d φ = 0