Root Multiplicity ge of shift zero

lemma rootMultiplicity_ge_of_shift_zero [DecidableEq F] {f : F[X][Y]} {x y : F}    {m : ℕ} (hf : f ≠ 0) (h : ∀ s t, s + t < m → ((shift f x y).coeff t).coeff s = 0) :    m ≤ rootMultiplicity f x y := by  by_contra h_contra  cases h : rootMultiplicity f x y  · simp_all only [ne_eq, Bivariate.rootMultiplicity, Option.le_none, reduceCtorEq,      not_false_eq_true, rootMultiplicity₀]    cases h' : weightedDegree (shift f x y) 1 1    · exact absurd h' (weightedDegree_ne_none _ _ _)    · simp_all +decide only [Nat.succ_eq_add_one, List.min?_eq_none_iff, List.filterMap_eq_nil_iff,        ite_eq_left_iff, reduceCtorEq, imp_false, Decidable.not_not, Prod.forall,        List.pair_mem_product, List.mem_range, and_imp]      have h_zero_poly : shift f x y = 0 := by        have h_zero_poly : ∀ p : F[X][Y], (∀ s t, s ≤ natWeightedDegree p 1 1 →            t ≤ natWeightedDegree p 1 1 → Polynomial.Bivariate.coeff p s t = 0) → p = 0 := by          intros p hp_zero          by_contra hp_nonzero          obtain ⟨s, t, hs⟩ : ∃ s t, Polynomial.Bivariate.coeff p s t ≠ 0 ∧              s ≤ natWeightedDegree p 1 1 ∧ t ≤ natWeightedDegree p 1 1 := by            obtain ⟨s, t, hs⟩ : ∃ s t, Polynomial.Bivariate.coeff p s t ≠ 0 := by              contrapose! hp_nonzero              ext s              aesop            refine ⟨s, t, hs, ?_, ?_⟩            · refine le_trans ?_ ( Finset.le_sup <| show (t : ℕ) ∈ p.support from ?_)              · exact le_trans (le_natDegree_of_ne_zero hs) (by linarith)              · simp_all only [Bivariate.coeff, ne_eq, Polynomial.mem_support_iff]                exact fun h ↦ hs <| by rw [h]; norm_num            · refine le_trans ?_ (Finset.le_sup <| Finsupp.mem_support_iff.mpr <|                show p.coeff t ≠ 0 from ?_)              · norm_num              · exact fun h ↦ hs <| by rw [Bivariate.coeff]; aesop          exact hs.1 (hp_zero s t hs.2.1 hs.2.2)        apply h_zero_poly        intros s t hs ht        convert h s t _ _ using 1        all_goals          rw [weightedDegree_eq_natWeightedDegree] at h'          grind      simp_all only [weightedDegree, coeff_zero, natDegree_zero, mul_zero, one_mul, zero_add,        Nat.succ_eq_add_one, List.range_one, List.map_cons, List.map_nil, List.max?_cons,        List.max?_nil, Option.elim_none, Option.some.injEq]      exact hf (shift_eq_zero_iff f x y |>.1 h_zero_poly)  · obtain ⟨deg, hdeg⟩ := Option.ne_none_iff_exists'.mp      (weightedDegree_ne_none (shift f x y) 1 1)    simp_all only [ne_eq, Option.some_le_some, not_le, weightedDegree, shift,      coeff_map, coe_compRingHom, one_mul, Nat.succ_eq_add_one]    have h_min_ge_m : ∀ p ∈ List.filterMap (fun p ↦ if Bivariate.coeff        (Polynomial.map (X + C x).compRingHom (f.comp (Y + C (C y)))) p.1 p.2 = 0          then Option.none else Option.some (p.1 + p.2))            (List.product (List.range (deg + 1)) (List.range (deg + 1))), m ≤ p := by      simp +zetaDelta only [List.mem_filterMap, Option.ite_none_left_eq_some, Option.some.injEq,        Prod.exists, List.pair_mem_product, List.mem_range, forall_exists_index, and_imp] at *      intro p s t hs ht hne hp      subst hp      contrapose! hne      simp only [Bivariate.coeff, Polynomial.coeff_map, Polynomial.coe_compRingHom]      aesop    have hmem := h    simp only [Bivariate.rootMultiplicity, rootMultiplicity₀] at hmem    have hdeg' : weightedDegree (shift f x y) 1 1 = some deg := by      simpa [weightedDegree, shift] using hdeg    rw [hdeg'] at hmem    exact absurd (h_min_ge_m _ (List.min?_mem hmem))      (by push Not; exact h_contra)