Node Poly quadratic Twist Of map splits of residue of two eq zero

theorem nodePoly_quadraticTwistOf_map_splits_of_residue_of_two_eq_zero    [E.HasMultiplicativeReduction R] (t' n' : R) (h2 : (2 : ResidueField R) = 0)    (hA : residue R (E.integralModel R).c₄ * residue R t'      + residue R ((E.integralModel R).a₁ * (E.integralModel R).c₄) = 0)    (hB : residue R (E.integralModel R).c₄ * residue R n'      + residue R (54 * (E.integralModel R).b₆        - 3 * (E.integralModel R).b₂ * (E.integralModel R).b₄        + (E.integralModel R).a₂ * (E.integralModel R).c₄) = 0) :    Polynomial.Splits (((E.integralModel R).quadraticTwistOf t' n').nodePoly.map      (algebraMap R (ResidueField R))) := by  -- `D = t'²-4n'` has nonzero residue (`residue_c₄_mul_residue_eq_neg_c₆`: `φc₄·φD = -φc₆ ≠ 0`).  have hkey := residue_c₄_mul_residue_eq_neg_c₆ E R t' n' hA hB  have hDne : residue R (t' ^ 2 - 4 * n') ≠ 0 := fun h0 ↦    residue_integralModel_c₆_ne_zero E R (neg_eq_zero.mp (by rw [← hkey, h0, mul_zero]))  set c₄' := (E.integralModel R).c₄ with hc₄'  set κ' := 54 * (E.integralModel R).b₆ - 3 * (E.integralModel R).b₂ * (E.integralModel R).b₄    + (E.integralModel R).a₂ * c₄' with hκ'  simp only [map_mul] at hA  have hc₄0 : residue R (E.integralModel R).c₄ ≠ 0 := residue_integralModel_c₄_ne_zero E R  have hc₄map : algebraMap R (ResidueField R) (E.integralModel R).c₄ ≠ 0 := by    rw [ResidueField.algebraMap_eq]; exact hc₄0  set D := t' ^ 2 - 4 * n' with hDdef  have h4 : (4 : ResidueField R) = 0 := by    rw [show (4 : ResidueField R) = 2 * 2 by norm_num, h2, mul_zero]  have hDmap : algebraMap R (ResidueField R) D ≠ 0 := by    rw [ResidueField.algebraMap_eq]; exact hDne  have hDt : residue R D = residue R t' ^ 2 := by    rw [hDdef, map_sub, map_mul, map_pow, map_ofNat, h4, zero_mul, sub_zero]  have hWc₄ : algebraMap R (ResidueField R)      ((E.integralModel R).quadraticTwistOf t' n').c₄ ≠ 0 := by    rw [c₄_quadraticTwistOf, ← hDdef, map_mul, map_pow]    exact mul_ne_zero (pow_ne_zero 2 hDmap) hc₄map  have hWc₆ : algebraMap R (ResidueField R)      ((E.integralModel R).quadraticTwistOf t' n').c₆ ≠ 0 := by    rw [c₆_quadraticTwistOf, ← hDdef, map_mul, map_pow]    exact mul_ne_zero (pow_ne_zero 3 hDmap)      (by rw [ResidueField.algebraMap_eq]; exact residue_integralModel_c₆_ne_zero E R)  have hta : residue R (E.integralModel R).a₁ = -residue R t' := by    rcases mul_eq_zero.mp (show residue R c₄'        * (residue R t' + residue R (E.integralModel R).a₁) = 0 by linear_combination hA)      with hz | hz    · exact absurd hz hc₄0    · linear_combination hz  have hκW_eq : 54 * ((E.integralModel R).quadraticTwistOf t' n').b₆      - 3 * ((E.integralModel R).quadraticTwistOf t' n').b₂          * ((E.integralModel R).quadraticTwistOf t' n').b₄      + ((E.integralModel R).quadraticTwistOf t' n').a₂          * ((E.integralModel R).quadraticTwistOf t' n').c₄      = D ^ 3 * κ' - D ^ 2 * n' * (E.integralModel R).a₁ ^ 2 * c₄' := by    rw [hDdef, hκ', hc₄']    exact kappa_quadraticTwistOf (E.integralModel R) t' n'  have hWc₄eq : ((E.integralModel R).quadraticTwistOf t' n').c₄ = D ^ 2 * c₄' := by    rw [c₄_quadraticTwistOf, ← hDdef, hc₄']  have hκW0 : algebraMap R (ResidueField R)      (D ^ 3 * κ' - D ^ 2 * n' * (E.integralModel R).a₁ ^ 2 * c₄') = 0 := by    simp only [map_sub, map_mul, map_pow, ResidueField.algebraMap_eq, hDt, hta]    linear_combination (residue R t') ^ 6 * hB      - (residue R t') ^ 6 * residue R n' * residue R c₄' * h2  rw [nodePoly_map_splits_iff_of_two_eq_zero h2 (algebraMap R (ResidueField R))    ((E.integralModel R).quadraticTwistOf t' n') hWc₄ hWc₆]  refine ⟨0, ?_⟩  rw [hκW_eq, hWc₄eq, show (0 : ResidueField R) ^ 2 + 0 = 0 from by ring, mul_zero, hκW0,    neg_zero, mul_zero]