feat: vectorSpan k (v +ᵥ s) = vectorSpan k s (#21305)

From PFR

Author: YaelDillies

Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean

@@ -90,6 +90,9 @@ theorem vsub_mem_vectorSpan {s : Set P} {p1 p2 : P} (hp1 : p1 ∈ s) (hp2 : p2 
     p1 -ᵥ p2 ∈ vectorSpan k s :=
   vsub_set_subset_vectorSpan k s (vsub_mem_vsub hp1 hp2)
 
+@[simp] lemma vectorSpan_vadd (s : Set P) (v : V) : vectorSpan k (v +ᵥ s) = vectorSpan k s := by
+  simp [vectorSpan]
+
 /-- The points in the affine span of a (possibly empty) set of points. Use `affineSpan` instead to
 get an `AffineSubspace k P`. -/
 def spanPoints (s : Set P) : Set P :=