Node Poly quadratic Twist Of map splits of residue

theorem nodePoly_quadraticTwistOf_map_splits_of_residue    [E.HasMultiplicativeReduction R] (t' n' : R)    (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  rcases ne_or_eq (2 : ResidueField R) 0 with h2 | h2  · -- Residue characteristic `≠ 2`: split ↔ `IsSquare (φ((t'²-4n')·-(c₄c₆)))`, which `hkey` shows    -- equals `IsSquare (φc₆²)`.    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]))    have hc₄0 : residue R (E.integralModel R).c₄ ≠ 0 := residue_integralModel_c₄_ne_zero E R    have : NeZero (2 : ResidueField R) := ⟨h2⟩    rw [nodePoly_quadraticTwistOf_map_splits_iff (algebraMap R (ResidueField R))      (E.integralModel R) t' n' (by rw [ResidueField.algebraMap_eq]; exact hc₄0)      (by rw [ResidueField.algebraMap_eq]; exact hDne)]    refine ⟨residue R (E.integralModel R).c₆, ?_⟩    apply mul_left_cancel₀ hc₄0    rw [ResidueField.algebraMap_eq]    simp only [map_mul, map_neg]    linear_combination      (-(residue R (E.integralModel R).c₄ * residue R (E.integralModel R).c₆)) * hkey  · exact nodePoly_quadraticTwistOf_map_splits_of_residue_of_two_eq_zero E R t' n' h2 hA hB