feat: a bit more API around ContinuousAffineEquiv.pointReflection (leanprover-community#40889)

Following its introduction in leanprover-community#40637.

Author: ADedecker

Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

@@ -427,6 +427,7 @@ def vaddConst (b : P₁) : V₁ ≃ᵃ[k] P₁ where
   map_vadd' _ _ := add_vadd _ _ _
 
 /-- `p' ↦ p -ᵥ p'` as an equivalence. -/
+@[simps! linear apply symm_apply]
 def constVSub (p : P₁) : P₁ ≃ᵃ[k] V₁ where
   toEquiv := Equiv.constVSub p
   linear := LinearEquiv.neg k
@@ -514,10 +515,13 @@ This is `Equiv.pointReflection` as an `AffineEquiv`. -/
 def pointReflection (x : P₁) : P₁ ≃ᵃ[k] P₁ :=
   (constVSub k x).trans (vaddConst k x)
 
-@[simp] lemma pointReflection_apply_eq_equivPointReflection_apply (x y : P₁) :
-    pointReflection k x y = Equiv.pointReflection x y :=
+@[simp]
+lemma coe_pointReflection (x y : P₁) : pointReflection k x y = Equiv.pointReflection x y :=
   rfl
 
+@[deprecated (since := "2026-06-22")]
+alias pointReflection_apply_eq_equivPointReflection_apply := coe_pointReflection
+
 theorem pointReflection_apply (x y : P₁) : pointReflection k x y = (x -ᵥ y) +ᵥ x :=
   rfl
 

Mathlib/Topology/Algebra/ContinuousAffineEquiv.lean

@@ -97,18 +97,6 @@ theorem coe_coe (e : P₁ ≃ᴬ[k] P₂) : ⇑(e : P₁ ≃ᵃ[k] P₂) = e :=
 theorem coe_toEquiv (e : P₁ ≃ᴬ[k] P₂) : ⇑e.toEquiv = e :=
   rfl
 
-/-- See Note [custom simps projection].
-  We need to specify this projection explicitly in this case,
-  because it is a composition of multiple projections. -/
-def Simps.apply (e : P₁ ≃ᴬ[k] P₂) : P₁ → P₂ :=
-  e
-
-/-- See Note [custom simps projection]. -/
-def Simps.symm_apply (e : P₁ ≃ᴬ[k] P₂) : P₂ → P₁ :=
-  e.symm
-
-initialize_simps_projections ContinuousAffineEquiv (toFun → apply, invFun → symm_apply)
-
 @[ext]
 theorem ext {e e' : P₁ ≃ᴬ[k] P₂} (h : ∀ x, e x = e' x) : e = e' :=
   DFunLike.ext _ _ h
@@ -178,6 +166,18 @@ def symm (e : P₁ ≃ᴬ[k] P₂) : P₂ ≃ᴬ[k] P₁ where
   continuous_toFun := e.continuous_invFun
   continuous_invFun := e.continuous_toFun
 
+/-- See Note [custom simps projection].
+  We need to specify this projection explicitly in this case,
+  because it is a composition of multiple projections. -/
+def Simps.apply (e : P₁ ≃ᴬ[k] P₂) : P₁ → P₂ :=
+  e
+
+/-- See Note [custom simps projection]. -/
+def Simps.symm_apply (e : P₁ ≃ᴬ[k] P₂) : P₂ → P₁ :=
+  e.symm
+
+initialize_simps_projections ContinuousAffineEquiv (toFun → apply, invFun → symm_apply)
+
 @[simp]
 theorem toAffineEquiv_symm (e : P₁ ≃ᴬ[k] P₂) : e.symm.toAffineEquiv = e.toAffineEquiv.symm :=
   rfl
@@ -312,16 +312,34 @@ section
 variable (k)
 variable [TopologicalSpace V₁] [IsTopologicalAddTorsor P₁]
 
+/-- The affine homeomorphism `V ≃ᴬ[k] P` given by `v ↦ v +ᵥ p`. This is `Equiv.vaddConst`
+as a `ContinuousAffineEquiv`. -/
+@[simps! apply symm_apply]
+def vaddConst (p : P₁) : V₁ ≃ᴬ[k] P₁ where
+  __ := AffineEquiv.vaddConst k p
+  __ := Homeomorph.vaddConst p
+
+@[simp]
+lemma toAffineEquiv_vaddConst {p : P₁} : vaddConst k p = AffineEquiv.vaddConst k p := rfl
+
+/-- The affine homeomorphism given by `p' ↦ p -ᵥ p'`. This is `Equiv.constVSub` as a
+`ContinuousAffineEquiv`. -/
+@[simps! apply symm_apply]
+def constVSub (p : P₁) : P₁ ≃ᴬ[k] V₁ where
+  __ := AffineEquiv.constVSub k p
+  __ := Homeomorph.constVSub p
+
+@[simp]
+lemma toAffineEquiv_constVSub {p : P₁} : constVSub k p = AffineEquiv.constVSub k p := rfl
+
 /-- The affine homeomorphism given by reflection about the point `x`.
 This is `Equiv.pointReflection` as a `ContinuousAffineEquiv`. -/
-@[simps toAffineEquiv]
-def pointReflection (x : P₁) : P₁ ≃ᴬ[k] P₁ where
-  toAffineEquiv := AffineEquiv.pointReflection k x
-  continuous_toFun := by dsimp [Equiv.pointReflection]; fun_prop
-  continuous_invFun := by
-    let : ContinuousNeg V₁ :=
-      IsTopologicalAddTorsor.to_isTopologicalAddGroup (V := V₁) (P := P₁) |>.toContinuousNeg
-    dsimp [Equiv.pointReflection]; fun_prop
+def pointReflection (x : P₁) : P₁ ≃ᴬ[k] P₁ :=
+  (constVSub k x).trans (vaddConst k x)
+
+@[simp]
+lemma coe_pointReflection (x : P₁) :
+    (pointReflection k x : P₁ → P₁) = Equiv.pointReflection x := rfl
 
 theorem pointReflection_apply (x y : P₁) : pointReflection k x y = (x -ᵥ y) +ᵥ x :=
   rfl
@@ -330,6 +348,17 @@ theorem pointReflection_apply (x y : P₁) : pointReflection k x y = (x -ᵥ y)
 theorem pointReflection_symm (x : P₁) : (pointReflection k x).symm = pointReflection k x :=
   toAffineEquiv_injective <| AffineEquiv.pointReflection_symm k x
 
+@[simp]
+theorem toAffineEquiv_pointReflection (x : P₁) :
+    (pointReflection k x).toAffineEquiv = AffineEquiv.pointReflection k x :=
+  rfl
+
+theorem pointReflection_self (x : P₁) : pointReflection k x x = x :=
+  vsub_vadd _ _
+
+theorem pointReflection_involutive (x : P₁) : Involutive (pointReflection k x : P₁ → P₁) :=
+  Equiv.pointReflection_involutive x
+
 end
 
 section