no goals
R : Type u_2
V : Type u_1
V' : Type ?u.123496
P : Type ?u.123499
P' : Type ?u.123502
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 : P
x y : V
⊢ midpoint R x y = ⅟2 • (x + y)
rw [midpoint_eq_iff, pointReflection_apply, vsub_eq_sub, vadd_eq_add, sub_add_eq_add_sub, ←
  two_smul R, smul_smul, mul_invOf_self, one_smul, add_sub_cancel']