K : Type u
inst✝ : Field K
x : RatFunc K
hx : x ≠ 0
s : K[X]
hs : s ≠ 0
⊢ num x * s * denom x = num x * (s * denom x)
K : Type u
inst✝ : Field K
x : RatFunc K
hx : x ≠ 0
s : K[X]
hs : s ≠ 0
⊢ ↑(natDegree (num x * s)) - ↑(natDegree (s * denom x)) = intDegree x
apply natDegree_sub_eq_of_prod_eq (mul_ne_zero (num_ne_zero hx) hs)
  (mul_ne_zero hs x.denom_ne_zero) (num_ne_zero hx) x.denom_ne_zero
no goals
K : Type u
inst✝ : Field K
x : RatFunc K
hx : x ≠ 0
s : K[X]
hs : s ≠ 0
⊢ num x * s * denom x = num x * (s * denom x)
rw [mul_assoc]