Nat Weighted Degree add le

lemma natWeightedDegree_add_le (p q : F[X][Y]) (u v : ℕ) :    natWeightedDegree (p + q) u v ≤ max (natWeightedDegree p u v) (natWeightedDegree q u v) := by  refine Finset.sup_le fun m hm ↦ ?_  by_cases h : m ∈ p.support <;>  by_cases h' : m ∈ q.support <;>    simp_all only [Polynomial.mem_support_iff, coeff_add, ne_eq, le_sup_iff]  · have h_deg : (p.coeff m + q.coeff m).natDegree ≤        max ((p.coeff m).natDegree) ((q.coeff m).natDegree) :=      natDegree_add_le (p.coeff m) (q.coeff m)    cases max_cases (natDegree (p.coeff m))      (natDegree (q.coeff m)) <;> simp_all only [sup_of_le_left, sup_eq_left, and_self,        natWeightedDegree]    · exact Or.inl (le_trans (add_le_add (mul_le_mul_of_nonneg_left h_deg <|        Nat.zero_le _) le_rfl) <| Finset.le_sup (f := fun m ↦ u * natDegree          (p.coeff m) + v * m) <| by aesop)    · exact Or.inr (le_trans (add_le_add (mul_le_mul_of_nonneg_left h_deg <|        Nat.zero_le _) le_rfl) <| Finset.le_sup        (f := fun m ↦ u * natDegree (q.coeff m) + v * m) <| by aesop)  all_goals simp_all only [not_not, add_zero, zero_add, not_false_eq_true]  · exact Or.inl <| Finset.le_sup (f := fun m ↦ u * natDegree (p.coeff m) + v * m) <| by aesop  · exact Or.inr <| Finset.le_sup (f := fun m ↦ u * natDegree (q.coeff m) + v * m) <| by aesop  · simp at hm