Theorem: MvPolynomial.sum_homogeneousComponent (DividedPowers/ForMathlib/Homogeneous.lean)

State before:
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
⊢ ∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i) φ = φ
Tactic:
ext1 d
State after:
case a
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d (∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i) φ) = coeff d φ

State before:
case a
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d (∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i) φ) = coeff d φ
Tactic:
suffices φ.totalDegree < degree d → 0 = coeff d φ by
  simpa [coeff_sum, coeff_homogeneousComponent]
State after:
case a
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ φ.totalDegree < degree d → 0 = coeff d φ

State before:
case a
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ φ.totalDegree < degree d → 0 = coeff d φ
Tactic:
rw [degree_eq_weightedDegree]
State after:
case a
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ φ.totalDegree < ∑ i ∈ d.support, d i → 0 = coeff d φ

State before:
case a
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ φ.totalDegree < ∑ i ∈ d.support, d i → 0 = coeff d φ
Tactic:
intro h
State after:
case a
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
h : φ.totalDegree < ∑ i ∈ d.support, d i
⊢ 0 = coeff d φ

State before:
case a
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
h : φ.totalDegree < ∑ i ∈ d.support, d i
⊢ 0 = coeff d φ
Tactic:
exact (coeff_eq_zero_of_totalDegree_lt h).symm
State after:
no goals

State before:
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
this : φ.totalDegree < degree d → 0 = coeff d φ
⊢ coeff d (∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i) φ) = coeff d φ
Tactic:
simpa [coeff_sum, coeff_homogeneousComponent]
State after:
no goals