-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_prod_le {ι : Type*} {P : ι → MvPolynomial σ R} {s : Finset ι} :
    m.degree (∏ i ∈ s, P i) ≼[m] ∑ i ∈ s, m.degree (P i)

Proof state:
case empty
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
⊢ m.toSyn (m.degree 1) ≤ m.toSyn 0

Tactic:
rw [← C_1, m.degree_C, map_zero]

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 : m.toSyn (m.degree (∏ i ∈ s, P i)) ≤ m.toSyn (∑ i ∈ s, m.degree (P i))
⊢ m.toSyn (m.degree (P a * ∏ x ∈ s, P x)) ≤ m.toSyn (m.degree (P a) + ∑ x ∈ s, m.degree (P x))

Tactic:
apply le_trans degree_mul_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 : m.toSyn (m.degree (∏ i ∈ s, P i)) ≤ m.toSyn (∑ i ∈ s, m.degree (P i))
⊢ m.toSyn (m.degree (P a) + m.degree (∏ x ∈ s, P x)) ≤ m.toSyn (m.degree (P a) + ∑ x ∈ s, m.degree (P x))

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 : m.toSyn (m.degree (∏ i ∈ s, P i)) ≤ m.toSyn (∑ i ∈ s, m.degree (P i))
⊢ m.toSyn (m.degree (∏ i ∈ insert a s, P i)) ≤ m.toSyn (∑ i ∈ insert a s, m.degree (P i))

Tactic:
rw [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 : m.toSyn (m.degree (∏ i ∈ s, P i)) ≤ m.toSyn (∑ i ∈ s, m.degree (P i))
⊢ m.toSyn (m.degree (P a * ∏ x ∈ s, P x)) ≤ m.toSyn (m.degree (P a) + ∑ x ∈ s, m.degree (P x))

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

Tactic:
induction s using Finset.induction_on with
| empty =>
  simp only [Finset.prod_empty, Finset.sum_empty]
  rw [← C_1, m.degree_C, map_zero]
| @insert a s has hrec =>
  rw [Finset.prod_insert has, Finset.sum_insert has]
  apply le_trans degree_mul_le
  simp only [map_add, add_le_add_iff_left, 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 : m.toSyn (m.degree (∏ i ∈ s, P i)) ≤ m.toSyn (∑ i ∈ s, m.degree (P i))
⊢ m.toSyn (m.degree (P a) + m.degree (∏ x ∈ s, P x)) ≤ m.toSyn (m.degree (P a) + ∑ x ∈ s, m.degree (P x))

Tactic:
simp only [map_add, add_le_add_iff_left, hrec]

Result:
no goals

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

Tactic:
simp only [Finset.prod_empty, Finset.sum_empty]

Result:
case empty
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
⊢ m.toSyn (m.degree 1) ≤ m.toSyn 0

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

Tactic:
classical
induction s using Finset.induction_on with
| empty =>
  simp only [Finset.prod_empty, Finset.sum_empty]
  rw [← C_1, m.degree_C, map_zero]
| @insert a s has hrec =>
  rw [Finset.prod_insert has, Finset.sum_insert has]
  apply le_trans degree_mul_le
  simp only [map_add, add_le_add_iff_left, hrec]

Result:
no goals