feat(AffineSpace): toAffineSubspace lemmas

Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean

@@ -44,6 +44,10 @@ topology are defined elsewhere; see `Analysis.Normed.Affine.AddTorsor` and
 
 * https://en.wikipedia.org/wiki/Affine_space
 * https://en.wikipedia.org/wiki/Principal_homogeneous_space
+
+## TODO
+
+* Delete `spanPoints`
 -/
 
 @[expose] public section
@@ -220,6 +224,10 @@ variable {k V : Type*} [Ring k] [AddCommGroup V] [Module k V]
 
 instance : Coe (Submodule k V) (AffineSubspace k V) := ⟨toAffineSubspace⟩
 
+@[simp]
+theorem coe_toAffineSubspace (p : Submodule k V) : (p.toAffineSubspace : Set V) = (p : Set V) :=
+  rfl
+
 @[simp]
 theorem mem_toAffineSubspace {p : Submodule k V} {x : V} :
     x ∈ (p : AffineSubspace k V) ↔ x ∈ p := Iff.rfl
@@ -793,6 +801,10 @@ theorem eq_bot_or_nonempty (Q : AffineSubspace k P) : Q = ⊥ ∨ (Q : Set P).No
   rw [nonempty_iff_ne_bot]
   apply eq_or_ne
 
+@[simp]
+theorem toAffineSubspace_ne_bot (p : Submodule k V) : p.toAffineSubspace ≠ ⊥ :=
+  (AffineSubspace.nonempty_iff_ne_bot _).mp ⟨0, p.zero_mem⟩
+
 instance [Subsingleton P] : IsSimpleOrder (AffineSubspace k P) where
   eq_bot_or_eq_top (s : AffineSubspace k P) := by
     rw [← coe_eq_bot_iff, ← coe_eq_univ_iff]
@@ -1149,15 +1161,19 @@ 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 simp-ed away to `spanPoints`!
--- Let's delete `spanPoints`
+@[simp]
 lemma affineSpan_insert_zero (s : Set V) :
-    (affineSpan k (insert 0 s) : Set V) = Submodule.span k s := by
-  rw [← Submodule.span_insert_zero]
+    affineSpan k (insert 0 s) = Submodule.span k s := by
+  rw [AffineSubspace.ext_iff, ← 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 ..
 
+theorem affineSpan_eq_span_iff_zero_mem {s : Set V} :
+    affineSpan k s = Submodule.span k s ↔ 0 ∈ affineSpan k s := by
+  refine ⟨by simp +contextual, fun h ↦ ?_⟩
+  rw [← affineSpan_insert_eq_affineSpan _ h, affineSpan_insert_zero]
+
 end AffineSpace'

Mathlib/LinearAlgebra/AffineSpace/Dimension.lean

@@ -92,6 +92,15 @@ theorem finDim_eq_finrank (h : s ≠ ⊥) : finDim s = Module.finrank R s.direct
   simp [finDim, dim_eq_rank h]
   norm_cast
 
+@[simp]
+theorem dim_toAffineSubspace (s : Submodule R V) : s.toAffineSubspace.dim = Module.rank R s := by
+  rw [dim_eq_rank (toAffineSubspace_ne_bot _), Submodule.toAffineSubspace_direction]
+
+@[simp]
+theorem finDim_toAffineSubspace (s : Submodule R V) :
+    s.toAffineSubspace.finDim = Module.finrank R s := by
+  rw [finDim_eq_finrank (toAffineSubspace_ne_bot _), Submodule.toAffineSubspace_direction]
+
 @[simp]
 theorem finDim_eq_finrank_of_not_finite [Module.Free R s.direction] [StrongRankCondition R]
     (h : ¬Module.Finite R s.direction) : finDim s = 0 := by