case pos
K : Type u
inst✝ : Field K
x : RatFunc K
hx : x = 0
⊢ intDegree (-x) = intDegree x

case neg
K : Type u
inst✝ : Field K
x : RatFunc K
hx : ¬x = 0
⊢ intDegree (-x) = intDegree x
K : Type u
inst✝ : Field K
x : RatFunc K
⊢ intDegree (-x) = intDegree x
by_cases hx : x = 0
no goals
case pos
K : Type u
inst✝ : Field K
x : RatFunc K
hx : x = 0
⊢ intDegree (-x) = intDegree x
rw [hx, neg_zero]
case neg
K : Type u
inst✝ : Field K
x : RatFunc K
hx : ¬x = 0
⊢ ↑(natDegree (num (-x))) - ↑(natDegree (denom (-x))) = ↑(natDegree (-num x)) - ↑(natDegree (denom x))
case neg
K : Type u
inst✝ : Field K
x : RatFunc K
hx : ¬x = 0
⊢ intDegree (-x) = intDegree x
rw [intDegree, intDegree, ← natDegree_neg x.num]
no goals
case neg
K : Type u
inst✝ : Field K
x : RatFunc K
hx : ¬x = 0
⊢ ↑(natDegree (num (-x))) - ↑(natDegree (denom (-x))) = ↑(natDegree (-num x)) - ↑(natDegree (denom x))
exact
  natDegree_sub_eq_of_prod_eq (num_ne_zero (neg_ne_zero.mpr hx)) (denom_ne_zero (-x))
    (neg_ne_zero.mpr (num_ne_zero hx)) (denom_ne_zero x) (num_denom_neg x)