From e2f74e842866e2a590b1cc314bbfbf4394b746e5 Mon Sep 17 00:00:00 2001
From: GuiBrandt <gui.g.brandt@gmail.com>
Date: Fri, 20 Sep 2024 17:47:42 -0300
Subject: [PATCH] Refactor mem_computeProjection

---
 .../Polyhedron/Projection.lean                | 306 +++++++++---------
 1 file changed, 156 insertions(+), 150 deletions(-)

diff --git a/PolyhedralCombinatorics/Polyhedron/Projection.lean b/PolyhedralCombinatorics/Polyhedron/Projection.lean
index 83321be..02a2596 100644
--- a/PolyhedralCombinatorics/Polyhedron/Projection.lean
+++ b/PolyhedralCombinatorics/Polyhedron/Projection.lean
@@ -37,11 +37,11 @@ theorem projection_concat_comm {P Q : LinearSystem 𝔽 n} {c}
   unfold projection
   simp_rw [concat_solutions, Set.inter_comm]
 
-@[simp] lemma mem_projection {P : LinearSystem 𝔽 n}
+@[simp low] lemma mem_projection {P : LinearSystem 𝔽 n}
   : x ∈ P.projection c ↔ ∃ α : 𝔽, x + α • c ∈ P.solutions := Set.mem_setOf
 
 @[simp]
-lemma projection_semiSpace_orthogonal (a : Fin n → 𝔽) (b : 𝔽) (c : Fin n → 𝔽) (h : a ⬝ᵥ c = 0)
+lemma proj_semiSpace_orthogonal {a : Fin n → 𝔽} {b : 𝔽} {c : Fin n → 𝔽} (h : a ⬝ᵥ c = 0)
   : projection (semiSpace a b) c = (semiSpace a b).solutions := by
   simp_rw [projection, Set.ext_iff, Set.mem_setOf, mem_semiSpace]
   intro x
@@ -54,7 +54,7 @@ lemma projection_semiSpace_orthogonal (a : Fin n → 𝔽) (b : 𝔽) (c : Fin n
     simp [h]
 
 @[simp]
-lemma projection_semiSpace_nonorthogonal (a : Fin n → 𝔽) (b : 𝔽) (c : Fin n → 𝔽) (h : a ⬝ᵥ c ≠ 0)
+lemma proj_semiSpace_nonorthogonal {a : Fin n → 𝔽} {b : 𝔽} {c : Fin n → 𝔽} (h : a ⬝ᵥ c ≠ 0)
   : projection (semiSpace a b) c = Set.univ := by
   simp_rw [projection, mem_semiSpace, Set.eq_univ_iff_forall, Set.mem_setOf]
   intro x
@@ -64,7 +64,7 @@ lemma projection_semiSpace_nonorthogonal (a : Fin n → 𝔽) (b : 𝔽) (c : Fi
   rfl
 
 @[simp] theorem proj_concat_semiSpace_orthogonal
-  (a₁ a₂ : Fin n → 𝔽) (b₁ b₂ : 𝔽) (c : Fin n → 𝔽)
+  {a₁ a₂ : Fin n → 𝔽} {b₁ b₂ : 𝔽} {c : Fin n → 𝔽}
   (h₁ : a₁ ⬝ᵥ c = 0) (h₂ : a₂ ⬝ᵥ c = 0)
   : let H₁ := semiSpace a₁ b₁
     let H₂ := semiSpace a₂ b₂
@@ -74,7 +74,7 @@ lemma projection_semiSpace_nonorthogonal (a : Fin n → 𝔽) (b : 𝔽) (c : Fi
     h₁, h₂, smul_zero, add_zero, exists_const]
 
 @[simp] theorem proj_concat_semiSpace_orthogonal_left
-  (a₁ a₂ : Fin n → 𝔽) (b₁ b₂ : 𝔽) (c : Fin n → 𝔽)
+  {a₁ a₂ : Fin n → 𝔽} {b₁ b₂ : 𝔽} {c : Fin n → 𝔽}
   (h₁ : a₁ ⬝ᵥ c = 0) (h₂ : a₂ ⬝ᵥ c ≠ 0)
   : let H₁ := semiSpace a₁ b₁
     let H₂ := semiSpace a₂ b₂
@@ -88,17 +88,17 @@ lemma projection_semiSpace_nonorthogonal (a : Fin n → 𝔽) (b : 𝔽) (c : Fi
   rfl
 
 @[simp] theorem proj_concat_semiSpace_orthogonal_right
-  (a₁ a₂ : Fin n → 𝔽) (b₁ b₂ : 𝔽) (c : Fin n → 𝔽)
+  {a₁ a₂ : Fin n → 𝔽} {b₁ b₂ : 𝔽} {c : Fin n → 𝔽}
   (h₁ : a₁ ⬝ᵥ c ≠ 0) (h₂ : a₂ ⬝ᵥ c = 0)
   : let H₁ := semiSpace a₁ b₁
     let H₂ := semiSpace a₂ b₂
     projection (H₁ ++ H₂) c = H₂.solutions := by
   extract_lets H₁ H₂
   rw [projection_concat_comm]
-  exact proj_concat_semiSpace_orthogonal_left _ _ b₂ b₁ _ h₂ h₁
+  exact proj_concat_semiSpace_orthogonal_left (b₁ := b₂) (b₂ := b₁) h₂ h₁
 
 @[simp] theorem proj_concat_semiSpace_nonorthogonal_pos
-  (a₁ a₂ : Fin n → 𝔽) (b₁ b₂ : 𝔽) (c : Fin n → 𝔽)
+  {a₁ a₂ : Fin n → 𝔽} {b₁ b₂ : 𝔽} {c : Fin n → 𝔽}
   (h₁ : 0 < a₁ ⬝ᵥ c) (h₂ : 0 < a₂ ⬝ᵥ c)
   : let H₁ := semiSpace a₁ b₁
     let H₂ := semiSpace a₂ b₂
@@ -125,7 +125,7 @@ lemma projection_semiSpace_nonorthogonal (a : Fin n → 𝔽) (b : 𝔽) (c : Fi
         simp_rw [r, div_mul_cancel₀ _ h₂.ne.symm, add_sub_cancel]
 
 @[simp] theorem proj_concat_semiSpace_nonorthogonal_neg
-  (a₁ a₂ : Fin n → 𝔽) (b₁ b₂ : 𝔽) (c : Fin n → 𝔽)
+  {a₁ a₂ : Fin n → 𝔽} {b₁ b₂ : 𝔽} {c : Fin n → 𝔽}
   (h₁ : a₁ ⬝ᵥ c < 0) (h₂ : a₂ ⬝ᵥ c < 0)
   : let H₁ := semiSpace a₁ b₁
     let H₂ := semiSpace a₂ b₂
@@ -135,7 +135,7 @@ lemma projection_semiSpace_nonorthogonal (a : Fin n → 𝔽) (b : 𝔽) (c : Fi
   apply proj_concat_semiSpace_nonorthogonal_pos <;> simp_all
 
 @[simp] theorem proj_concat_semiSpace_nonorthogonal_neg_pos
-  (a₁ a₂ : Fin n → 𝔽) (b₁ b₂ : 𝔽) (c : Fin n → 𝔽)
+  {a₁ a₂ : Fin n → 𝔽} {b₁ b₂ : 𝔽} {c : Fin n → 𝔽}
   (h₁ : a₁ ⬝ᵥ c < 0) (h₂ : 0 < a₂ ⬝ᵥ c)
   : let H₁ := semiSpace a₁ b₁
     let H₂ := semiSpace a₂ b₂
@@ -171,7 +171,7 @@ lemma projection_semiSpace_nonorthogonal (a : Fin n → 𝔽) (b : 𝔽) (c : Fi
     . simp [div_mul_cancel₀ _ h₂.ne.symm]
 
 @[simp] theorem proj_concat_semiSpace_nonorthogonal_pos_neg
-  (a₁ a₂ : Fin n → 𝔽) (b₁ b₂ : 𝔽) (c : Fin n → 𝔽)
+  {a₁ a₂ : Fin n → 𝔽} {b₁ b₂ : 𝔽} {c : Fin n → 𝔽}
   (h₁ : 0 < a₁ ⬝ᵥ c) (h₂ : a₂ ⬝ᵥ c < 0)
   : let H₁ := semiSpace a₁ b₁
     let H₂ := semiSpace a₂ b₂
@@ -200,8 +200,106 @@ lemma projection_inter_pairs (S : LinearSystem 𝔽 n) (c : Fin n → 𝔽) {x}
     apply (S.mem_solutions_iff_inter_pairs (x + α • c)).mp h
   . intro h
     simp_rw [mem_projection] at h ⊢
-    simp_rw [S.mem_solutions_iff_inter_pairs]
-    sorry
+    let N : Finset (Fin S.m) := {i | S.mat i ⬝ᵥ c < 0}
+    let Z : Finset (Fin S.m) := {i | S.mat i ⬝ᵥ c = 0}
+    let P : Finset (Fin S.m) := {i | S.mat i ⬝ᵥ c > 0}
+    let Λ : Fin S.m → 𝔽 := fun i ↦ (S.vec i - S.mat i ⬝ᵥ x) / (S.mat i ⬝ᵥ c)
+    let L := (N.image Λ).max
+    let U := (P.image Λ).min
+    have ⟨α, hl, hu⟩ : ∃ α : 𝔽, L ≤ α ∧ α ≤ U := by
+      match hL : L, hU : U with
+      | ⊥, ⊤ => exact ⟨0, bot_le, le_top⟩
+      | ⊥, .some u => exact ⟨u, bot_le, le_rfl⟩
+      | .some l, ⊤ => exact ⟨l, le_rfl, le_top⟩
+      | .some l, .some u =>
+        have hN : N.Nonempty := Finset.image_nonempty.mp ⟨l, Finset.mem_of_max hL⟩
+        have hP : P.Nonempty := Finset.image_nonempty.mp ⟨u, Finset.mem_of_min hU⟩
+        unfold_let L U at hL hU
+        let ⟨i, hi₁, hi₂⟩ := Finset.mem_image.mp $ Finset.mem_of_max hL
+        let ⟨j, hj₁, hj₂⟩ := Finset.mem_image.mp $ Finset.mem_of_min hU
+        simp_rw [N, P, mem_filter_univ] at hi₁ hj₁
+        subst l u
+        replace ⟨α, h⟩ := h i j
+        simp_rw [mem_concat, mem_semiSpace] at h
+        simp only [WithBot.coe_le_coe, WithTop.coe_le_coe]
+        exists α
+        constructor <;> by_contra hc <;> rw [not_le] at hc
+        . replace h := h.1
+          simp_rw [dotProduct_add, dotProduct_smul] at h
+          have : S.mat i ⬝ᵥ x + α • (S.mat i ⬝ᵥ c) > S.vec i := calc
+            _ > _ + Λ i • _ := by
+              apply add_lt_add_left
+              exact mul_lt_mul_of_neg_right hc hi₁
+            _ = _ := by simp_rw [Λ, smul_eq_mul, div_mul_cancel₀ _ hi₁.ne, add_sub_cancel]
+          linarith
+        . replace h := h.2
+          simp_rw [dotProduct_add, dotProduct_smul] at h
+          have : S.mat j ⬝ᵥ x + α • (S.mat j ⬝ᵥ c) > S.vec j := calc
+            _ > _ + Λ j • _ := by
+              apply add_lt_add_left
+              exact mul_lt_mul_of_pos_right hc hj₁
+            _ = _ := by simp_rw [Λ, smul_eq_mul, div_mul_cancel₀ _ hj₁.ne', add_sub_cancel]
+          linarith
+    exists α
+    rw [mem_solutions, Pi.le_def, mulVec_add, mulVec_smul]
+    intro i
+    rw [Pi.add_apply, Pi.smul_apply]
+    change S.mat i ⬝ᵥ x + α * S.mat i ⬝ᵥ c ≤ S.vec i
+    rcases lt_trichotomy (S.mat i ⬝ᵥ c) 0 with neg | zero | pos
+    . have mem_N : i ∈ N := mem_filter_univ.mpr neg
+      have : N.Nonempty := ⟨_, mem_N⟩
+      simp only [Finset.max_le_iff, mem_image, WithBot.coe_le_coe, forall_exists_index, and_imp,
+        forall_apply_eq_imp_iff₂, L] at hl
+      rw [add_comm, ←le_sub_iff_add_le, ←div_le_iff_of_neg neg]
+      exact hl _ mem_N
+    . rw [zero, mul_zero, add_zero]
+      have : i ∈ Z := mem_filter_univ.mpr zero
+      have ⟨α', hα'⟩ := h i i
+      rw [mem_concat, and_self, mem_semiSpace, dotProduct_add, dotProduct_smul, zero, smul_zero,
+        add_zero] at hα'
+      assumption
+    . have mem_P : i ∈ P := mem_filter_univ.mpr pos
+      have : P.Nonempty := ⟨_, mem_P⟩
+      simp only [Finset.le_min_iff, mem_image, WithTop.coe_le_coe, forall_exists_index, and_imp,
+        forall_apply_eq_imp_iff₂, U] at hu
+      rw [add_comm, ←le_sub_iff_add_le, ←le_div_iff₀ pos]
+      exact hu _ mem_P
+
+lemma projection_inter_pairs' (S : LinearSystem 𝔽 n) (c : Fin n → 𝔽) {x}
+  : x ∈ S.projection c ↔
+    (∀ i, S.mat i ⬝ᵥ c = 0 → x ∈ (S.ith_semiSpace i).solutions)
+    ∧ (∀ i j, S.mat i ⬝ᵥ c < 0 → S.mat j ⬝ᵥ c > 0 →
+        x ∈ (S.ith_semiSpace i ++ S.ith_semiSpace j).projection c) := by
+    apply (S.projection_inter_pairs c).trans
+    constructor
+    . intro h
+      constructor
+      . intro i hi
+        have := h i i
+        rw [proj_concat_semiSpace_orthogonal hi hi, mem_concat, and_self] at this
+        exact this
+      . intro i j _ _
+        apply h
+    . intro ⟨hz, hnp⟩ i j
+      rcases lt_trichotomy (S.mat i ⬝ᵥ c) 0 with neg₁ | zero₁ | pos₁
+      <;> rcases lt_trichotomy (S.mat j ⬝ᵥ c) 0 with neg₂ | zero₂ | pos₂
+      . rw [proj_concat_semiSpace_nonorthogonal_neg]
+        repeat trivial
+      . rw [proj_concat_semiSpace_orthogonal_right neg₁.ne zero₂]
+        apply hz j zero₂
+      . exact hnp i j neg₁ pos₂
+      . rw [proj_concat_semiSpace_orthogonal_left zero₁ neg₂.ne]
+        apply hz i zero₁
+      . rw [proj_concat_semiSpace_orthogonal zero₁ zero₂, mem_concat]
+        exact ⟨hz i zero₁, hz j zero₂⟩
+      . rw [proj_concat_semiSpace_orthogonal_left zero₁ pos₂.ne']
+        apply hz i zero₁
+      . rw [projection_concat_comm]
+        exact hnp j i neg₂ pos₁
+      . rw [proj_concat_semiSpace_orthogonal_right pos₁.ne' zero₂]
+        apply hz j zero₂
+      . rw [proj_concat_semiSpace_nonorthogonal_pos]
+        repeat trivial
 
 def computeProjection (S : LinearSystem 𝔽 n) (c : Fin n → 𝔽) : LinearSystem 𝔽 n :=
   let N : Finset (Fin S.m) := {i | S.mat i ⬝ᵥ c < 0}
@@ -220,141 +318,49 @@ def computeProjection (S : LinearSystem 𝔽 n) (c : Fin n → 𝔽) : LinearSys
     | .inr (s, t) => (S.mat t ⬝ᵥ c) • S.vec s - (S.mat s ⬝ᵥ c) • S.vec t
   of D d
 
-lemma mem_computeProjection {S : LinearSystem 𝔽 n} {c} {x}
-  : x ∈ (computeProjection S c).solutions ↔ ∃ α : 𝔽, x + α • c ∈ S.solutions := by
+@[simp] theorem mem_computeProjection {S : LinearSystem 𝔽 n} {c} {x}
+  : x ∈ (computeProjection S c).solutions ↔ x ∈ S.projection c := by
   let A := S.mat
   let b := S.vec
   unfold computeProjection
   lift_lets
-  extract_lets N Z P R r p D d
-  have lemma_0 : x ∈ (of D d).solutions ↔ ∀ (i : Fin r), match p i with
-    | .inl i => A i ⬝ᵥ x ≤ b i
-    | .inr (s, t) => ((A t ⬝ᵥ c) • A s - (A s ⬝ᵥ c) • A t) ⬝ᵥ x ≤ (A t ⬝ᵥ c) • b s - (A s ⬝ᵥ c) • b t
-    := by
-    simp_rw [mem_solutions]
-    show (∀ (i : Fin r), D i ⬝ᵥ x ≤ d i) ↔ _
-    apply forall_congr'
-    intro i
-    rcases hi : p i with s | ⟨s, t⟩ <;> simp only
-    . have : D i = A s := by simp_all only [D, funext_iff, of_apply, implies_true]
-      have : d i = b s := by simp_all only [d]
-      simp_all only
-    . have : D i = ((A t ⬝ᵥ c) • A s - (A s ⬝ᵥ c) • A t) := by simp_all only [D, funext_iff, of_apply, implies_true]
-      have : d i = (A t ⬝ᵥ c) • b s - (A s ⬝ᵥ c) • b t := by simp_all only [d]
-      simp_all only
-  constructor <;> intro h
-  . let Λ : Fin S.m → 𝔽 := fun i ↦ (b i - A i ⬝ᵥ x) / (A i ⬝ᵥ c)
-    let L := (N.image Λ).max
-    let U := (P.image Λ).min
-    have lemma_1 (h : x ∈ (of D d).solutions) (α : 𝔽) (hl : L ≤ α) (hu : α ≤ U)
-      : x + α • c ∈ S.solutions := by
-      rw [lemma_0] at h
-      rw [mem_solutions, Pi.le_def, mulVec_add, mulVec_smul]
-      intro i
-      rw [Pi.add_apply, Pi.smul_apply]
-      change A i ⬝ᵥ x + α * A i ⬝ᵥ c ≤ b i
-      rcases lt_trichotomy (A i ⬝ᵥ c) 0 with neg | zero | pos
-      . have mem_N : i ∈ N := mem_filter_univ.mpr neg
-        have : N.Nonempty := ⟨_, mem_N⟩
-        simp only [Finset.max_le_iff, mem_image, WithBot.coe_le_coe, forall_exists_index, and_imp,
-          forall_apply_eq_imp_iff₂, L] at hl
-        rw [add_comm, ←le_sub_iff_add_le, ←div_le_iff_of_neg neg]
-        exact hl _ mem_N
-      . rw [zero, mul_zero, add_zero]
-        have : i ∈ Z := mem_filter_univ.mpr zero
-        apply p.apply_symm_apply _ ▸ h (p.symm $ Sum.inl ⟨_, this⟩)
-      . have mem_P : i ∈ P := mem_filter_univ.mpr pos
-        have : P.Nonempty := ⟨_, mem_P⟩
-        simp only [Finset.le_min_iff, mem_image, WithTop.coe_le_coe, forall_exists_index, and_imp,
-          forall_apply_eq_imp_iff₂, U] at hu
-        rw [add_comm, ←le_sub_iff_add_le, ←le_div_iff₀ pos]
-        exact hu _ mem_P
-    suffices h' : ∃ α : 𝔽, L ≤ α ∧ α ≤ U by
-      obtain ⟨α, hl, hu⟩ := h'
-      exact ⟨_, lemma_1 h α hl hu⟩
-    match hL : L, hU : U with
-    | ⊥, ⊤ => exact ⟨0, bot_le, le_top⟩
-    | ⊥, .some u => exact ⟨u, bot_le, le_rfl⟩
-    | .some l, ⊤ => exact ⟨l, le_rfl, le_top⟩
-    | .some l, .some u =>
-      have : l ≤ u := by
-        unfold_let L U at hL hU
-        suffices ∀ x ∈ N.image Λ, ∀ y ∈ P.image Λ, x ≤ y from
-          this _ (Finset.mem_of_max hL) _ (Finset.mem_of_min hU)
-        intro _ x_mem _ y_mem
-        simp_rw [mem_image] at x_mem y_mem
-        obtain ⟨_, mem_N, hi⟩ := x_mem
-        obtain ⟨_, mem_P, hj⟩ := y_mem
-        let k : Fin r := p.symm (.inr (⟨_, mem_N⟩, ⟨_, mem_P⟩))
-        simp_rw [N, P, mem_filter_univ] at mem_N mem_P
-        subst hi hj
-        have := lemma_0.mp h k
-        simp_rw [k, p.apply_symm_apply, sub_dotProduct, smul_dotProduct, smul_eq_mul] at this
-        simp_rw [Λ, div_le_iff_of_neg mem_N, mul_comm, ←mul_div_assoc, div_le_iff₀ mem_P, sub_mul,
-          mul_sub, sub_le_iff_le_add, sub_add_comm, ←sub_le_iff_le_add]
-        conv => rw [←neg_le_neg_iff]; simp only [neg_sub]; congr <;> rw [mul_comm]
-        exact this
-      exists l
-      simp [this]
-  . obtain ⟨α, h⟩ := h
-    simp_rw [mem_solutions, Pi.le_def] at h
-    rw [lemma_0]
-    intro i
-    split
-    . rename_i z _
-      obtain ⟨z, hz⟩ := z
-      simp_rw [Z, mem_filter_univ] at hz
-      have := h z
-      simp_rw [mulVec_add, mulVec_smul, Pi.add_apply, Pi.smul_apply] at this
-      change A z ⬝ᵥ x + α * (A z ⬝ᵥ c) ≤ b z at this
-      rw [hz, mul_zero, add_zero] at this
+  extract_lets _ _ _ _ r p D d
+  rw [projection_inter_pairs']
+  show (∀ (i : Fin r), D i ⬝ᵥ x ≤ d i) ↔ _
+  constructor
+  . intro h
+    constructor
+    . intro i hi
+      rw [mem_semiSpace]
+      have := h $ p.symm $ Sum.inl ⟨i, mem_filter_univ.mpr hi⟩
+      simp only [D, d, dotProduct, Matrix.of_apply, OrderIso.apply_symm_apply] at this
+      exact this
+    . intro i j hi hj
+      have := h $ p.symm $ Sum.inr ⟨⟨i, mem_filter_univ.mpr hi⟩, ⟨j, mem_filter_univ.mpr hj⟩⟩
+      simp only [D, d, dotProduct, Matrix.of_apply, OrderIso.apply_symm_apply] at this
+      rw [proj_concat_semiSpace_nonorthogonal_neg_pos hi hj, mem_semiSpace]
+      exact this
+  . intro ⟨hz, hnp⟩ i
+    rcases hi : p i with s | ⟨s, t⟩
+    . have hD : D i = A s := by simp only [D, funext_iff, of_apply, hi, implies_true]
+      have hd : d i = b s := by simp only [d, hi]
+      have hs := Finset.mem_filter_univ.mp s.property
+      replace := hz s hs
+      rw [mem_semiSpace] at this
+      rw [hD, hd]
+      exact this
+    . have hD : D i = ((A t ⬝ᵥ c) • A s - (A s ⬝ᵥ c) • A t) := by simp_all only [D, funext_iff, of_apply, implies_true]
+      have hd : d i = (A t ⬝ᵥ c) • b s - (A s ⬝ᵥ c) • b t := by simp_all only [d]
+      have hs := mem_filter_univ.mp s.property
+      have ht := mem_filter_univ.mp t.property
+      replace := hnp s t hs ht
+      rw [proj_concat_semiSpace_nonorthogonal_neg_pos hs ht, mem_semiSpace] at this
+      rw [hD, hd]
       exact this
-    . rename_i s t _
-      obtain ⟨s, hs⟩ := s
-      obtain ⟨t, ht⟩ := t
-      simp_rw [N, P, mem_filter_univ] at hs ht
-      have : ((A t ⬝ᵥ c) • A s - (A s ⬝ᵥ c) • A t) ⬝ᵥ (α • c) = 0 := by
-        simp_rw [sub_dotProduct, smul_dotProduct, dotProduct_smul, smul_eq_mul]
-        conv =>
-          lhs; congr <;> rw [mul_comm, mul_assoc]
-          . rfl
-          . rhs; rw [mul_comm]
-        apply sub_self
-      rw [←add_zero (_ ⬝ᵥ x), ←this, ←dotProduct_add]
-      simp_rw [sub_dotProduct, smul_dotProduct, smul_eq_mul]
-      apply sub_le_sub
-      . rw [mul_le_mul_left ht]
-        exact h s
-      . rw [mul_le_mul_left_of_neg hs]
-        exact h t
-
--- @[simp] theorem computeProjection_empty {c : Fin n → 𝔽}
---   : computeProjection LinearSystem.empty c = LinearSystem.empty := by
---   unfold computeProjection
---   lift_lets
---   extract_lets _ _ _ R _ D d
---   suffices R.card = 0 by
---     simp_rw [this] at D d
---     simp only [eq_empty_iff, this]
---   rw [card_eq_zero, Finset.eq_empty_iff_forall_not_mem]
---   simp only [empty, IsEmpty.forall_iff]
-
--- @[simp] theorem computeProjection_cons_ortho
---   {a : Fin n → 𝔽} {b : 𝔽} {p : LinearSystem 𝔽 n} {c : Fin n → 𝔽}
---   (h : a ⬝ᵥ c = 0)
---   : computeProjection (cons a b p) c = cons a b (computeProjection p c) := by
---   rw [computeProjection]
---   lift_lets
---   extract_lets N Z P R p D d
---   suffices R.card = 0 by
---     simp_rw [this] at D d
---     simp only [eq_empty_iff, this]
---   rw [card_eq_zero, Finset.eq_empty_iff_forall_not_mem]
---   simp only [empty, IsEmpty.forall_iff]
 
 lemma solutions_computeProjection (S : LinearSystem 𝔽 n) (c : Fin n → 𝔽)
-  : (computeProjection S c).solutions = { x | ∃ α : 𝔽, x + α • c ∈ S.solutions } := by
-  simp_rw [Set.ext_iff, Set.mem_setOf]
+  : (computeProjection S c).solutions = S.projection c := by
+  simp_rw [Set.ext_iff, mem_projection]
   apply mem_computeProjection
 
 end LinearSystem
@@ -379,7 +385,7 @@ open Matrix LinearSystem
 --   : x ∈ P.projection c ↔ ∃ α : 𝔽, x + α • c ∈ P := Set.mem_setOf
 
 -- @[simp]
--- lemma projection_semiSpace_orthogonal (a : Fin n → 𝔽) (b : 𝔽) (c : Fin n → 𝔽) (h : a ⬝ᵥ c = 0)
+-- lemma projection_semiSpace_orthogonal {a : Fin n → 𝔽} {b : 𝔽} {c : Fin n → 𝔽} (h : a ⬝ᵥ c = 0)
 --   : projection (semiSpace a b) c = (semiSpace a b).toSet := by
 --   simp_rw [projection, semiSpace_toSet, mem_semiSpace, Set.ext_iff, Set.mem_setOf]
 --   intro x
@@ -392,7 +398,7 @@ open Matrix LinearSystem
 --     simp [h]
 
 -- @[simp]
--- lemma projection_semiSpace_nonorthogonal (a : Fin n → 𝔽) (b : 𝔽) (c : Fin n → 𝔽) (h : a ⬝ᵥ c ≠ 0)
+-- lemma projection_semiSpace_nonorthogonal {a : Fin n → 𝔽} {b : 𝔽} {c : Fin n → 𝔽} (h : a ⬝ᵥ c ≠ 0)
 --   : projection (semiSpace a b) c = Set.univ := by
 --   simp_rw [projection, mem_semiSpace, Set.eq_univ_iff_forall, Set.mem_setOf]
 --   intro x
@@ -402,7 +408,7 @@ open Matrix LinearSystem
 --   rfl
 
 -- @[simp] theorem proj_inter_semiSpace_orthogonal
---   (a₁ a₂ : Fin n → 𝔽) (b₁ b₂ : 𝔽) (c : Fin n → 𝔽)
+--   {a₁ a₂ : Fin n → 𝔽} {b₁ b₂ : 𝔽} {c : Fin n → 𝔽}
 --   (h₁ : a₁ ⬝ᵥ c = 0) (h₂ : a₂ ⬝ᵥ c = 0)
 --   : let H₁ := semiSpace a₁ b₁
 --     let H₂ := semiSpace a₂ b₂
@@ -411,7 +417,7 @@ open Matrix LinearSystem
 --   simp_all
 
 -- @[simp] theorem proj_inter_semiSpace_orthogonal_left
---   (a₁ a₂ : Fin n → 𝔽) (b₁ b₂ : 𝔽) (c : Fin n → 𝔽)
+--   {a₁ a₂ : Fin n → 𝔽} {b₁ b₂ : 𝔽} {c : Fin n → 𝔽}
 --   (h₁ : a₁ ⬝ᵥ c = 0) (h₂ : a₂ ⬝ᵥ c ≠ 0)
 --   : let H₁ := semiSpace a₁ b₁
 --     let H₂ := semiSpace a₂ b₂
@@ -425,7 +431,7 @@ open Matrix LinearSystem
 --   rfl
 
 -- @[simp] theorem proj_inter_semiSpace_orthogonal_right
---   (a₁ a₂ : Fin n → 𝔽) (b₁ b₂ : 𝔽) (c : Fin n → 𝔽)
+--   {a₁ a₂ : Fin n → 𝔽} {b₁ b₂ : 𝔽} {c : Fin n → 𝔽}
 --   (h₁ : a₁ ⬝ᵥ c ≠ 0) (h₂ : a₂ ⬝ᵥ c = 0)
 --   : let H₁ := semiSpace a₁ b₁
 --     let H₂ := semiSpace a₂ b₂
@@ -435,7 +441,7 @@ open Matrix LinearSystem
 --   apply proj_inter_semiSpace_orthogonal_left _ _ _ _ _ h₂ h₁
 
 -- @[simp] theorem proj_inter_semiSpace_nonorthogonal_pos
---   (a₁ a₂ : Fin n → 𝔽) (b₁ b₂ : 𝔽) (c : Fin n → 𝔽)
+--   {a₁ a₂ : Fin n → 𝔽} {b₁ b₂ : 𝔽} {c : Fin n → 𝔽}
 --   (h₁ : 0 < a₁ ⬝ᵥ c) (h₂ : 0 < a₂ ⬝ᵥ c)
 --   : let H₁ := semiSpace a₁ b₁
 --     let H₂ := semiSpace a₂ b₂
@@ -461,7 +467,7 @@ open Matrix LinearSystem
 --         simp_rw [r, div_mul_cancel₀ _ h₂.ne.symm, add_sub_cancel]
 
 -- @[simp] theorem proj_inter_semiSpace_nonorthogonal_neg
---   (a₁ a₂ : Fin n → 𝔽) (b₁ b₂ : 𝔽) (c : Fin n → 𝔽)
+--   {a₁ a₂ : Fin n → 𝔽} {b₁ b₂ : 𝔽} {c : Fin n → 𝔽}
 --   (h₁ : a₁ ⬝ᵥ c < 0) (h₂ : a₂ ⬝ᵥ c < 0)
 --   : let H₁ := semiSpace a₁ b₁
 --     let H₂ := semiSpace a₂ b₂
@@ -471,7 +477,7 @@ open Matrix LinearSystem
 --   apply proj_inter_semiSpace_nonorthogonal_pos <;> simp_all
 
 -- @[simp] theorem proj_inter_semiSpace_nonorthogonal_neg_pos
---   (a₁ a₂ : Fin n → 𝔽) (b₁ b₂ : 𝔽) (c : Fin n → 𝔽)
+--   {a₁ a₂ : Fin n → 𝔽} {b₁ b₂ : 𝔽} {c : Fin n → 𝔽}
 --   (h₁ : a₁ ⬝ᵥ c < 0) (h₂ : 0 < a₂ ⬝ᵥ c)
 --   : let H₁ := semiSpace a₁ b₁
 --     let H₂ := semiSpace a₂ b₂
@@ -508,7 +514,7 @@ open Matrix LinearSystem
 
 -- @[simp]
 -- theorem proj_inter_semiSpace_nonorthogonal_pos_neg
---   (a₁ a₂ : Fin n → 𝔽) (b₁ b₂ : 𝔽) (c : Fin n → 𝔽)
+--   {a₁ a₂ : Fin n → 𝔽} {b₁ b₂ : 𝔽} {c : Fin n → 𝔽}
 --   (h₁ : 0 < a₁ ⬝ᵥ c) (h₂ : a₂ ⬝ᵥ c < 0)
 --   : let H₁ := semiSpace a₁ b₁
 --     let H₂ := semiSpace a₂ b₂