R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
⊢ ∑ i in Finite.toFinset (_ : Set.Finite (Function.support fun m => ↑(weightedHomogeneousComponent w m) φ)),
      ↑(weightedHomogeneousComponent w i) φ =
    φ
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
⊢ (∑ᶠ (m : M), ↑(weightedHomogeneousComponent w m) φ) = φ
rw [finsum_eq_sum _ (weightedHomogeneousComponent_finsupp φ)]
case a
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d
      (∑ i in Finite.toFinset (_ : Set.Finite (Function.support fun m => ↑(weightedHomogeneousComponent w m) φ)),
        ↑(weightedHomogeneousComponent w i) φ) =
    coeff d φ
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
⊢ ∑ i in Finite.toFinset (_ : Set.Finite (Function.support fun m => ↑(weightedHomogeneousComponent w m) φ)),
      ↑(weightedHomogeneousComponent w i) φ =
    φ
ext1 d
case a
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (∑ x in Finite.toFinset (_ : Set.Finite (Function.support fun m => ↑(weightedHomogeneousComponent w m) φ)),
      if ↑(weightedDegree' w) d = x then coeff d φ else 0) =
    coeff d φ
case a
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d
      (∑ i in Finite.toFinset (_ : Set.Finite (Function.support fun m => ↑(weightedHomogeneousComponent w m) φ)),
        ↑(weightedHomogeneousComponent w i) φ) =
    coeff d φ
simp only [coeff_sum, coeff_weightedHomogeneousComponent]
case a
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (if ↑(weightedDegree' w) d = ↑(weightedDegree' w) d then coeff d φ else 0) = coeff d φ

case a.h₀
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ ∀ (b : (fun x => M) d),
    b ∈ Finite.toFinset (_ : Set.Finite (Function.support fun m => ↑(weightedHomogeneousComponent w m) φ)) →
      b ≠ ↑(weightedDegree' w) d → (if ↑(weightedDegree' w) d = b then coeff d φ else 0) = 0

case a.h₁
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ ¬↑(weightedDegree' w) d ∈
        Finite.toFinset (_ : Set.Finite (Function.support fun m => ↑(weightedHomogeneousComponent w m) φ)) →
    (if ↑(weightedDegree' w) d = ↑(weightedDegree' w) d then coeff d φ else 0) = 0
case a
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (∑ x in Finite.toFinset (_ : Set.Finite (Function.support fun m => ↑(weightedHomogeneousComponent w m) φ)),
      if ↑(weightedDegree' w) d = x then coeff d φ else 0) =
    coeff d φ
rw [Finset.sum_eq_single (weightedDegree' w d)]
no goals
case a
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (if ↑(weightedDegree' w) d = ↑(weightedDegree' w) d then coeff d φ else 0) = coeff d φ
rw [if_pos rfl]
case a.h₀
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
m : M
a✝ : m ∈ Finite.toFinset (_ : Set.Finite (Function.support fun m => ↑(weightedHomogeneousComponent w m) φ))
hm' : m ≠ ↑(weightedDegree' w) d
⊢ (if ↑(weightedDegree' w) d = m then coeff d φ else 0) = 0
case a.h₀
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ ∀ (b : (fun x => M) d),
    b ∈ Finite.toFinset (_ : Set.Finite (Function.support fun m => ↑(weightedHomogeneousComponent w m) φ)) →
      b ≠ ↑(weightedDegree' w) d → (if ↑(weightedDegree' w) d = b then coeff d φ else 0) = 0
intro m _ hm'
no goals
case a.h₀
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
m : M
a✝ : m ∈ Finite.toFinset (_ : Set.Finite (Function.support fun m => ↑(weightedHomogeneousComponent w m) φ))
hm' : m ≠ ↑(weightedDegree' w) d
⊢ (if ↑(weightedDegree' w) d = m then coeff d φ else 0) = 0
rw [if_neg hm'.symm]
case a.h₁
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hm :
  ¬↑(weightedDegree' w) d ∈
      Finite.toFinset (_ : Set.Finite (Function.support fun m => ↑(weightedHomogeneousComponent w m) φ))
⊢ (if ↑(weightedDegree' w) d = ↑(weightedDegree' w) d then coeff d φ else 0) = 0
case a.h₁
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ ¬↑(weightedDegree' w) d ∈
        Finite.toFinset (_ : Set.Finite (Function.support fun m => ↑(weightedHomogeneousComponent w m) φ)) →
    (if ↑(weightedDegree' w) d = ↑(weightedDegree' w) d then coeff d φ else 0) = 0
intro hm
case a.h₁
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hm :
  ¬↑(weightedDegree' w) d ∈
      Finite.toFinset (_ : Set.Finite (Function.support fun m => ↑(weightedHomogeneousComponent w m) φ))
⊢ coeff d φ = 0
case a.h₁
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hm :
  ¬↑(weightedDegree' w) d ∈
      Finite.toFinset (_ : Set.Finite (Function.support fun m => ↑(weightedHomogeneousComponent w m) φ))
⊢ (if ↑(weightedDegree' w) d = ↑(weightedDegree' w) d then coeff d φ else 0) = 0
rw [if_pos rfl]
case a.h₁
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hm : ↑(weightedHomogeneousComponent w (↑(weightedDegree' w) d)) φ = 0
⊢ coeff d φ = 0
case a.h₁
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hm :
  ¬↑(weightedDegree' w) d ∈
      Finite.toFinset (_ : Set.Finite (Function.support fun m => ↑(weightedHomogeneousComponent w m) φ))
⊢ coeff d φ = 0
simp only [Finite.mem_toFinset, mem_support, Ne.def, Classical.not_not] at hm
case a.h₁
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hm : ↑(weightedHomogeneousComponent w (↑(weightedDegree' w) d)) φ = 0
this :
  coeff d (↑(weightedHomogeneousComponent w (↑(weightedDegree' w) d)) φ) =
    if ↑(weightedDegree' w) d = ↑(weightedDegree' w) d then coeff d φ else 0
⊢ coeff d φ = 0
case a.h₁
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hm : ↑(weightedHomogeneousComponent w (↑(weightedDegree' w) d)) φ = 0
⊢ coeff d φ = 0
have := coeff_weightedHomogeneousComponent (w := w) (weightedDegree' w d) φ d
case a.h₁
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hm : ↑(weightedHomogeneousComponent w (↑(weightedDegree' w) d)) φ = 0
this : 0 = coeff d φ
⊢ coeff d φ = 0
case a.h₁
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hm : ↑(weightedHomogeneousComponent w (↑(weightedDegree' w) d)) φ = 0
this :
  coeff d (↑(weightedHomogeneousComponent w (↑(weightedDegree' w) d)) φ) =
    if ↑(weightedDegree' w) d = ↑(weightedDegree' w) d then coeff d φ else 0
⊢ coeff d φ = 0
rw [hm, if_pos rfl, coeff_zero] at this
no goals
case a.h₁
R : Type u_1
M : Type u_3
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hm : ↑(weightedHomogeneousComponent w (↑(weightedDegree' w) d)) φ = 0
this : 0 = coeff d φ
⊢ coeff d φ = 0
exact this.symm