no goals
R : Type u_3
V : Type u_2
V' : Type ?u.17515
P : Type u_1
P' : Type ?u.17521
inst✝⁷ : Ring R
inst✝⁶ : Invertible 2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x✝ y✝ z x y : P
⊢ ↑(pointReflection (midpoint R x y)) x = y
rw [midpoint, pointReflection_apply, lineMap_apply, vadd_vsub, vadd_vadd, ← add_smul, ← two_mul,
  mul_invOf_self, one_smul, vsub_vadd]