-- Mathlib/RingTheory/MvPolynomial/Groebner.lean
theorem degree_sub_LTerm_lt {f : MvPolynomial σ R} (hf : m.degree f ≠ 0) :
    m.degree (m.subLTerm f) ≺[m] m.degree f

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
⊢ m.toSyn (m.degree (m.subLTerm f)) ≠ m.toSyn (m.degree f)

Tactic:
intro hf'

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.toSyn (m.degree (m.subLTerm f)) = m.toSyn (m.degree f)
⊢ False

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
h : m.subLTerm f = 0
hf' : 0 = m.degree f
⊢ False

Tactic:
exact hf hf'.symm

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
⊢ m.toSyn (m.degree (m.subLTerm f)) < m.toSyn (m.degree f)

Tactic:
rw [lt_iff_le_and_ne]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
⊢ m.toSyn (m.degree (m.subLTerm f)) ≤ m.toSyn (m.degree f) ∧ m.toSyn (m.degree (m.subLTerm f)) ≠ m.toSyn (m.degree f)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
this : coeff (m.degree f) (m.subLTerm f) ≠ 0
⊢ False

Tactic:
apply this

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
this : coeff (m.degree f) (m.subLTerm f) ≠ 0
⊢ coeff (m.degree f) (m.subLTerm f) = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
this : coeff (m.degree f) (m.subLTerm f) ≠ 0
⊢ coeff (m.degree f) (m.subLTerm f) = 0

Tactic:
simp [subLTerm, coeff_monomial, leadingCoeff]

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.toSyn (m.degree (m.subLTerm f)) = m.toSyn (m.degree f)
⊢ False

Tactic:
simp only [EmbeddingLike.apply_eq_iff_eq] at hf'

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
⊢ False

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
⊢ m.toSyn (m.degree (m.subLTerm f)) ≠ m.toSyn (m.degree f)

Tactic:
classical
intro hf'
simp only [EmbeddingLike.apply_eq_iff_eq] at hf'
have : m.subLTerm f ≠ 0 := by
  intro h
  simp only [h, degree_zero] at hf'
  exact hf hf'.symm
rw [← coeff_degree_ne_zero_iff (m := m), hf'] at this
apply this
simp [subLTerm, coeff_monomial, leadingCoeff]

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
⊢ m.toSyn (m.degree (m.subLTerm f)) ≤ m.toSyn (m.degree f) ∧ m.toSyn (m.degree (m.subLTerm f)) ≠ m.toSyn (m.degree f)

Tactic:
refine ⟨degree_sub_LTerm_le f, ?_⟩

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
⊢ m.toSyn (m.degree (m.subLTerm f)) ≠ m.toSyn (m.degree f)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
h : m.subLTerm f = 0
⊢ False

Tactic:
simp only [h, degree_zero] at hf'

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
h : m.subLTerm f = 0
hf' : 0 = m.degree f
⊢ False

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
⊢ False

Tactic:
have : m.subLTerm f ≠ 0 := by
  intro h
  simp only [h, degree_zero] at hf'
  exact hf hf'.symm

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
this : m.subLTerm f ≠ 0
⊢ False

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
this : m.subLTerm f ≠ 0
⊢ False

Tactic:
rw [← coeff_degree_ne_zero_iff (m := m), hf'] at this

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
this : coeff (m.degree f) (m.subLTerm f) ≠ 0
⊢ False

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
⊢ m.subLTerm f ≠ 0

Tactic:
intro h

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
h : m.subLTerm f = 0
⊢ False