-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_mul_le {f g : MvPolynomial σ R} :
    m.degree (f * g) ≼[m] m.degree f + m.degree g

Proof state:
case h.mk
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : (d, e) ∈ Finset.antidiagonal c
⊢ coeff (d, e).1 f * coeff (d, e).2 g = 0

Tactic:
simp only [Finset.mem_antidiagonal] at hde

Result:
case h.mk
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
⊢ coeff (d, e).1 f * coeff (d, e).2 g = 0

Proof state:
case h.mk
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
⊢ coeff d f * coeff e g = 0

Tactic:
by_cases hd : m.degree f ≺[m] d

Result:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : m.toSyn (m.degree f) < m.toSyn d
⊢ coeff d f * coeff e g = 0

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : ¬m.toSyn (m.degree f) < m.toSyn d
⊢ coeff d f * coeff e g = 0

Proof state:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : m.toSyn d ≤ m.toSyn (m.degree f)
⊢ m.toSyn (m.degree g) < m.toSyn e

Tactic:
apply lt_of_add_lt_add_left (a := m.toSyn d)

Result:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : m.toSyn d ≤ m.toSyn (m.degree f)
⊢ m.toSyn d + m.toSyn (m.degree g) < m.toSyn d + m.toSyn e

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
⊢ m.toSyn (m.degree f + m.degree g) < m.toSyn c → coeff c (f * g) = 0

Tactic:
intro hc

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
⊢ coeff c (f * g) = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ m.toSyn (m.degree (f * g)) ≤ m.toSyn (m.degree f + m.degree g)

Tactic:
rw [degree_le_iff]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ ∀ c ∈ (f * g).support, m.toSyn c ≤ m.toSyn (m.degree f + m.degree g)

Proof state:
case h.mk
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
⊢ coeff (d, e).1 f * coeff (d, e).2 g = 0

Tactic:
dsimp only

Result:
case h.mk
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
⊢ coeff d f * coeff e g = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : ¬m.toSyn (m.degree f) < m.toSyn d
this : m.toSyn (m.degree g) < m.toSyn e
⊢ coeff d f * coeff e g = 0

Tactic:
rw [m.coeff_eq_zero_of_lt this, mul_zero]

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : m.toSyn d ≤ m.toSyn (m.degree f)
⊢ m.toSyn d + m.toSyn (m.degree g) ≤ m.toSyn (m.degree f) + m.toSyn (m.degree g)

Tactic:
exact add_le_add_right hd _

Result:
no goals

Proof state:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : ¬m.toSyn (m.degree f) < m.toSyn d
⊢ coeff d f * coeff e g = 0

Tactic:
suffices m.degree g ≺[m] e by
  rw [m.coeff_eq_zero_of_lt this, mul_zero]

Result:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : ¬m.toSyn (m.degree f) < m.toSyn d
⊢ m.toSyn (m.degree g) < m.toSyn e

Proof state:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : m.toSyn d ≤ m.toSyn (m.degree f)
⊢ m.toSyn d + m.toSyn (m.degree g) < m.toSyn d + m.toSyn e

Tactic:
simp only [← map_add, hde]

Result:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : m.toSyn d ≤ m.toSyn (m.degree f)
⊢ m.toSyn (d + m.degree g) < m.toSyn c

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
⊢ c ∈ (f * g).support → m.toSyn c ≤ m.toSyn (m.degree f + m.degree g)

Tactic:
rw [← not_lt, mem_support_iff, not_imp_not]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
⊢ m.toSyn (m.degree f + m.degree g) < m.toSyn c → coeff c (f * g) = 0

Proof state:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : m.toSyn d ≤ m.toSyn (m.degree f)
⊢ m.toSyn (d + m.degree g) < m.toSyn c

Tactic:
apply lt_of_le_of_lt _ hc

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : m.toSyn d ≤ m.toSyn (m.degree f)
⊢ m.toSyn (d + m.degree g) ≤ m.toSyn (m.degree f + m.degree g)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
⊢ coeff c (f * g) = 0

Tactic:
rw [coeff_mul]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
⊢ ∑ x ∈ Finset.antidiagonal c, coeff x.1 f * coeff x.2 g = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
⊢ ∑ x ∈ Finset.antidiagonal c, coeff x.1 f * coeff x.2 g = 0

Tactic:
apply Finset.sum_eq_zero

Result:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
⊢ ∀ x ∈ Finset.antidiagonal c, coeff x.1 f * coeff x.2 g = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ ∀ c ∈ (f * g).support, m.toSyn c ≤ m.toSyn (m.degree f + m.degree g)

Tactic:
intro c

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
⊢ c ∈ (f * g).support → m.toSyn c ≤ m.toSyn (m.degree f + m.degree g)