Total Degree mul

@[simp, grind _=_]theorem totalDegree_mul [IsDomain F] {f g : F[X][Y]} (hf : f ≠ 0) (hg : g ≠ 0) :    totalDegree (f * g) = totalDegree f + totalDegree g := by  apply le_antisymm (totalDegree_mul_le f g)  classical  rcases exists_max_index_totalDegree f hf with ⟨mmf, hmmf, hmmf_deg, hmmf_max⟩  rcases exists_max_index_totalDegree g hg with ⟨mmg, hmmg, hmmg_deg, hmmg_max⟩  let N := mmf + mmg  let deg := (f.coeff mmf).natDegree + (g.coeff mmg).natDegree  let term : ℕ × ℕ → F[X] := fun x => f.coeff x.1 * g.coeff x.2  have hmx : (mmf, mmg) ∈ Finset.antidiagonal N := by simp [N]  have hfx0 : f.coeff mmf ≠ 0 := Polynomial.mem_support_iff.mp hmmf  have hgx0 : g.coeff mmg ≠ 0 := Polynomial.mem_support_iff.mp hmmg  have hterm_mx : (term (mmf, mmg)).natDegree = deg := by    simpa [term, deg] using      Polynomial.natDegree_mul (p := f.coeff mmf) (q := g.coeff mmg) hfx0 hgx0  have hterm_other : ∀ y ∈ Finset.antidiagonal N, y ≠ (mmf, mmg) →      (term y).natDegree < deg ∨ term y = 0 := by    intro y hy hyne    rcases y with ⟨i, j⟩    have hij : i + j = mmf + mmg := by simpa [N] using Finset.mem_antidiagonal.mp hy    have hlt : mmf < i ∨ mmg < j := by      by_contra hcontra      push Not at hcontra      have hi : i ≤ mmf := hcontra.1      have hj : j ≤ mmg := hcontra.2      have : i = mmf ∧ j = mmg := by omega      exact hyne (by simp [this.1, this.2])    cases hlt with    | inl hi_lt =>      have hfi := hmmf_max i hi_lt      cases hfi with      | inr hfi0 => exact Or.inr (by simp [term, hfi0])      | inl hfi_lt =>        by_cases hgj0 : g.coeff j = 0        · exact Or.inr (by simp [term, hgj0])        · left          have hg_le : (g.coeff j).natDegree + j ≤ totalDegree g := by            rcases coeff_totalDegree_le' g j with h | h            · exact h            · exact absurd h hgj0          have hnat_le : (term (i, j)).natDegree ≤              (f.coeff i).natDegree + (g.coeff j).natDegree := by            simpa [term] using Polynomial.natDegree_mul_le (p := f.coeff i) (q := g.coeff j)          have hsum_lt : (f.coeff i).natDegree + (g.coeff j).natDegree < deg := by            change _ < (f.coeff mmf).natDegree + (g.coeff mmg).natDegree            have h1 := Nat.add_lt_add_of_lt_of_le hfi_lt hg_le            have h2 : totalDegree f + totalDegree g =                ((f.coeff mmf).natDegree + mmf) + ((g.coeff mmg).natDegree + mmg) := by              rw [hmmf_deg, hmmg_deg]            omega          exact lt_of_le_of_lt hnat_le hsum_lt    | inr hj_lt =>      have hgj := hmmg_max j hj_lt      cases hgj with      | inr hgj0 => exact Or.inr (by simp [term, hgj0])      | inl hgj_lt =>        by_cases hfi0 : f.coeff i = 0        · exact Or.inr (by simp [term, hfi0])        · left          have hf_le : (f.coeff i).natDegree + i ≤ totalDegree f := by            rcases coeff_totalDegree_le' f i with h | h            · exact h            · exact absurd h hfi0          have hnat_le : (term (i, j)).natDegree ≤              (f.coeff i).natDegree + (g.coeff j).natDegree := by            simpa [term] using Polynomial.natDegree_mul_le (p := f.coeff i) (q := g.coeff j)          have hsum_lt : (f.coeff i).natDegree + (g.coeff j).natDegree < deg := by            change _ < (f.coeff mmf).natDegree + (g.coeff mmg).natDegree            have h1 := Nat.add_lt_add_of_le_of_lt hf_le hgj_lt            have h2 : totalDegree f + totalDegree g =                ((f.coeff mmf).natDegree + mmf) + ((g.coeff mmg).natDegree + mmg) := by              rw [hmmf_deg, hmmg_deg]            omega          exact lt_of_le_of_lt hnat_le hsum_lt  have hsum_nat : (∑ x ∈ Finset.antidiagonal N, term x).natDegree = deg :=    natDegree_sum_eq_of_unique (mmf, mmg) hmx hterm_mx hterm_other  have hcoeff_nat : ((f * g).coeff N).natDegree = deg := by    have : (f * g).coeff N = ∑ x ∈ Finset.antidiagonal N, term x := by      simpa [term] using Polynomial.coeff_mul f g N    simpa [this] using hsum_nat  have hcoeff_ne : (f * g).coeff N ≠ 0 := by    intro h0    have hfg_nd : ((f * g).coeff N).natDegree = 0 := by simp [h0]    rw [hcoeff_nat] at hfg_nd    -- deg = 0 means all other antidiag terms are zero (natDegree < 0 impossible)    have hfg_sum : (f * g).coeff N = ∑ x ∈ Finset.antidiagonal N, term x := by      simpa [term] using Polynomial.coeff_mul f g N    -- Since deg = 0, all non-(mmf,mmg) terms are zero    have hall_zero : ∀ y ∈ Finset.antidiagonal N, y ≠ (mmf, mmg) → term y = 0 := by      intro y hy hyne      rcases hterm_other y hy hyne with h | h      · omega  -- natDegree < 0 impossible      · exact h    have : (f * g).coeff N = term (mmf, mmg) := by      rw [hfg_sum]      exact Finset.sum_eq_single_of_mem (mmf, mmg) hmx (fun y hy hyne => hall_zero y hy hyne)    rw [this] at h0    exact _root_.mul_ne_zero hfx0 hgx0 h0  have hfg_support : N ∈ (f * g).support := Polynomial.mem_support_iff.2 hcoeff_ne  have hle := coeff_totalDegree_le (f * g) hfg_support  omega