diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean
index 70ea2fa947229..4ad30ae06cd1d 100644
--- a/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean
+++ b/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean
@@ -49,6 +49,7 @@ noncomputable section
 open Affine
 
 open Set
+open scoped Pointwise
 
 section
 
@@ -510,6 +511,12 @@ theorem direction_affineSpan (s : Set P) : (affineSpan k s).direction = vectorSp
 theorem mem_affineSpan {p : P} {s : Set P} (hp : p ∈ s) : p ∈ affineSpan k s :=
   mem_spanPoints k p s hp
 
+@[simp]
+lemma vectorSpan_add_self (s : Set V) : (vectorSpan k s : Set V) + s = affineSpan k s := by
+  ext
+  simp [mem_add, spanPoints]
+  aesop
+
 end affineSpan
 
 namespace AffineSubspace
@@ -1284,6 +1291,17 @@ lemma affineSpan_subset_span {s : Set V} :
     (affineSpan k s : Set V) ⊆  Submodule.span k s :=
   affineSpan_le_toAffineSubspace_span
 
+-- TODO: We want this to be simp, but `affineSpan` gets simped away to `spanPoints`!
+-- Let's delete `spanPoints`
+lemma affineSpan_insert_zero (s : Set V) :
+    (affineSpan k (insert 0 s) : Set V) = Submodule.span k s := by
+  rw [← Submodule.span_insert_zero]
+  refine affineSpan_subset_span.antisymm ?_
+  rw [← vectorSpan_add_self, vectorSpan_def]
+  refine Subset.trans ?_ <| subset_add_left _ <| mem_insert ..
+  gcongr
+  exact subset_sub_left <| mem_insert ..
+
 end AffineSpace'
 
 namespace AffineSubspace