-- Mathlib/Algebra/Polynomial/Div.lean
theorem degree_add_divByMonic (hq : Monic q) (h : degree q ≤ degree p) :
    degree q + degree (p /ₘ q) = degree p

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
⊢ p /ₘ q ≠ 0

Tactic:
rwa [Ne, divByMonic_eq_zero_iff hq, not_lt]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
⊢ q.degree + (p /ₘ q).degree = p.degree

Tactic:
have hlc : leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0 := by
  rwa [Monic.def.1 hq, one_mul, Ne, leadingCoeff_eq_zero]

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ q.degree + (p /ₘ q).degree = p.degree

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
⊢ q.degree + (p /ₘ q).degree = p.degree

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
⊢ q.degree + (p /ₘ q).degree = p.degree

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ q.degree ≤ (q * (p /ₘ q)).degree

Tactic:
rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero, degree_eq_natDegree hdiv0, ←
    Nat.cast_add, Nat.cast_le]

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ q.natDegree ≤ q.natDegree + (p /ₘ q).natDegree

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ q.natDegree ≤ q.natDegree + (p /ₘ q).natDegree

Tactic:
exact Nat.le_add_right _ _

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
⊢ q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0

Tactic:
rwa [Monic.def.1 hq, one_mul, Ne, leadingCoeff_eq_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
hmod : (p %ₘ q).degree < (q * (p /ₘ q)).degree
⊢ q.degree + (p /ₘ q).degree = p.degree

Tactic:
calc
  degree q + degree (p /ₘ q) = degree (q * (p /ₘ q)) := Eq.symm (degree_mul' hlc)
  _ = degree (p %ₘ q + q * (p /ₘ q)) := (degree_add_eq_right_of_degree_lt hmod).symm
  _ = _ := congr_arg _ (modByMonic_add_div _ hq)

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ q.degree + (p /ₘ q).degree = p.degree

Tactic:
have hmod : degree (p %ₘ q) < degree (q * (p /ₘ q)) :=
  calc
    degree (p %ₘ q) < degree q := degree_modByMonic_lt _ hq
    _ ≤ _ := by
      rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero, degree_eq_natDegree hdiv0, ←
          Nat.cast_add, Nat.cast_le]
      exact Nat.le_add_right _ _

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
hmod : (p %ₘ q).degree < (q * (p /ₘ q)).degree
⊢ q.degree + (p /ₘ q).degree = p.degree

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
⊢ q.degree + (p /ₘ q).degree = p.degree

Tactic:
have hdiv0 : p /ₘ q ≠ 0 := by rwa [Ne, divByMonic_eq_zero_iff hq, not_lt]

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
a✝ : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
⊢ q.degree + (p /ₘ q).degree = p.degree