Root Multiplicity le of coeff ne zero

lemma rootMultiplicity_le_of_coeff_ne_zero [DecidableEq F] {Q : F[X][Y]} {x y : F} {s t : ℕ}    (h : Bivariate.coeff (shift Q x y) s t ≠ 0) :    rootMultiplicity Q x y ≤ (s + t : WithTop ℕ) := by      set g : F[X][Y] := shift Q x y;      have h_rootMultiplicity : Polynomial.Bivariate.rootMultiplicity Q x y =          List.min? (List.filterMap (fun p ↦            if Bivariate.coeff g p.1 p.2 = 0 then none            else some (p.1 + p.2)) (List.product (List.range              (natWeightedDegree g 1 1 + 1)) (List.range (natWeightedDegree g 1 1 + 1)))) := by        rw [Bivariate.rootMultiplicity, Bivariate.rootMultiplicity₀,          Bivariate.weightedDegree_eq_natWeightedDegree]      obtain ⟨p, hp⟩ : ∃ p ∈ List.product (List.range (natWeightedDegree g 1 1 + 1))          (List.range (natWeightedDegree g 1 1 + 1)), p.1 + p.2 = s + t ∧            Bivariate.coeff g p.1 p.2 ≠ 0 := by        use (s, t);        have h_deg : s + t ≤ Bivariate.natWeightedDegree g 1 1 := by          refine Finset.le_sup (f := fun m ↦ 1 * ((g.coeff m).natDegree ) + 1 * m)              (Finset.mem_coe.mpr <| Polynomial.mem_support_iff.mpr <|                show g.coeff t ≠ 0 from ?_) |> le_trans ?_          · simp +zetaDelta only [ne_eq, one_mul, add_le_add_iff_right] at *            exact le_natDegree_of_ne_zero h          · exact fun h' => h <| by rw [Polynomial.Bivariate.coeff]; aesop        exact ⟨List.mem_product.mpr ⟨List.mem_range.mpr (by linarith),          List.mem_range.mpr (by linarith)⟩, rfl, h⟩      have h_min_le : ∀ {l : List ℕ} {m : ℕ}, m ∈ l → (List.min? l).getD 0 ≤ m := by        exact fun {l} {m} a ↦ List.min?_getD_le_of_mem a      convert h_min_le _      any_goals exact List.filterMap (fun p ↦ if Bivariate.coeff g p.1 p.2 = 0        then Option.none else Option.some (p.1 + p.2)) (List.product (List.range          (natWeightedDegree g 1 1 + 1)) (List.range (natWeightedDegree g 1 1 + 1 )))      rotate_left      · exact p.1 + p.2      · rw [List.mem_filterMap]; aesop      · cases h : List.min? (List.filterMap (fun p ↦ if Bivariate.coeff g p.1 p.2 = 0          then Option.none else Option.some (p.1 + p.2)) (List.product (List.range            (natWeightedDegree g 1 1 + 1)) (List.range (natWeightedDegree g 1 1 + 1)))) <;> aesop