Ps exists p nonzero

lemma ps_exists_p_nonzero {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]) (hA0 : A ≠ 0) (hB0 : B ≠ 0)    (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 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  rcases ps_gcd_decompose (A := A) (B := B) hA0 hB0 with ⟨G, A1, B1, hA, hB, hrel, hA1, hB1⟩  have hG0 : G ≠ 0 := fun hG ↦ hA0 (by simp [hA, hG])  set g_x := degreeX G; set g_y := natDegreeY G  have hdegX_A : degreeX A = g_x + degreeX A1 := by    rw [hA]; simpa [g_x] using degreeX_mul G A1 hG0 hA1  have hdegY_A : natDegreeY A = g_y + natDegreeY A1 := by    rw [hA]; simpa [g_y] using degreeY_mul G A1 hG0 hA1  have hdegX_B : degreeX B = g_x + degreeX B1 := by    rw [hB]; simpa [g_x] using degreeX_mul G B1 hG0 hB1  have hdegY_B : natDegreeY B = g_y + natDegreeY B1 := by    rw [hB]; simpa [g_y] using degreeY_mul G B1 hG0 hB1  have hbxltnx := ps_bx_lt_nx h_le_1  have hbyltny := ps_by_lt_ny h_le_1  have hgx_le_ax : g_x ≤ a_x := le_trans (by simp [hdegX_A]) h_f_degX  have hgy_le_ay : g_y ≤ a_y := le_trans (by simp [hdegY_A]) h_f_degY  have hgx_le_bx : g_x ≤ b_x := le_trans hgx_le_ax h_bx_ge_ax  have hgy_le_by : g_y ≤ b_y := le_trans hgy_le_ay h_by_ge_ay  have hx_lt_nx : g_x < (n_x : ℕ) := lt_of_le_of_lt hgx_le_bx hbxltnx  have hy_lt_ny : g_y < (n_y : ℕ) := lt_of_le_of_lt hgy_le_by hbyltny  let Px' := P_x.filter (fun x ↦ evalX x G ≠ 0)  let Py' := P_y.filter (fun y ↦ evalY y G ≠ 0)  have hcard_Px' : (n_x : ℕ) - g_x ≤ Px'.card := by    have := Finset.card_filter_add_card_filter_not (s := P_x) (fun x ↦ evalX x G = 0)    have := by simpa [g_x] using ps_card_eval_x_eq_zero_le_degree_x (A := G) hG0 P_x    have : {a ∈ P_x | ¬evalX a G = 0}.card = Px'.card := rfl    omega  have hcard_Py' : (n_y : ℕ) - g_y ≤ Py'.card := by    have := Finset.card_filter_add_card_filter_not (s := P_y) (fun y ↦ evalY y G = 0)    have := by simpa [g_y] using ps_card_eval_y_eq_zero_le_nat_degree_y G hG0 P_y    have : {a ∈ P_y | ¬evalY a G = 0}.card = Py'.card := rfl    omega  haveI : Nonempty Px' := ⟨⟨_, (Finset.card_pos.mp (by omega)).choose_spec⟩⟩  haveI : Nonempty Py' := ⟨⟨_, (Finset.card_pos.mp (by omega)).choose_spec⟩⟩  let ax' := a_x - g_x; let ay' := a_y - g_y  let bx' := b_x - g_x; let by' := b_y - g_y  let nx' : ℕ+ := ⟨(n_x : ℕ) - g_x, Nat.sub_pos_of_lt hx_lt_nx⟩  let ny' : ℕ+ := ⟨(n_y : ℕ) - g_y, Nat.sub_pos_of_lt hy_lt_ny⟩  have hdiff_x : bx' - ax' = b_x - a_x := by    simpa [bx', ax'] using tsub_tsub_tsub_cancel_right hgx_le_ax  have hdiff_y : by' - ay' = b_y - a_y := by    simpa [by', ay'] using tsub_tsub_tsub_cancel_right hgy_le_ay  have hquotX' : ∀ y ∈ Py', (quot_x y).natDegree ≤ (bx' - ax') ∧      evalY y B1 = (quot_x y) * evalY y A1 := fun y hy ↦    ⟨hdiff_x ▸ (h_quot_x y (Finset.mem_filter.mp hy).1).1,     ps_descend_eval_y hA hB y (Finset.mem_filter.mp hy).2 _       (h_quot_x y (Finset.mem_filter.mp hy).1).2⟩  have hquotY' : ∀ x ∈ Px', (quot_y x).natDegree ≤ (by' - ay') ∧      evalX x B1 = (quot_y x) * evalX x A1 := fun x hx ↦    ⟨hdiff_y ▸ (h_quot_y x (Finset.mem_filter.mp hx).1).1,     ps_descend_eval_x hA hB x (Finset.mem_filter.mp hx).2 _       (h_quot_y x (Finset.mem_filter.mp hx).1).2⟩  have hxfrac : (bx' : ℚ) / (nx' : ℚ) ≤ (b_x : ℚ) / (n_x : ℚ) := by    have hn2 : (0 : ℚ) < (nx' : ℚ) := by exact_mod_cast nx'.pos    have hbx'cast : (bx' : ℚ) = (b_x : ℚ) - g_x := by simp [bx', Nat.cast_sub hgx_le_bx]    have hnx'cast : (nx' : ℚ) = (n_x : ℚ) - g_x := by      simp [nx', Nat.cast_sub (le_of_lt hx_lt_nx)]    rw [hbx'cast, hnx'cast,      div_le_div_iff₀ (by rw [hnx'cast] at hn2; exact hn2) (by exact_mod_cast n_x.pos)]    nlinarith [show (b_x : ℚ) ≤ n_x from by exact_mod_cast le_of_lt hbxltnx,      Nat.cast_nonneg (α := ℚ) g_x]  have hyfrac : (by' : ℚ) / (ny' : ℚ) ≤ (b_y : ℚ) / (n_y : ℚ) := by    have hn2 : (0 : ℚ) < (ny' : ℚ) := by exact_mod_cast ny'.pos    have hby'cast : (by' : ℚ) = (b_y : ℚ) - g_y := by simp [by', Nat.cast_sub hgy_le_by]    have hny'cast : (ny' : ℚ) = (n_y : ℚ) - g_y := by      simp [ny', Nat.cast_sub (le_of_lt hy_lt_ny)]    rw [hby'cast, hny'cast,      div_le_div_iff₀ (by rw [hny'cast] at hn2; exact hn2) (by exact_mod_cast n_y.pos)]    nlinarith [show (b_y : ℚ) ≤ n_y from by exact_mod_cast le_of_lt hbyltny,      Nat.cast_nonneg (α := ℚ) g_y]  have hconst := ps_coprime_case_constant ax' ay' bx' by' nx' ny'    (by simpa [bx', ax'] using Nat.sub_le_sub_right h_bx_ge_ax g_x)    (by simpa [by', ay'] using Nat.sub_le_sub_right h_by_ge_ay g_y)    A1 B1 hA1 hB1 hrel    (by simpa [ax', ge_iff_le] using      le_tsub_of_add_le_left (show g_x + degreeX A1 ≤ a_x by simpa [hdegX_A] using h_f_degX))    (by simpa [bx', ge_iff_le] using      le_tsub_of_add_le_left (show g_x + degreeX B1 ≤ b_x by simpa [hdegX_B] using h_g_degX))    (by simpa [ay', ge_iff_le] using      le_tsub_of_add_le_left (show g_y + natDegreeY A1 ≤ a_y by simpa [hdegY_A] using h_f_degY))    (by simpa [by', ge_iff_le] using      le_tsub_of_add_le_left (show g_y + natDegreeY B1 ≤ b_y by simpa [hdegY_B] using h_g_degY))    Px' Py' quot_x quot_y    (by simpa [nx'] using hcard_Px') (by simpa [ny'] using hcard_Py')    hquotX' hquotY' (lt_of_le_of_lt (add_le_add hxfrac hyfrac) h_le_1)  rcases ps_exists_p_of_degree_x_eq_zero_nat_degree_y_eq_zero hA1 hconst.1 hconst.2 (B := B1)    with ⟨P1, hB1fac⟩  exact ⟨P1, by rw [hB, hB1fac, hA]; ring⟩