-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem coeff_prod_sum_degree {ι : Type*} (P : ι → MvPolynomial σ R) (s : Finset ι) :
    coeff (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)

Proof state:
case empty
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
⊢ coeff (∑ i ∈ ∅, m.degree (P i)) (∏ i ∈ ∅, P i) = ∏ i ∈ ∅, m.leadingCoeff (P i)

Tactic:
simp

Result:
no goals

Proof state:
case insert
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hrec : coeff (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)
⊢ coeff (∑ i ∈ insert a s, m.degree (P i)) (∏ i ∈ insert a s, P i) = ∏ i ∈ insert a s, m.leadingCoeff (P i)

Tactic:
simp only [Finset.prod_insert has, Finset.sum_insert has]

Result:
case insert
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hrec : coeff (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)
⊢ coeff (m.degree (P a) + ∑ i ∈ s, m.degree (P i)) (P a * ∏ i ∈ s, P i) =
    m.leadingCoeff (P a) * ∏ i ∈ s, m.leadingCoeff (P i)

Proof state:
case insert
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hrec : coeff (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)
⊢ coeff (m.degree (P a)) (P a) * coeff (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) =
    m.leadingCoeff (P a) * ∏ i ∈ s, m.leadingCoeff (P i)

Tactic:
exact congr_arg₂ _ rfl hrec

Result:
no goals

Proof state:
case insert
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hrec : coeff (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)
⊢ coeff (m.degree (P a) + ∑ i ∈ s, m.degree (P i)) (P a * ∏ i ∈ s, P i) =
    m.leadingCoeff (P a) * ∏ i ∈ s, m.leadingCoeff (P i)

Tactic:
rw [coeff_mul_of_add_of_degree_le (le_of_eq rfl) degree_prod_le]

Result:
case insert
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hrec : coeff (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)
⊢ coeff (m.degree (P a)) (P a) * coeff (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) =
    m.leadingCoeff (P a) * ∏ i ∈ s, m.leadingCoeff (P i)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
⊢ coeff (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)

Tactic:
induction s using Finset.induction_on with
| empty => simp
| @insert a s has hrec =>
  simp only [Finset.prod_insert has, Finset.sum_insert has]
  rw [coeff_mul_of_add_of_degree_le (le_of_eq rfl) degree_prod_le]
  exact congr_arg₂ _ rfl hrec

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
⊢ coeff (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)

Tactic:
classical
induction s using Finset.induction_on with
| empty => simp
| @insert a s has hrec =>
  simp only [Finset.prod_insert has, Finset.sum_insert has]
  rw [coeff_mul_of_add_of_degree_le (le_of_eq rfl) degree_prod_le]
  exact congr_arg₂ _ rfl hrec

Result:
no goals