no goals
k : Type u_1
E : Type u_2
PE : Type ?u.20418
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → E
a b : k
h : a ≠ b
⊢ slope (fun x => (x - a) • f x) a b = f b
simp [slope, inv_smul_smul₀ (sub_ne_zero.2 h.symm)]