K : Type u
inst✝ : Field K
x y : RatFunc K
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(natDegree (num (x * y))) + (↑(natDegree (denom x)) + ↑(natDegree (denom y))) =
    ↑(natDegree (num x)) + ↑(natDegree (num y)) + ↑(natDegree (denom (x * y)))
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : x ≠ 0
hy : y ≠ 0
⊢ intDegree (x * y) = intDegree x + intDegree y
simp only [intDegree, add_sub, sub_add, sub_sub_eq_add_sub, sub_sub, sub_eq_sub_iff_add_eq_add]
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : x ≠ 0
hy : y ≠ 0
⊢ natDegree (num (x * y)) + (natDegree (denom x) + natDegree (denom y)) =
    natDegree (num x) + natDegree (num y) + natDegree (denom (x * y))
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(natDegree (num (x * y))) + (↑(natDegree (denom x)) + ↑(natDegree (denom y))) =
    ↑(natDegree (num x)) + ↑(natDegree (num y)) + ↑(natDegree (denom (x * y)))
norm_cast
no goals
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : x ≠ 0
hy : y ≠ 0
⊢ natDegree (num (x * y)) + (natDegree (denom x) + natDegree (denom y)) =
    natDegree (num x) + natDegree (num y) + natDegree (denom (x * y))
rw [← Polynomial.natDegree_mul x.denom_ne_zero y.denom_ne_zero, ←
  Polynomial.natDegree_mul (RatFunc.num_ne_zero (mul_ne_zero hx hy))
    (mul_ne_zero x.denom_ne_zero y.denom_ne_zero),
  ← Polynomial.natDegree_mul (RatFunc.num_ne_zero hx) (RatFunc.num_ne_zero hy), ←
  Polynomial.natDegree_mul (mul_ne_zero (RatFunc.num_ne_zero hx) (RatFunc.num_ne_zero hy))
    (x * y).denom_ne_zero,
  RatFunc.num_denom_mul]