Quadratic Twist Point Equiv map

theorem quadraticTwistPointEquiv_map {N : Type*} [Field N] [Algebra K N] [Algebra L N]    [IsScalarTower K L N] [DecidableEq N] (f : M →ₐ[L] N)    (P : ((E.quadraticTwist L)⁄M).Point) :    E.quadraticTwistPointEquiv L N (Affine.Point.map f P) =      Affine.Point.map f (E.quadraticTwistPointEquiv L M P) := by  -- The base-changed change of variables over `N` is the image under `f` of that over `M`.  have hu : (((E.quadraticTwistVarChange L).baseChange N).u : N)      = f (((E.quadraticTwistVarChange L).baseChange M).u : M) := by    simp only [VariableChange.baseChange, VariableChange.map, Units.coe_map, MonoidHom.coe_coe]    exact (f.commutes _).symm  have hr : ((E.quadraticTwistVarChange L).baseChange N).r      = f ((E.quadraticTwistVarChange L).baseChange M).r := (f.commutes _).symm  have hs : ((E.quadraticTwistVarChange L).baseChange N).s      = f ((E.quadraticTwistVarChange L).baseChange M).s := (f.commutes _).symm  have ht : ((E.quadraticTwistVarChange L).baseChange N).t      = f ((E.quadraticTwistVarChange L).baseChange M).t := (f.commutes _).symm  rcases P with _ | ⟨x, y, h⟩  · simp [← Affine.Point.zero_def]  · simp only [quadraticTwistPointEquiv, AddEquiv.trans_apply, Affine.Point.equivOfEq_some,      Affine.Point.equivVariableChange_some, Affine.Point.map_some]    refine Affine.Point.some_eq_some (E.baseChange N) ?_ ?_    · simp only [map_add, map_mul, map_pow, hu, hr]    · simp only [map_add, map_mul, map_pow, hu, hs, ht]