Quadratic Twist Point Equiv map of not fixed

theorem quadraticTwistPointEquiv_map_of_not_fixed {σ : M ≃ₐ[K] M}    (hσ : ¬ ∀ x : L, σ (algebraMap L M x) = algebraMap L M x)    (P : ((E.quadraticTwist L)⁄M).Point) :    E.quadraticTwistPointEquiv L M (Affine.Point.map σ.toAlgHom P) =      -Affine.Point.map σ.toAlgHom (E.quadraticTwistPointEquiv L M P) := by  have hM := E.quadraticTwistVarChange_baseChange_map L M hσ  have hu : σ.toAlgHom (((E.quadraticTwistVarChange L).baseChange M).u : M)      = -(((E.quadraticTwistVarChange L).baseChange M).u : M) := by    simpa [VariableChange.mul_def, negVariableChange]      using congrArg (fun C ↦ (VariableChange.u C : M)) hM  have hr : σ.toAlgHom ((E.quadraticTwistVarChange L).baseChange M).r      = ((E.quadraticTwistVarChange L).baseChange M).r := by    simpa [VariableChange.mul_def, negVariableChange] using congrArg VariableChange.r hM  have hs : σ.toAlgHom ((E.quadraticTwistVarChange L).baseChange M).s      = -((E.quadraticTwistVarChange L).baseChange M).s - (E.baseChange M).a₁ := by    simpa [VariableChange.mul_def, negVariableChange, sub_eq_add_neg]      using congrArg VariableChange.s hM  have ht : σ.toAlgHom ((E.quadraticTwistVarChange L).baseChange M).t      = -((E.quadraticTwistVarChange L).baseChange M).t        - ((E.quadraticTwistVarChange L).baseChange M).r * (E.baseChange M).a₁        - (E.baseChange M).a₃ := by    simpa [VariableChange.mul_def, negVariableChange, sub_eq_add_neg, mul_neg_one,      (by ring : ((-1 : M)) ^ 3 = -1)] using congrArg VariableChange.t hM  rcases P with _ | ⟨x, y, hns⟩  · simp [← Affine.Point.zero_def]  · simp only [quadraticTwistPointEquiv, AddEquiv.trans_apply, Affine.Point.equivOfEq_some,      Affine.Point.equivVariableChange_some, Affine.Point.map_some, Affine.Point.neg_some]    refine Affine.Point.some_eq_some (E.baseChange M) ?_ ?_    · simp only [map_add, map_mul, map_pow, hu, hr]      ring    · simp only [Affine.negY, map_add, map_mul, map_pow, hu, hr, hs, ht]      ring