Ps resultant dvd pow eval x

lemma ps_resultant_dvd_pow_eval_x {F : Type} [Field F]    (A B : F[X][Y]) (x : F) (Q : F[X]) (n : ℕ)    (hmn : natDegreeY A ≤ n) (hn : natDegreeY B ≤ n)    (hQdeg : Q.natDegree ≤ n - natDegreeY A)    (hQ : evalX x B = Q * evalX x A) :    (X - C x) ^ (natDegreeY A) ∣ resultant B A n (natDegreeY A) := by  classical  set m := natDegreeY A with hm  let p : F[X] := X - C x  let M0 : Matrix (Fin (n + m)) (Fin (n + m)) F[X] := sylvester B A n m  let U : Matrix (Fin (n + m)) (Fin (n + m)) F[X] := fun i j ↦    j.addCases      (fun jn ↦ if i = .castAdd m jn then 1 else 0)      (fun jm ↦ i.addCases        (fun in_ ↦ -C ((Q * X ^ (jm : ℕ)).coeff in_))        (fun im_ ↦ if im_ = jm then 1 else 0))  let M1 := M0 * U  have h_u_det : U.det = 1 := by    have h_u_tri : U.BlockTriangular (fun x : Fin (n + m) ↦ x) := by      intro i j hij      induction j using Fin.addCases with      | left jn => simp [U, ne_of_gt hij]      | right jm =>        induction i using Fin.addCases with        | left in_ =>          exact absurd hij (not_lt_of_ge (Fin.lt_def.2 (by simp; omega) |>.le))        | right im_ =>          simp [U, (show im_ ≠ jm from fun hEq ↦ ne_of_gt hij (by simp [hEq]))]    rw [det_of_upperTriangular h_u_tri]; simp [Fin.prod_univ_add, U]  have hdet1 : M1.det = M0.det := by simp [M1, det_mul, h_u_det, M0]  let ev : F[X] →+* F := evalRingHom x  have hdiv_entry (i : Fin (n + m)) (j' : Fin m) : p ∣ M1 i (.natAdd n j') := by    let col : Fin (n + m) := .natAdd n j'    let v_col : Fin (n + m) → F := fun k ↦ ev (U k col)    suffices hx0 : ev (M1 i col) = 0 by      change eval x (M1 i (.natAdd n j')) = 0 at hx0      exact dvd_iff_isRoot.2 (by simpa [IsRoot] using hx0)    have hM0map : M0.map (⇑ev) = sylvester (B.map ev) (A.map ev) n m := by      simpa [M0] using ps_sylvester_map ev A B m n    have hmA : (A.map ev).natDegree ≤ m :=      le_trans natDegree_map_le (by simp [hm, natDegreeY])    have hnB : (B.map ev).natDegree ≤ n :=      le_trans natDegree_map_le (by simpa [natDegreeY] using hn)    set q : F[X] := Q * X ^ (j' : ℕ) with hq_def    have hqdeg_lt : q.natDegree < n :=      lt_of_le_of_lt (ps_nat_degree_mul_x_pow_le Q j' hmn hQdeg)        (Nat.sub_lt (lt_of_lt_of_le (Fin.size_positive j') hmn) Nat.one_pos)    have hBmap : B.map ev = Q * A.map ev := by simpa [ps_eval_x_eq_map, ev] using hQ    have hsum_left : (∑ j : Fin n, monomial (j : ℕ) (v_col (.castAdd m j))) = -q := by      have hv : (fun j : Fin n ↦ v_col (.castAdd m j)) = fun j : Fin n ↦ -(toFn n q j) := by        funext j; simp [v_col, col, U, ev, q, toFn]      rw [show (∑ j : Fin n, monomial (j : ℕ) (v_col (.castAdd m j))) =          ofFn n (fun j ↦ v_col (.castAdd m j)) from by        simpa using (ofFn_eq_sum_monomial <| fun j : Fin n ↦ v_col (.castAdd m j)).symm,        hv, show ofFn n (fun j : Fin n ↦ -(toFn n q j)) = -ofFn n (toFn n q) from by          simp [ofFn_eq_sum_monomial], ofFn_comp_toFn_eq_id_of_natDegree_lt hqdeg_lt]    have hsum_right :        (∑ j : Fin m, monomial (j : ℕ) (v_col (.natAdd n j))) = X ^ (j' : ℕ) := by      classical      have hv (j : Fin m) : v_col (.natAdd n j) = if j = j' then (1 : F) else 0 := by        by_cases h : j = j' <;> simp [v_col, col, U, ev, h]      simp_rw [hv]      have hfun (j : Fin m) : monomial (j : ℕ) (if j = j' then (1 : F) else 0) =          if j = j' then monomial (j : ℕ) (1 : F) else 0 := by        by_cases hj : j = j' <;> simp [hj]      simp_rw [hfun]; simp [monomial_one_right_eq_X_pow]    have hSylv : ev (M1 i col) = (sylvester (B.map ev) (A.map ev) n m).mulVec v_col i := by      have := RingHom.map_matrix_mul (M := M0) (N := U) (i := i) (j := col) (f := ev)      simpa [M1, mul_apply, mulVec, dotProduct, v_col, hM0map] using this    rw [hSylv, congrArg (fun f : (Fin (n + m) → F) ↦ f i)      (ps_sylvester_mul_vec_eq_coeff_add (A.map ev) (B.map ev) m n hmA hnB v_col)]    simp [hsum_left, hsum_right, hBmap, q, mul_assoc, mul_left_comm, mul_comm]  classical  let q_mat : Matrix (Fin (n + m)) (Fin (n + m)) F[X] := fun i j ↦    j.addCases (fun jn ↦ M1 i (.castAdd m jn)) (fun jm ↦ Classical.choose (hdiv_entry i jm))  have hQs (i : Fin (n + m)) (j' : Fin m) : M1 i (.natAdd n j') = p * q_mat i (.natAdd n j') := by    simpa [q_mat, Fin.addCases_right] using Classical.choose_spec (hdiv_entry i j')  let v : Fin (n + m) → F[X] := fun j ↦ j.addCases (fun _ ↦ 1) (fun _ ↦ p)  have hM1_scale : M1 = fun i j ↦ v j * q_mat i j := by    apply Matrix.ext; intro i j    induction j using Fin.addCases with    | left jn => simp [v, q_mat, Fin.addCases_left]    | right jm => simpa [v, q_mat, Fin.addCases_right, mul_assoc] using hQs i jm  have hdivM1 : p ^ m ∣ M1.det :=    ⟨q_mat.det, by      rw [show M1.det = (∏ j, v j) * q_mat.det from by        rw [hM1_scale]        exact det_mul_row v q_mat]      simp [Fin.prod_univ_add, v]⟩  simpa [p, m, hm, natDegreeY, resultant, M0] using (hdet1 ▸ hdivM1)