case h.e'_3
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
hq : Monic q
hdiv : p ∣ q
hdeg : natDegree q ≤ natDegree p
⊢ p = ↑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
hq : Monic q
hdiv : p ∣ q
hdeg : natDegree q ≤ natDegree p
⊢ q = p
convert eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le hp hdiv hdeg
no goals
case h.e'_3
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
hq : Monic q
hdiv : p ∣ q
hdeg : natDegree q ≤ natDegree p
⊢ p = ↑C (leadingCoeff q) * p
rw [hq.leadingCoeff, C_1, one_mul]