no goals
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing R
inst✝³ : CharZero R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
a b : P
⊢ ↑(lineMap a b) (1 / 2) = midpoint R a b
rw [one_div, lineMap_inv_two]