rank_le_card_isInSight sorry-free

LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Set.lean

@@ -3,12 +3,27 @@ import Mathlib.Algebra.Group.Pointwise.Set
 open scoped Pointwise
 
 namespace Set
-variable {α β : Type*} [SMul α β]
+variable {α β : Type*}
 
-attribute [gcongr] smul_subset_smul vadd_subset_vadd smul_set_mono vadd_set_mono
+attribute [gcongr] smul_subset_smul vadd_subset_vadd smul_set_mono vadd_set_mono vsub_subset_vsub
+
+section SMul
+variable [SMul α β]
 
 @[to_additive]
 lemma smul_set_insert (a : α) (b : β) (s : Set β) : a • insert b s = insert (a • b) (a • s) :=
   image_insert_eq ..
 
+end SMul
+
+section DivisionMonoid
+variable [DivisionMonoid α] {s t : Set α}
+
+@[to_additive] lemma subset_div_left (ht : 1 ∈ t) : s ⊆ s / t := by
+  rw [div_eq_mul_inv]; exact subset_mul_left _ <| by simpa
+
+@[to_additive] lemma inv_subset_div_right (hs : 1 ∈ s) : t⁻¹ ⊆ s / t := by
+  rw [div_eq_mul_inv]; exact subset_mul_right _ hs
+
+end DivisionMonoid
 end Set

LeanCamCombi/Mathlib/Data/SetLike/Basic.lean

@@ -0,0 +1,6 @@
+import Mathlib.Data.SetLike.Basic
+
+namespace SetLike
+
+@[gcongr] protected alias ⟨_, GCongr.coe_subset_coe⟩ := coe_subset_coe
+@[gcongr] protected alias ⟨_, GCongr.coe_ssubset_coe⟩ := coe_ssubset_coe

LeanCamCombi/Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean

@@ -1,6 +1,7 @@
 import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace
-import Mathlib.LinearAlgebra.AffineSpace.Combination
-import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
+import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set
+import LeanCamCombi.Mathlib.Data.SetLike.Basic
+import LeanCamCombi.Mathlib.LinearAlgebra.Span
 
 /-!
 # TODO
@@ -9,32 +10,21 @@ Kill `spanPoints`
 -/
 
 open Set
+open scoped Pointwise
 
 variable {k V P : Type*} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P]
 
-namespace AffineSubspace
-variable {s : AffineSubspace k P} {x y z : P}
-
-lemma mem_of_collinear (h : Collinear k {x, y, z}) (hx : x ∈ s) (hz : z ∈ s) : y ∈ s := sorry
-
-end AffineSubspace
-
--- TODO: Prove that `SameRay` implies `Collinear`
+@[simp]
+lemma vectorSpan_add_self (s : Set V) : (vectorSpan k s : Set V) + s = affineSpan k s := by
+  ext
+  simp [mem_add, spanPoints]
+  aesop
 
 @[simp] lemma affineSpan_insert_zero (s : Set V) :
     (affineSpan k (insert 0 s) : Set V) = Submodule.span k s := by
-  refine subset_antisymm ?_ ?_
-  · rw [← Submodule.span_insert_zero]
-    exact affineSpan_subset_span
-  let W : Submodule k V :=
-    { carrier := affineSpan k (insert 0 s)
-      add_mem' := fun {x y} hx hy ↦ by
-        sorry
-      zero_mem' := subset_affineSpan _ _ <| mem_insert ..
-      smul_mem' := fun {a x} hx ↦ by
-        simp only [SetLike.mem_coe]
-        refine AffineSubspace.mem_of_collinear ?_ hx <| subset_affineSpan _ _ <| mem_insert ..
-        sorry
-         }
-  change Submodule.span k s ≤ W
-  exact Submodule.span_le.2 fun x hx ↦ subset_affineSpan _ _ <| subset_insert _ _ hx
+  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 ..

LeanCamCombi/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

@@ -0,0 +1,12 @@
+import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
+
+variable {k V P : Type*} [DivisionRing k] [AddCommGroup V] [Module k V] [AddTorsor V P]
+
+namespace AffineSubspace
+variable {s : AffineSubspace k P} {x y z : P}
+
+lemma mem_of_collinear (h : Collinear k {x, y, z}) (hx : x ∈ s) (hz : z ∈ s) : y ∈ s := sorry
+
+end AffineSubspace
+
+-- TODO: Prove that `SameRay` implies `Collinear`