case pos
K : Type u
inst✝ : Field K
x y : RatFunc K
hy : y ≠ 0
hxy : x + y ≠ 0
hx : x = 0
⊢ intDegree (x + y) ≤ max (intDegree x) (intDegree y)

case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ intDegree (x + y) ≤ max (intDegree x) (intDegree y)
K : Type u
inst✝ : Field K
x y : RatFunc K
hy : y ≠ 0
hxy : x + y ≠ 0
⊢ intDegree (x + y) ≤ max (intDegree x) (intDegree y)
by_cases hx : x = 0
case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ natDegree (num x * denom y + denom x * num y) ≤ max (natDegree (num x * denom y)) (natDegree (denom x * num y))
case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ intDegree (x + y) ≤ max (intDegree x) (intDegree y)
rw [intDegree_add hxy, ←
  natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree hx y.denom_ne_zero,
  mul_comm y.denom, ←
  natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree hy x.denom_ne_zero,
  le_max_iff, sub_le_sub_iff_right, Int.ofNat_le, sub_le_sub_iff_right, Int.ofNat_le, ←
  le_max_iff, mul_comm y.num]
no goals
case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ natDegree (num x * denom y + denom x * num y) ≤ max (natDegree (num x * denom y)) (natDegree (denom x * num y))
exact natDegree_add_le _ _
case pos
K : Type u
inst✝ : Field K
x y : RatFunc K
hy : y ≠ 0
hx : x = 0
hxy : ¬y = 0
⊢ intDegree (x + y) ≤ max (intDegree x) (intDegree y)
case pos
K : Type u
inst✝ : Field K
x y : RatFunc K
hy : y ≠ 0
hxy : x + y ≠ 0
hx : x = 0
⊢ intDegree (x + y) ≤ max (intDegree x) (intDegree y)
simp [hx] at hxy
no goals
case pos
K : Type u
inst✝ : Field K
x y : RatFunc K
hy : y ≠ 0
hx : x = 0
hxy : ¬y = 0
⊢ intDegree (x + y) ≤ max (intDegree x) (intDegree y)
simp [hx, hxy]