Ps exists p

lemma ps_exists_p {F : Type} [Field F]    (a_x a_y b_x b_y : ℕ) (n_x n_y : ℕ+)    (h_bx_ge_ax : b_x ≥ a_x) (h_by_ge_ay : b_y ≥ a_y)    (A B : F[X][Y])    (h_f_degX : a_x ≥ degreeX A) (h_g_degX : b_x ≥ degreeX B)    (h_f_degY : a_y ≥ natDegreeY A) (h_g_degY : b_y ≥ natDegreeY B)    (P_x P_y : Finset F) [Nonempty P_x] [Nonempty P_y]    (quot_x : F → F[X]) (quot_y : F → F[X])    (h_card_Px : n_x ≤ P_x.card) (h_card_Py : n_y ≤ P_y.card)    (h_quot_x : ∀ y ∈ P_y, (quot_x y).natDegree ≤ (b_x - a_x) ∧      evalY y B = (quot_x y) * (evalY y A))    (h_quot_y : ∀ x ∈ P_x, (quot_y x).natDegree ≤ (b_y - a_y) ∧      evalX x B = (quot_y x) * (evalX x A))    (h_le_1 : 1 > (b_x : ℚ) / (n_x : ℚ) + (b_y : ℚ) / (n_y : ℚ)) :    ∃ P : F[X][Y], B = P * A := by  classical  letI : DecidableEq F := Classical.decEq F  by_cases hB0 : B = 0  · exact ⟨0, by simp [hB0]⟩  by_cases hA0 : A = 0  · exfalso    have hBx_lt_card : b_x < P_x.card := lt_of_lt_of_le (ps_bx_lt_nx h_le_1) h_card_Px    have h_all_zero : ∀ x ∈ P_x, evalX x B = 0 := fun x hx ↦ by      simpa [hA0, ps_eval_x_eq_map] using (h_quot_y x hx).2    have := ps_card_eval_x_eq_zero_le_degree_x B hB0 P_x    rw [Finset.filter_true_of_mem h_all_zero] at this; omega  · exact ps_exists_p_nonzero a_x a_y b_x b_y n_x n_y h_bx_ge_ax h_by_ge_ay A B hA0 hB0      h_f_degX h_g_degX h_f_degY h_g_degY P_x P_y quot_x quot_y h_card_Px h_card_Py      h_quot_x h_quot_y h_le_1