Exists max index total Degree

theorem exists_max_index_totalDegree (f : F[X][Y]) (hf : f ≠ 0) :    ∃ mm ∈ f.support,      (f.coeff mm).natDegree + mm = totalDegree f ∧      ∀ n, mm < n → (f.coeff n).natDegree + n < totalDegree f ∨ f.coeff n = 0 := by  classical  let s₁ : Finset ℕ := f.support.filter (fun n => (f.coeff n).natDegree + n = totalDegree f)  have hs₁ : s₁.Nonempty := by    have hsupp : f.support.Nonempty := Polynomial.support_nonempty.2 hf    obtain ⟨m, hm_mem, hm_sup⟩ :=      Finset.exists_mem_eq_sup _ hsupp (fun n => (f.coeff n).natDegree + n)    have hm_deg : (f.coeff m).natDegree + m = totalDegree f := by      simpa [totalDegree] using hm_sup.symm    exact ⟨m, Finset.mem_filter.mpr ⟨hm_mem, hm_deg⟩⟩  set mm : ℕ := s₁.max' hs₁ with hmm  have hmm_mem_s₁ : mm ∈ s₁ := by simpa [hmm] using Finset.max'_mem s₁ hs₁  have hmm_filter : mm ∈ f.support ∧ (f.coeff mm).natDegree + mm = totalDegree f := by    simpa [s₁] using Finset.mem_filter.mp hmm_mem_s₁  refine ⟨mm, hmm_filter.1, hmm_filter.2, ?_⟩  intro n hmn  by_cases hn0 : f.coeff n = 0  · exact Or.inr hn0  · have hn_support : n ∈ f.support := Polynomial.mem_support_iff.2 hn0    have hn_le : (f.coeff n).natDegree + n ≤ totalDegree f := coeff_totalDegree_le f hn_support    have hn_ne : (f.coeff n).natDegree + n ≠ totalDegree f := by      intro hEq      have hn_s₁ : n ∈ s₁ := Finset.mem_filter.mpr ⟨hn_support, hEq⟩      have : n ≤ mm := Finset.le_max' s₁ n hn_s₁      exact not_le_of_gt hmn this    exact Or.inl (lt_of_le_of_ne hn_le hn_ne)