no goals
k : Type u_3
E : Type u_2
PE : Type u_1
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
⊢ (b - a) • slope f a b +ᵥ f a = f b
rw [sub_smul_slope, vsub_vadd]