Ps resultant ne zero of is rel prime

lemma ps_resultant_ne_zero_of_is_rel_prime {F : Type} [Field F]    (A B : F[X][Y]) (n : ℕ)    (hn : natDegreeY B ≤ n) (hA0 : A ≠ 0) (hrel : IsRelPrime A B) :    resultant B A n (natDegreeY A) ≠ 0 := by  classical  set m := natDegreeY A with hm  intro hres  rcases (exists_mulVec_eq_zero_iff (M := sylvester B A n m)).2    (by simpa [resultant] using hres) with ⟨v, hv0, hv⟩  let P : F[X][Y] := ∑ j : Fin n, monomial (j : ℕ) (v (.castAdd m j))  let Q : F[X][Y] := ∑ j : Fin m, monomial (j : ℕ) (v (.natAdd n j))  have hP_ofFn : P = ofFn n (fun j : Fin n ↦ v (.castAdd m j)) := by    simpa [P] using (ofFn_eq_sum_monomial (fun j ↦ v (.castAdd m j))).symm  have hQ_ofFn : Q = ofFn m (fun j : Fin m ↦ v (.natAdd n j)) := by    simpa [Q] using (ofFn_eq_sum_monomial (fun j ↦ v (.natAdd n j))).symm  have hvcoeff (i : Fin (n + m)) : (A * P + B * Q).coeff (i : ℕ) = 0 := by    have hsyl := congrFun      (ps_sylvester_mul_vec_eq_coeff_add A B m n        (by simp [hm, natDegreeY]) (by simpa [natDegreeY] using hn) v) i    simpa [P, Q] using (show      (A * (∑ j : Fin n, monomial (j : ℕ) (v (.castAdd m j))) +       B * (∑ j : Fin m, monomial (j : ℕ) (v (.natAdd n j)))).coeff (i : ℕ) = 0 from by        rw [← hsyl]; exact congrFun hv i)  have hnmpos : 0 < n + m := by    by_contra h; exact hv0 (funext fun i ↦ absurd i.isLt (by omega))  have hA_nd : A.natDegree = m := by simpa [natDegreeY] using hm.symm  have hcomb : A * P + B * Q = 0 := by    apply Polynomial.ext; intro k    by_cases hk : k < n + m    · simpa using hvcoeff ⟨k, hk⟩    · have hdegAP : (A * P).natDegree < n + m := by        by_cases hn0 : n = 0        · subst hn0; simpa [P] using (show 0 < m by omega)        · exact lt_of_le_of_lt natDegree_mul_le (by            rw [hA_nd]; have : P.natDegree < n := by              simpa [hP_ofFn] using                ofFn_natDegree_lt (show 1 ≤ n by omega) (fun j ↦ v (.castAdd m j))            omega)      have hdegBQ : (B * Q).natDegree < n + m := by        by_cases hm0 : m = 0        · rw [show Q = 0 from by simp [hm0, hQ_ofFn, ofFn]; rfl]; simp; omega        · have hndeg : B.natDegree ≤ n := by simpa [natDegreeY] using hn          have hQnat : Q.natDegree < m := by            simpa [hQ_ofFn] using              ofFn_natDegree_lt (show 1 ≤ m by omega) (fun j ↦ v (.natAdd n j))          exact lt_of_le_of_lt natDegree_mul_le (by omega)      exact coeff_eq_zero_of_natDegree_lt (by        have := lt_of_le_of_lt (natDegree_add_le _ _) (max_lt hdegAP hdegBQ); omega)  have hA_dvd_BQ : A ∣ B * Q :=    ⟨-P, (neg_eq_of_add_eq_zero_left (by rwa [add_comm] at hcomb)).symm.trans (mul_neg A P).symm⟩  have hA_dvd_Q : A ∣ Q := hrel.dvd_of_dvd_mul_left hA_dvd_BQ  have hQ0 : Q = 0 := by    by_cases hm0 : m = 0    · simp_all only [m, P, Q]      ext n_1 n_2 : 2      simp_all only [zero_le, ofFn_coeff_eq_zero_of_ge, coeff_zero]    · rcases hA_dvd_Q with ⟨R, hR⟩      by_contra hQ_ne      have hR0 : R ≠ 0 := by rintro rfl; exact hQ_ne (by simpa using hR)      have : A.natDegree + R.natDegree < m := by        rw [← natDegree_mul hA0 hR0, ← hR]        simpa [hQ_ofFn] using          ofFn_natDegree_lt (show 1 ≤ m by omega) (fun j ↦ v (.natAdd n j))      omega  have hP0 : P = 0 := (mul_eq_zero.mp (by simpa [hQ0] using hcomb)).resolve_left hA0  exact hv0 (funext ((Fin.forall_fin_add <| fun i ↦ v i = 0).2    ⟨fun j ↦ by simpa [hP_ofFn] using congrArg (Polynomial.coeff · (j : ℕ)) hP0,     fun j ↦ by simpa [hQ_ofFn] using congrArg (Polynomial.coeff · (j : ℕ)) hQ0⟩))