no goals
𝕜 : Type u_2
E : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f✝ : 𝕜 → E
a✝ b✝ : 𝕜
s : Set 𝕜
f : 𝕜 → E
a b : 𝕜
⊢ (b - a) • dslope f a b = f b - f a
rcases eq_or_ne b a with (rfl | hne) <;> simp [dslope_of_ne, *]