Node Poly quadratic Twist Of map splits iff

lemma nodePoly_quadraticTwistOf_map_splits_iff {A : Type*} [CommRing A] {k : Type*} [Field k]    [NeZero (2 : k)] (φ : A →+* k) (W : WeierstrassCurve A) (t n : A) (hc₄ : φ W.c₄ ≠ 0)    (hD : φ (t ^ 2 - 4 * n) ≠ 0) :    ((W.quadraticTwistOf t n).nodePoly.map φ).Splits      ↔ IsSquare (φ ((t ^ 2 - 4 * n) * -(W.c₄ * W.c₆))) := by  have key : ∀ s y : k, s ≠ 0 → (IsSquare (s ^ 2 * y) ↔ IsSquare y) := fun s y hs ↦    ⟨fun ⟨w, hw⟩ ↦ ⟨w / s, by field_simp; linear_combination hw⟩,      fun ⟨w, hw⟩ ↦ ⟨s * w, by rw [hw]; ring⟩⟩  have hc₄' : φ (W.quadraticTwistOf t n).c₄ ≠ 0 := by    rw [c₄_quadraticTwistOf, map_mul, map_pow]; exact mul_ne_zero (pow_ne_zero 2 hD) hc₄  rw [nodePoly_map_splits_iff_isSquare φ (W.quadraticTwistOf t n) hc₄',    show -((W.quadraticTwistOf t n).c₄ * (W.quadraticTwistOf t n).c₆)        = ((t ^ 2 - 4 * n) ^ 2) ^ 2 * ((t ^ 2 - 4 * n) * -(W.c₄ * W.c₆)) from by      rw [c₄_quadraticTwistOf, c₆_quadraticTwistOf]; ring,    map_mul, map_pow,    key _ _ (show φ ((t ^ 2 - 4 * n) ^ 2) ≠ 0 by rw [map_pow]; exact pow_ne_zero 2 hD)]