[GOAL]
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
[PROOFSTEP]
rw [one_div, lineMap_inv_two]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Field k
inst✝³ : CharZero k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AddTorsor V P
a b : P
⊢ ↑(homothety a (1 / 2)) b = midpoint k a b
[PROOFSTEP]
rw [one_div, homothety_inv_two]
