Ps exists qy of cancel

lemma ps_exists_qy_of_cancel {F : Type} [Field F]    (a_y : ℕ) (n_y : ℕ+) {A B P : F[X][Y]} (hA : A ≠ 0) (hBA : B = P * A)    (P_y : Finset F) (h_card_Py : n_y ≤ P_y.card) (quot_x : F → F[X])    (h_quot_x : ∀ y ∈ P_y, evalY y B = (quot_x y) * (evalY y A))    (h_f_degY : a_y ≥ natDegreeY A) :    ∃ Q_y : Finset F, Q_y.card ≥ (n_y : ℕ) - a_y ∧ Q_y ⊆ P_y ∧      ∀ y ∈ Q_y, evalY y P = quot_x y := by  classical  refine ⟨P_y.filter (fun y ↦ evalY y A ≠ 0), ?_, Finset.filter_subset _ _, ?_⟩  · have := ps_card_eval_y_eq_zero_le_nat_degree_y A hA P_y    have := Finset.card_filter_add_card_filter_not (s := P_y) (fun y ↦ evalY y A = 0)    have : {a ∈ P_y | ¬evalY a A = 0}.card = {y ∈ P_y | evalY y A ≠ 0}.card := rfl    omega  · intro y hy    exact mul_right_cancel₀ (Finset.mem_filter.mp hy).2 (by      rw [← show evalY y (P * A) = evalY y P * evalY y A from by simp [evalY], ← hBA]      exact h_quot_x y (Finset.mem_filter.mp hy).1)