Gs dvd property

theorem gs_dvd_property [DecidableEq F] (hk : k + 1 ≤ n) (hm : 1 ≤ m) (p : code ωs k)    {Q : F[X][Y]}  (hQ_deg : weightedDegree Q 1 (k - 1) ≤ gs_degree_bound k n m)  (hQ_mult : ∀ i, m ≤ rootMultiplicity Q (ωs i) (f i))  (h_dist : (hammingDist f (fun i ↦ (toPolynomial p).eval (ωs i)) : ℝ) / n <    gs_johnson k n m) :  X - C (toPolynomial p) ∣ Q := by    contrapose! h_dist with h_distots    have hR_nonzero : (Q.eval (toPolynomial p)) ≠ 0 := by      contrapose! h_distots      exact dvd_iff_isRoot.mpr h_distots    have hR_roots : (Q.eval (toPolynomial p)).natDegree ≥        m * (n - hammingDist f (fun i ↦ (toPolynomial p).eval (ωs i))) := by      have hR_roots : ∀ i ∈ Finset.univ.filter (fun i ↦ f i = (toPolynomial p).eval (ωs i)), m ≤          (Q.eval (toPolynomial p)).rootMultiplicity (ωs i) := by        intro i hi        have h_root : m ≤ (Q.eval (toPolynomial p)).rootMultiplicity (ωs i) := by          have hQ_mult : ∀ i, HasOrderAt Q (ωs i) (f i) m := by            intro i s t hst            contrapose! hQ_mult            use i            refine fun h ↦ hst.not_ge <| le_of_not_gt fun h_lt ↦ ?_            exact (by              convert rootMultiplicity_le_of_coeff_ne_zero hQ_mult using 1              cases h' : rootMultiplicity Q (ωs i) (f i)              · aesop              · simp_all only [ne_eq, WithTop.some_eq_coe, ENat.some_eq_coe, false_iff]                exact_mod_cast not_le_of_gt (lt_of_lt_of_le h_lt (mod_cast h)))          have := hQ_mult i;          have := orderAt_eval_ge Q (toPolynomial p) (ωs i) m (by aesop); aesop;        exact h_root;      have hR_roots_card : (Finset.univ.filter (fun i ↦          f i = (toPolynomial p).eval (ωs i))).card * m ≤            (Q.eval (toPolynomial p)).natDegree := by        have hR_roots_card : (∏ i ∈ Finset.univ.filter (fun i ↦            f i = (toPolynomial p).eval (ωs i)), (X - C (ωs i)) ^ m) ∣              (Q.eval (toPolynomial p)) := by          refine Finset.prod_dvd_of_coprime ?_ ?_          · intros i hi j hj hij            exact IsCoprime.pow (irreducible_X_sub_C (ωs i) |> fun hi ↦              hi.coprime_iff_not_dvd.mpr fun h => hij <| by                have := dvd_iff_isRoot.mp h; simp_all [sub_eq_iff_eq_add])          · exact fun i hi ↦              dvd_trans (pow_dvd_pow _ (hR_roots i hi)) (pow_rootMultiplicity_dvd _ _)        have := natDegree_le_of_dvd hR_roots_card        convert this hR_nonzero using 1        rw [natDegree_prod _ _ fun i hi ↦ pow_ne_zero _ <| Polynomial.X_sub_C_ne_zero _]        simp [natDegree_sub_eq_left_of_natDegree_lt]      convert hR_roots_card.ge using 1      simp only [hammingDist, ne_eq, mul_comm, mul_eq_mul_left_iff]      rw [Finset.filter_not, Finset.card_sdiff]      norm_num      exact Or.inl (Nat.sub_sub_self (le_trans (Finset.card_le_univ _) (by norm_num)))    have hR_deg : (Q.eval (toPolynomial p)).natDegree ≤ gs_degree_bound k n m := by      have hR_deg : (Q.eval (toPolynomial p)).natDegree ≤ natWeightedDegree Q 1 (k - 1) := by        apply degree_eval_le_weightedDegree        exact toPolynomial_degree_le hk p      refine le_trans hR_deg ?_      convert hQ_deg using 1      rw [weightedDegree_eq_natWeightedDegree]      aesop    contrapose! hR_roots    refine lt_of_le_of_lt hR_deg ?_    convert gs_sufficient_multiplicity_bound hk hm hR_roots using 1    rw [← @Nat.cast_lt ℝ]    norm_num [Nat.cast_sub (show hammingDist f (fun i ↦ (toPolynomial p).eval (ωs i)) ≤ n      from le_trans (Finset.card_le_univ _) (by norm_num))]