case intro
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
hdeg : natDegree q ≤ natDegree p
r : R[X]
hr : q = p * r
⊢ q = ↑C (leadingCoeff q) * p
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
hdiv : p ∣ q
hdeg : natDegree q ≤ natDegree p
⊢ q = ↑C (leadingCoeff q) * p
obtain ⟨r, hr⟩ := hdiv
case intro.inl
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q : R✝[X]
R : Type u_1
inst✝ : CommRing R
p : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree 0 ≤ natDegree p
hr : 0 = p * r
⊢ 0 = ↑C (leadingCoeff 0) * p

case intro.inr
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
hdeg : natDegree q ≤ natDegree p
r : R[X]
hr : q = p * r
hq : q ≠ 0
⊢ q = ↑C (leadingCoeff q) * p
case intro
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
hdeg : natDegree q ≤ natDegree p
r : R[X]
hr : q = p * r
⊢ q = ↑C (leadingCoeff q) * p
obtain rfl | hq := eq_or_ne q 0
case intro.inr
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
hdeg : natDegree q ≤ natDegree p
r : R[X]
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ q = ↑C (leadingCoeff q) * p
case intro.inr
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
hdeg : natDegree q ≤ natDegree p
r : R[X]
hr : q = p * r
hq : q ≠ 0
⊢ q = ↑C (leadingCoeff q) * p
have rzero : r ≠ 0 := fun h => by simp [h, hq] at hr
case intro.inr
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree p + natDegree r ≤ natDegree p
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ q = ↑C (leadingCoeff q) * p

case intro.inr
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree (p * r) ≤ natDegree p
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ leadingCoeff p * leadingCoeff r ≠ 0
case intro.inr
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
hdeg : natDegree q ≤ natDegree p
r : R[X]
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ q = ↑C (leadingCoeff q) * p
rw [hr, natDegree_mul'] at hdeg
case intro.inr
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree (p * r) ≤ natDegree p
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ leadingCoeff p * leadingCoeff r ≠ 0

case intro.inr
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree p + natDegree r ≤ natDegree p
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ q = ↑C (leadingCoeff q) * p
case intro.inr
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree p + natDegree r ≤ natDegree p
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ q = ↑C (leadingCoeff q) * p

case intro.inr
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree (p * r) ≤ natDegree p
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ leadingCoeff p * leadingCoeff r ≠ 0
swap
case intro.inr
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree p + natDegree r ≤ natDegree p
hr : q = ↑C (coeff r 0) * p
hq : q ≠ 0
rzero : r ≠ 0
⊢ q = ↑C (leadingCoeff q) * p

case intro.inr
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree p + natDegree r ≤ natDegree p
hr : q = r * p
hq : q ≠ 0
rzero : r ≠ 0
⊢ natDegree r = 0
case intro.inr
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree p + natDegree r ≤ natDegree p
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ q = ↑C (leadingCoeff q) * p
rw [mul_comm, @eq_C_of_natDegree_eq_zero _ _ r] at hr
no goals
case intro.inl
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q : R✝[X]
R : Type u_1
inst✝ : CommRing R
p : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree 0 ≤ natDegree p
hr : 0 = p * r
⊢ 0 = ↑C (leadingCoeff 0) * p
simp
no goals
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
hdeg : natDegree q ≤ natDegree p
r : R[X]
hr : q = p * r
hq : q ≠ 0
h : r = 0
⊢ False
simp [h, hq] at hr
case intro.inr
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree (p * r) ≤ natDegree p
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ r ≠ 0
case intro.inr
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree (p * r) ≤ natDegree p
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ leadingCoeff p * leadingCoeff r ≠ 0
rw [hp.leadingCoeff, one_mul, leadingCoeff_ne_zero]
no goals
case intro.inr
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree (p * r) ≤ natDegree p
hr : q = p * r
hq : q ≠ 0
rzero : r ≠ 0
⊢ r ≠ 0
exact rzero
case h.e'_3.h.e'_5.h.e'_6
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree p + natDegree r ≤ natDegree p
hr : q = ↑C (coeff r 0) * p
hq : q ≠ 0
rzero : r ≠ 0
⊢ leadingCoeff q = coeff r 0
case intro.inr
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree p + natDegree r ≤ natDegree p
hr : q = ↑C (coeff r 0) * p
hq : q ≠ 0
rzero : r ≠ 0
⊢ q = ↑C (leadingCoeff q) * p
convert hr
case h.e'_2
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree p + natDegree r ≤ natDegree p
hr : q = ↑C (coeff r 0) * p
hq : q ≠ 0
rzero : r ≠ 0
⊢ leadingCoeff q = leadingCoeff (↑C (coeff r 0))
case h.e'_3.h.e'_5.h.e'_6
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree p + natDegree r ≤ natDegree p
hr : q = ↑C (coeff r 0) * p
hq : q ≠ 0
rzero : r ≠ 0
⊢ leadingCoeff q = coeff r 0
convert leadingCoeff_C (coeff r 0) using 1
no goals
case h.e'_2
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree p + natDegree r ≤ natDegree p
hr : q = ↑C (coeff r 0) * p
hq : q ≠ 0
rzero : r ≠ 0
⊢ leadingCoeff q = leadingCoeff (↑C (coeff r 0))
rw [hr, leadingCoeff_mul_monic hp]
no goals
case intro.inr
R✝ : Type u
S : Type v
T : Type w
a b : R✝
n : ℕ
inst✝² : CommRing R✝
inst✝¹ : IsDomain R✝
p✝ q✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : Monic p
r : R[X]
hdeg : natDegree p + natDegree r ≤ natDegree p
hr : q = r * p
hq : q ≠ 0
rzero : r ≠ 0
⊢ natDegree r = 0
exact (add_right_inj _).1 (le_antisymm hdeg <| Nat.le.intro rfl)