From 054aa6cbdca97165c441575e81897f4c1012b7c3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 16 Oct 2024 22:13:35 +0000
Subject: [PATCH] feat: `affineSpan k (insert 0 s) = span k s` (#17661)

From LeanCamCombi
---
 .../AffineSpace/AffineSubspace.lean            | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

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