-- Mathlib/Algebra/Polynomial/Div.lean
theorem div_modByMonic_unique {f g} (q r : R[X]) (hg : Monic g)
    (h : r + g * q = f ∧ degree r < degree g) : f /ₘ g = q ∧ f %ₘ g = r

Proof state:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
h₅ : q - f /ₘ g = 0
⊢ f /ₘ g = q ∧ f %ₘ g = r

Tactic:
exact ⟨Eq.symm <| eq_of_sub_eq_zero h₅, Eq.symm <| eq_of_sub_eq_zero <| by simpa [h₅] using h₁⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.natDegree ≤ g.natDegree + (q - f /ₘ g).natDegree

Tactic:
exact Nat.le_add_right _ _

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
⊢ r - f %ₘ g - -g * (q - f /ₘ g) = 0

Tactic:
rw [← sub_eq_zero_of_eq (h.1.trans (modByMonic_add_div f hg).symm)]

Result:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
⊢ r - f %ₘ g - -g * (q - f /ₘ g) = r + g * q - (f %ₘ g + g * (f /ₘ g))

Proof state:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
⊢ f /ₘ g = q ∧ f %ₘ g = r

Tactic:
have h₄ : degree (r - f %ₘ g) < degree g :=
  calc
    degree (r - f %ₘ g) ≤ max (degree r) (degree (f %ₘ g)) := degree_sub_le _ _
    _ < degree g := max_lt_iff.2 ⟨h.2, degree_modByMonic_lt _ hg⟩

Result:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
⊢ f /ₘ g = q ∧ f %ₘ g = r

Proof state:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.degree ≤ g.degree + (q - f /ₘ g).degree

Tactic:
rw [degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hqf]

Result:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ ↑g.natDegree ≤ ↑g.natDegree + ↑(q - f /ₘ g).natDegree

Proof state:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.leadingCoeff * (q - f /ₘ g).leadingCoeff ≠ 0

Tactic:
simpa [Monic.def.1 hg]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
⊢ f /ₘ g = q ∧ f %ₘ g = r

Tactic:
have h₂ : degree (r - f %ₘ g) = degree (g * (q - f /ₘ g)) := by simp [h₁]

Result:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
⊢ f /ₘ g = q ∧ f %ₘ g = r

Proof state:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
⊢ f /ₘ g = q ∧ f %ₘ g = r

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
⊢ f /ₘ g = q ∧ f %ₘ g = r

Proof state:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ ↑g.natDegree ≤ ↑g.natDegree + ↑(q - f /ₘ g).natDegree

Tactic:
norm_cast

Result:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.natDegree ≤ g.natDegree + (q - f /ₘ g).natDegree

Proof state:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
⊢ r - f %ₘ g - -g * (q - f /ₘ g) = r + g * q - (f %ₘ g + g * (f /ₘ g))

Tactic:
simp [mul_add, mul_comm, sub_eq_add_neg, add_comm, add_left_comm, add_assoc]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
⊢ (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree

Tactic:
simp [h₁]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
h₅ : q - f /ₘ g = 0
⊢ r - f %ₘ g = 0

Tactic:
simpa [h₅] using h₁

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.degree + (q - f /ₘ g).degree = (r - f %ₘ g).degree

Tactic:
rw [h₂, degree_mul']

Result:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.leadingCoeff * (q - f /ₘ g).leadingCoeff ≠ 0

Proof state:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
⊢ f /ₘ g = q ∧ f %ₘ g = r

Tactic:
have h₁ : r - f %ₘ g = -g * (q - f /ₘ g) :=
  eq_of_sub_eq_zero
    (by
      rw [← sub_eq_zero_of_eq (h.1.trans (modByMonic_add_div f hg).symm)]
      simp [mul_add, mul_comm, sub_eq_add_neg, add_comm, add_left_comm, add_assoc])

Result:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
⊢ f /ₘ g = q ∧ f %ₘ g = r

Proof state:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
⊢ f /ₘ g = q ∧ f %ₘ g = r

Tactic:
have h₅ : q - f /ₘ g = 0 :=
  _root_.by_contradiction fun hqf =>
    not_le_of_gt h₄ <|
      calc
        degree g ≤ degree g + degree (q - f /ₘ g) := by
          rw [degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hqf]
          norm_cast
          exact Nat.le_add_right _ _
        _ = degree (r - f %ₘ g) := by rw [h₂, degree_mul']; simpa [Monic.def.1 hg]

Result:
R : Type u
inst✝ : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
a✝ : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
h₅ : q - f /ₘ g = 0
⊢ f /ₘ g = q ∧ f %ₘ g = r