no goals
k : Type u_2
V : Type u_1
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type ?u.358935
p₁ p₂ : P
⊢ vectorSpan k {p₁, p₂} = Submodule.span k {p₁ -ᵥ p₂}
simp_rw [vectorSpan_eq_span_vsub_set_left k (mem_insert p₁ _), image_pair, vsub_self,
  Submodule.span_insert_zero]