-- Mathlib/Algebra/Polynomial/Div.lean
lemma eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le {R} [CommRing R] {p q : R[X]}
    (hp : p.Monic) (hdiv : p ∣ q) (hdeg : q.natDegree ≤ p.natDegree) :
    q = C q.leadingCoeff * p

Proof state:
case intro.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hdeg : q.natDegree ≤ p.natDegree
r : R[X]
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ q = C q.leadingCoeff * p

Tactic:
rw [hr, natDegree_mul'] at hdeg

Result:
case intro.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
r : R[X]
hdeg : p.natDegree + r.natDegree ≤ p.natDegree
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ q = C q.leadingCoeff * p

case intro.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ p.leadingCoeff * r.leadingCoeff ≠ 0

Proof state:
case intro.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hdeg : q.natDegree ≤ p.natDegree
r : R[X]
hr : q = p * r
hq : q ≠ 0
⊢ q = C q.leadingCoeff * p

Tactic:
have rzero : r ≠ 0 := fun h => by simp [h, hq] at hr

Result:
case intro.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hdeg : q.natDegree ≤ p.natDegree
r : R[X]
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ q = C q.leadingCoeff * p

Proof state:
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hdeg : q.natDegree ≤ p.natDegree
r : R[X]
hr : q = p * r
hq : q ≠ 0
h : r = 0
⊢ False

Tactic:
simp [h, hq] at hr

Result:
no goals

Proof state:
case intro.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
r : R[X]
hdeg : p.natDegree + r.natDegree ≤ p.natDegree
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ q = C q.leadingCoeff * p

case intro.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ p.leadingCoeff * r.leadingCoeff ≠ 0

Tactic:
swap

Result:
case intro.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ p.leadingCoeff * r.leadingCoeff ≠ 0

case intro.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
r : R[X]
hdeg : p.natDegree + r.natDegree ≤ p.natDegree
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ q = C q.leadingCoeff * p

Proof state:
case intro.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
r : R[X]
hdeg : p.natDegree + r.natDegree ≤ p.natDegree
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ q = C q.leadingCoeff * p

Tactic:
rw [mul_comm, @eq_C_of_natDegree_eq_zero _ _ r] at hr

Result:
case intro.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
r : R[X]
hdeg : p.natDegree + r.natDegree ≤ p.natDegree
hr : q = C (r.coeff 0) * p
hq : q ≠ 0
rzero : r ≠ 0
⊢ q = C q.leadingCoeff * p

case intro.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
r : R[X]
hdeg : p.natDegree + r.natDegree ≤ p.natDegree
hr : q = r * p
hq : q ≠ 0
rzero : r ≠ 0
⊢ r.natDegree = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hdiv : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ q = C q.leadingCoeff * p

Tactic:
obtain ⟨r, hr⟩ := hdiv

Result:
case intro
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hdeg : q.natDegree ≤ p.natDegree
r : R[X]
hr : q = p * r
⊢ q = C q.leadingCoeff * p

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hdeg : q.natDegree ≤ p.natDegree
r : R[X]
hr : q = p * r
⊢ q = C q.leadingCoeff * p

Tactic:
obtain rfl | hq := eq_or_ne q 0

Result:
case intro.inl
R : Type u_1
inst✝ : CommRing R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : natDegree 0 ≤ p.natDegree
hr : 0 = p * r
⊢ 0 = C (leadingCoeff 0) * p

case intro.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hdeg : q.natDegree ≤ p.natDegree
r : R[X]
hr : q = p * r
hq : q ≠ 0
⊢ q = C q.leadingCoeff * p

Proof state:
case intro.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
r : R[X]
hdeg : p.natDegree + r.natDegree ≤ p.natDegree
hr : q = C (r.coeff 0) * p
hq : q ≠ 0
rzero : r ≠ 0
⊢ q = C q.leadingCoeff * p

Tactic:
convert hr

Result:
case h.e'_3.h.e'_5.h.e'_6
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
r : R[X]
hdeg : p.natDegree + r.natDegree ≤ p.natDegree
hr : q = C (r.coeff 0) * p
hq : q ≠ 0
rzero : r ≠ 0
⊢ q.leadingCoeff = r.coeff 0

Proof state:
case intro.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ p.leadingCoeff * r.leadingCoeff ≠ 0

Tactic:
rw [hp.leadingCoeff, one_mul, leadingCoeff_ne_zero]

Result:
case intro.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ r ≠ 0

Proof state:
case intro.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ r ≠ 0

Tactic:
exact rzero

Result:
no goals

Proof state:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
r : R[X]
hdeg : p.natDegree + r.natDegree ≤ p.natDegree
hr : q = C (r.coeff 0) * p
hq : q ≠ 0
rzero : r ≠ 0
⊢ q.leadingCoeff = (C (r.coeff 0)).leadingCoeff

Tactic:
rw [hr, leadingCoeff_mul_monic hp]

Result:
no goals

Proof state:
case intro.inl
R : Type u_1
inst✝ : CommRing R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : natDegree 0 ≤ p.natDegree
hr : 0 = p * r
⊢ 0 = C (leadingCoeff 0) * p

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3.h.e'_5.h.e'_6
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
r : R[X]
hdeg : p.natDegree + r.natDegree ≤ p.natDegree
hr : q = C (r.coeff 0) * p
hq : q ≠ 0
rzero : r ≠ 0
⊢ q.leadingCoeff = r.coeff 0

Tactic:
convert leadingCoeff_C (coeff r 0) using 1

Result:
case h.e'_2
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
r : R[X]
hdeg : p.natDegree + r.natDegree ≤ p.natDegree
hr : q = C (r.coeff 0) * p
hq : q ≠ 0
rzero : r ≠ 0
⊢ q.leadingCoeff = (C (r.coeff 0)).leadingCoeff

Proof state:
case intro.inr
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
r : R[X]
hdeg : p.natDegree + r.natDegree ≤ p.natDegree
hr : q = r * p
hq : q ≠ 0
rzero : r ≠ 0
⊢ r.natDegree = 0

Tactic:
exact (add_right_inj _).1 (le_antisymm hdeg <| Nat.le.intro rfl)

Result:
no goals