Exists quadratic Twist Point Equiv base Change eq iff

theorem exists_quadraticTwistPointEquiv_baseChange_eq_iff [DecidableEq K] [DecidableEq L]    {σ : L ≃ₐ[K] L} (hσ : σ ≠ 1) (P : (E⁄L).Point) :    (∃ Q : ((E.quadraticTwist L)⁄K).Point,        E.quadraticTwistPointEquiv L L (Affine.Point.baseChange K L Q) = P) ↔      Affine.Point.map σ.toAlgHom P = -P := by  constructor  · rintro ⟨Q, rfl⟩    have hfix := Affine.Point.map_baseChange (W' := E.quadraticTwist L) σ.toAlgHom Q    have hc := E.quadraticTwistPointEquiv_conj L hσ (Affine.Point.baseChange K L Q)    rw [hfix] at hc    exact neg_eq_iff_eq_neg.mp hc.symm  · intro hP    have hRfix : Affine.Point.map σ.toAlgHom ((E.quadraticTwistPointEquiv L L).symm P)        = (E.quadraticTwistPointEquiv L L).symm P := by      apply (E.quadraticTwistPointEquiv L L).injective      rw [E.quadraticTwistPointEquiv_conj L hσ, AddEquiv.apply_symm_apply, hP, neg_neg]    obtain ⟨Q, hQ⟩ := exists_baseChange_point_eq_of_map_eq L hσ hRfix    exact ⟨Q, by rw [hQ, AddEquiv.apply_symm_apply]⟩