-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_add_of_lt {f g : MvPolynomial σ R} (h : m.degree g ≺[m] m.degree f) :
    m.degree (f + g) = m.degree f

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

Tactic:
apply m.toSyn.injective

Result:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (f + g)) = m.toSyn (m.degree f)

Proof state:
case a.a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g) ≤ m.toSyn (m.degree f)

Tactic:
simp only [sup_le_iff, le_refl, true_and, le_of_lt h]

Result:
no goals

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

Tactic:
apply le_trans degree_add_le

Result:
case a.a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g) ≤ m.toSyn (m.degree f)

Proof state:
case a.a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : ¬m.toSyn (m.degree 0) ≤ m.toSyn (m.degree g)
hf : f = 0
⊢ m.toSyn (m.degree 0) ≤ m.toSyn (m.degree g)

Tactic:
simp only [degree_zero, map_zero]

Result:
case a.a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : ¬m.toSyn (m.degree 0) ≤ m.toSyn (m.degree g)
hf : f = 0
⊢ 0 ≤ m.toSyn (m.degree g)

Proof state:
case a.a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : ¬m.toSyn (m.degree 0) ≤ m.toSyn (m.degree g)
hf : f = 0
⊢ 0 ≤ m.toSyn (m.degree g)

Tactic:
apply bot_le

Result:
no goals

Proof state:
case a.a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : ¬m.toSyn (m.degree 0) ≤ m.toSyn (m.degree g)
hf : f = 0
⊢ False

Tactic:
apply h

Result:
case a.a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : ¬m.toSyn (m.degree 0) ≤ m.toSyn (m.degree g)
hf : f = 0
⊢ m.toSyn (m.degree 0) ≤ m.toSyn (m.degree g)

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

Tactic:
apply le_degree

Result:
case a.a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.degree f ∈ (f + g).support

Proof state:
case a.a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ f ≠ 0

Tactic:
intro hf

Result:
case a.a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
hf : f = 0
⊢ False

Proof state:
case a.a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
hf : f = 0
⊢ False

Tactic:
rw [← not_le, hf] at h

Result:
case a.a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : ¬m.toSyn (m.degree 0) ≤ m.toSyn (m.degree g)
hf : f = 0
⊢ False

Proof state:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (f + g)) = m.toSyn (m.degree f)

Tactic:
apply le_antisymm

Result:
case a.a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (f + g)) ≤ m.toSyn (m.degree f)

case a.a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree (f + g))

Proof state:
case a.a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.degree f ∈ (f + g).support

Tactic:
rw [mem_support_iff, coeff_add, m.coeff_eq_zero_of_lt h, add_zero,
  ← leadingCoeff, leadingCoeff_ne_zero_iff]

Result:
case a.a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ f ≠ 0