-- Mathlib/RingTheory/MvPolynomial/Groebner.lean
theorem degree_reduce_lt {f b : MvPolynomial σ R} (hb : IsUnit (m.leadingCoeff b))
    (hbf : m.degree b ≤ m.degree f) (hf : m.degree f ≠ 0) :
    m.degree (m.reduce hb f) ≺[m] m.degree f

Proof state:
case right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
K : m.toSyn (m.degree (m.reduce hb f)) = m.toSyn (m.degree f)
⊢ False

Tactic:
simp only [EmbeddingLike.apply_eq_iff_eq] at K

Result:
case right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
K : m.degree (m.reduce hb f) = m.degree f
⊢ False

Proof state:
case right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
H' : m.reduce hb f = 0
K : m.degree (m.reduce hb f) = m.degree f
⊢ False

Tactic:
rw [H', degree_zero] at K

Result:
case right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
H' : m.reduce hb f = 0
K : 0 = m.degree f
⊢ False

Proof state:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
d : σ
⊢ (m.degree f) d = (m.degree f - m.degree b + m.degree b) d

Tactic:
rw [tsub_add_cancel_of_le hbf]

Result:
no goals

Proof state:
case right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
H' : coeff (m.degree (m.reduce hb f)) (m.reduce hb f) = 0
K : m.degree (m.reduce hb f) = m.degree f
⊢ False

Tactic:
rw [← leadingCoeff, leadingCoeff_eq_zero_iff] at H'

Result:
case right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
H' : m.reduce hb f = 0
K : m.degree (m.reduce hb f) = m.degree f
⊢ False

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
⊢ m.toSyn (m.degree (m.reduce hb f)) < m.toSyn (m.degree f)

Tactic:
have H' : coeff (m.degree f) (m.reduce hb f) = 0 := by
  simp only [reduce, coeff_sub, sub_eq_zero]
  nth_rewrite 2 [H]
  rw [coeff_mul_of_degree_add (m := m), leadingCoeff_monomial, mul_comm, ← mul_assoc,
    IsUnit.mul_val_inv, one_mul, ← leadingCoeff]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
⊢ m.toSyn (m.degree (m.reduce hb f)) < m.toSyn (m.degree f)

Proof state:
case right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
⊢ m.toSyn (m.degree (m.reduce hb f)) ≠ m.toSyn (m.degree f)

Tactic:
intro K

Result:
case right
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
K : m.toSyn (m.degree (m.reduce hb f)) = m.toSyn (m.degree f)
⊢ False

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
⊢ m.degree f = m.degree f - m.degree b + m.degree b

Tactic:
ext d

Result:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
d : σ
⊢ (m.degree f) d = (m.degree f - m.degree b + m.degree b) d

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
⊢ m.toSyn (m.degree (m.reduce hb 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 b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
⊢ m.toSyn (m.degree (m.reduce hb f)) ≤ m.toSyn (m.degree f) ∧ m.toSyn (m.degree (m.reduce hb f)) ≠ m.toSyn (m.degree f)

Proof state:
case hnc
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
hf0 : f = 0
⊢ m.degree f = 0

Tactic:
simp [hf0]

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
⊢ coeff (m.degree f) f =
    coeff (m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b)
      ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f) * b)

Tactic:
rw [coeff_mul_of_degree_add (m := m), leadingCoeff_monomial, mul_comm, ← mul_assoc,
  IsUnit.mul_val_inv, one_mul, ← leadingCoeff]

Result:
no goals