From 0b9cc1186a4265ef65fb5b4a024a401af1771779 Mon Sep 17 00:00:00 2001
From: Lei Bichang <leibichang58@ruc.edu.cn>
Date: Fri, 19 Apr 2024 15:00:20 +0800
Subject: [PATCH 01/23] Refine definitions and comments

---
 Coxeter/ForMathlib/ASCShelling.lean           | 39 ++++++++-----------
 .../ForMathlib/AbstractSimplicialComplex.lean |  3 +-
 2 files changed, 18 insertions(+), 24 deletions(-)

diff --git a/Coxeter/ForMathlib/ASCShelling.lean b/Coxeter/ForMathlib/ASCShelling.lean
index aca63313..569e43d7 100644
--- a/Coxeter/ForMathlib/ASCShelling.lean
+++ b/Coxeter/ForMathlib/ASCShelling.lean
@@ -2,44 +2,37 @@
 import Mathlib.Data.Set.Card
 import Coxeter.ForMathlib.AbstractSimplicialComplex
 
-
-
-
 namespace AbstractSimplicialComplex
 variable {V : Type*} --[DecidableEq V]
 
-/-
-Definition: Let F be a pure abstract simplicial complex of rank d+1.
-A shelling of F is an linear ordering l_1, ⋯ , l_m of all (maximal) facets of F such that
- l_i ⊓ (⨆ {j < i}, l_j)  is an abstract simplicial complex pure of rank d.
+/--
+Definition: Let `F` be a pure abstract simplicial complex of rank `d + 1` with finite facets.
+A shelling of `F` is an linear ordering `l₁`, ⋯ , `lₘ` of all (maximal) facets of F such that
+ `lᵢ ⊓ (⨆ {j < i}, lⱼ)`  is an abstract simplicial complex pure of rank `d`.
 -/
+def Shelling {F : AbstractSimplicialComplex V} [hpure : Pure F] {m : ℕ} (l : Fin m ≃ Facets F) := F.rank > 0 ∧
+  ∀ i : Fin m, 1 < i.val → IsPure' ((⨆ j ∈ {j | j < i}, closure {(l j).val}) ⊓ (closure {(l i).val})) (F.rank-1)
 
-def shelling {F : AbstractSimplicialComplex V} [hpure: Pure F] {m : ℕ } (l : Fin m ≃ Facets F) := F.rank > 0 ∧
-  ∀ i : Fin m, 1 < i.val → IsPure' ((⨆ j ∈ {j | j<i}, closure {(l j).val}) ⊓ (closure {(l i).val})) (F.rank-1)
-
-
-/-
-Definition': Let F be a pure abstract simplicial complex of rank d+1.
-A shelling of F is an linear ordering l_1, ⋯ , l_m of all (maximal) facets of F such that
- for any i < k, there exists j < k, such that l_i ∩ l_k ⊆ l_j ∩ l_k and |l_j ∩ l_k| = d.
+/--
+Definition': Let `F` be a pure abstract simplicial complex of rank `d + 1`.
+A shelling of `F` is an linear ordering `l₁`, ⋯ , `lₘ` of all (maximal) facets of `F` such that
+ for any `i < k`, there exists `j < k`, such that `lᵢ ∩ lₖ ⊆ lⱼ ∩ lₖ` and `|lⱼ ∩ lₖ| = d`.
 -/
-def shelling' [DecidableEq V] {F :  AbstractSimplicialComplex V} [hpure:Pure F]  {m : ℕ } (l : Fin m ≃ Facets F) :=
+def Shelling' [DecidableEq V] {F :  AbstractSimplicialComplex V} [hpure : Pure F]  {m : ℕ} (l : Fin m ≃ Facets F) :=
   F.rank > 0 ∧
   ∀ k i : Fin m, i < k → ∃ j : Fin m, j < k ∧
     ((l i).val ∩ (l k).val ⊆ (l j).val ∩ (l k).val) ∧
     ((l j).val ∩ (l k).val).card + 1 = F.rank
 
-
 /- Lemma: The two definitions of shellings are equivalent.
 -/
 lemma shelling_iff_shelling' [DecidableEq V] {F : AbstractSimplicialComplex V}  [hpure: Pure F]    {m : ℕ} (l : Fin m ≃ Facets F) :
-    shelling l ↔ shelling' l := by sorry
+    Shelling l ↔ Shelling' l := by sorry
 
-/- Definition: An abstract simplicial complex F is called shellable, if it admits a shelling.
--/
-def shellable (F : AbstractSimplicialComplex F) [Pure F] := ∃ (m: ℕ) (l : Fin m ≃ Facets F), shelling l
+/-- Definition: An abstract simplicial complex `F` is called shellable, if it admits a shelling. -/
+def Shellable (F : AbstractSimplicialComplex F) [Pure F] := ∃ (m: ℕ) (l : Fin m ≃ Facets F), Shelling l
 
-lemma cone_shellabe_iff [DecidableEq V] {F G : AbstractSimplicialComplex V} {r : ℕ} [Pure F] [Pure G] (x : V)  (hcone: Cone F G x) :
-  shellable F ↔ shellable G  := by sorry
+lemma cone_Shellabe_iff [DecidableEq V] {F G : AbstractSimplicialComplex V} {r : ℕ} [Pure F] [Pure G] (x : V)  (hcone: Cone F G x) :
+  Shellable F ↔ Shellable G  := by sorry
 
 end AbstractSimplicialComplex
diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index 13955e47..6ddf9e69 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -199,7 +199,8 @@ lemma pure_def {F : AbstractSimplicialComplex V} [Pure F] : ∀ s ∈ F.Facets,
 lemma pure_isPure {F : AbstractSimplicialComplex V} [Pure F] : IsPure F := pure_def
 
 /--
-If the size of simplices in F is unbounded, it has rank 0 by definition.
+The rank of an ASC is defined to be the supremum of the cardinals of its faces.
+If the size of simplices in F is unbounded, it has rank `0` by definition.
 
 Remark: We should general be careful with the unbounded case.
 -/

From 4cf3a31d8b81907cdd6d690aa6e692b7737d6b0f Mon Sep 17 00:00:00 2001
From: Lei Bichang <leibichang58@ruc.edu.cn>
Date: Fri, 19 Apr 2024 15:32:08 +0800
Subject: [PATCH 02/23] Change `\in` to `:`

---
 Coxeter/ForMathlib/ASCShelling.lean | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/Coxeter/ForMathlib/ASCShelling.lean b/Coxeter/ForMathlib/ASCShelling.lean
index 569e43d7..400fdec0 100644
--- a/Coxeter/ForMathlib/ASCShelling.lean
+++ b/Coxeter/ForMathlib/ASCShelling.lean
@@ -11,23 +11,30 @@ A shelling of `F` is an linear ordering `l₁`, ⋯ , `lₘ` of all (maximal) fa
  `lᵢ ⊓ (⨆ {j < i}, lⱼ)`  is an abstract simplicial complex pure of rank `d`.
 -/
 def Shelling {F : AbstractSimplicialComplex V} [hpure : Pure F] {m : ℕ} (l : Fin m ≃ Facets F) := F.rank > 0 ∧
-  ∀ i : Fin m, 1 < i.val → IsPure' ((⨆ j ∈ {j | j < i}, closure {(l j).val}) ⊓ (closure {(l i).val})) (F.rank-1)
+  ∀ i : Fin m, 1 < i.val → IsPure' ((⨆ j : {j // j < i}, closure {(l j).val}) ⊓ (closure {(l i).val})) (F.rank - 1)
 
 /--
 Definition': Let `F` be a pure abstract simplicial complex of rank `d + 1`.
 A shelling of `F` is an linear ordering `l₁`, ⋯ , `lₘ` of all (maximal) facets of `F` such that
  for any `i < k`, there exists `j < k`, such that `lᵢ ∩ lₖ ⊆ lⱼ ∩ lₖ` and `|lⱼ ∩ lₖ| = d`.
 -/
-def Shelling' [DecidableEq V] {F :  AbstractSimplicialComplex V} [hpure : Pure F]  {m : ℕ} (l : Fin m ≃ Facets F) :=
+def Shelling' [DecidableEq V] {F :  AbstractSimplicialComplex V} [hpure : Pure F] {m : ℕ} (l : Fin m ≃ Facets F) :=
   F.rank > 0 ∧
   ∀ k i : Fin m, i < k → ∃ j : Fin m, j < k ∧
     ((l i).val ∩ (l k).val ⊆ (l j).val ∩ (l k).val) ∧
     ((l j).val ∩ (l k).val).card + 1 = F.rank
 
-/- Lemma: The two definitions of shellings are equivalent.
+/-- Lemma: The two definitions of shellings are equivalent.
 -/
 lemma shelling_iff_shelling' [DecidableEq V] {F : AbstractSimplicialComplex V}  [hpure: Pure F]    {m : ℕ} (l : Fin m ≃ Facets F) :
-    Shelling l ↔ Shelling' l := by sorry
+    Shelling l ↔ Shelling' l := by
+    constructor
+    · refine fun a ↦ ⟨a.1, ?_⟩
+      intro k i ilek
+      sorry
+    · refine fun a ↦ ⟨a.1, ?_⟩
+      intro i ige1
+      sorry
 
 /-- Definition: An abstract simplicial complex `F` is called shellable, if it admits a shelling. -/
 def Shellable (F : AbstractSimplicialComplex F) [Pure F] := ∃ (m: ℕ) (l : Fin m ≃ Facets F), Shelling l

From bbd50027ce3c2af9e3b2300677d4675e1970af9a Mon Sep 17 00:00:00 2001
From: Lei Bichang <leibichang58@ruc.edu.cn>
Date: Fri, 19 Apr 2024 16:40:34 +0800
Subject: [PATCH 03/23] Statement: closure commuting with inter

---
 Coxeter/ForMathlib/ASCShelling.lean              |  4 ++++
 .../ForMathlib/AbstractSimplicialComplex.lean    | 16 ++++++++++++++--
 2 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/Coxeter/ForMathlib/ASCShelling.lean b/Coxeter/ForMathlib/ASCShelling.lean
index 400fdec0..c0d48f8f 100644
--- a/Coxeter/ForMathlib/ASCShelling.lean
+++ b/Coxeter/ForMathlib/ASCShelling.lean
@@ -31,6 +31,10 @@ lemma shelling_iff_shelling' [DecidableEq V] {F : AbstractSimplicialComplex V}
     constructor
     · refine fun a ↦ ⟨a.1, ?_⟩
       intro k i ilek
+      unfold Shelling at a
+      have kge1 : 1 < k.1 := by
+
+
       sorry
     · refine fun a ↦ ⟨a.1, ?_⟩
       intro i ige1
diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index 6ddf9e69..603d0244 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -275,7 +275,7 @@ def closurePower (s : Set (Finset V)) : AbstractSimplicialComplex V where
       congr
     · exact Finset.isLowerSet_singleton_empty V
 
-theorem closure_union_eq_iSup_closure {ι : Type*} (p : ι → Set (Finset V)) :
+theorem closure_iUnion_eq_iSup_closure {ι : Type*} (p : ι → Set (Finset V)) :
   closure (⋃ i : ι, p i) = ⨆ i : ι, closure (p i) := by
   apply le_antisymm
   · apply sInf_le
@@ -288,13 +288,25 @@ theorem closure_union_eq_iSup_closure {ι : Type*} (p : ι → Set (Finset V)) :
     intro i
     apply closure_mono <| Set.subset_iUnion p i
 
+lemma closure_union_eq_sup_closure {f g : Set (Finset V)} :
+  closure (f ∪ g) = closure f ⊔ closure g := by
+  sorry
+
+theorem closure_iInter_eq_iInf_closure {ι : Type*} (p : ι → Set (Finset V)) :
+  closure (⋂ i : ι, p i) = ⨅ i : ι, closure (p i) := by
+  sorry
+
+lemma closure_inter_eq_inf_closure {f g : Set (Finset V)} :
+  closure (f ∩ g) = closure f ⊔ closure g := by
+  sorry
+
 /--
 Lemma: Let s be a collection of finsets in V. Then the closure of s is just the union of the closure of elements in s.
 
 Remark: So taking closure commuts with taking union.
 -/
 lemma closure_eq_iSup (s : Set (Finset V)) : closure s = ⨆ f : s,  closure {f.1} := by
-  rw [← closure_union_eq_iSup_closure,
+  rw [← closure_iUnion_eq_iSup_closure,
     Set.iUnion_singleton_eq_range, Subtype.range_coe_subtype, Set.setOf_mem_eq]
 
 theorem closure_eq_closurePower (s: Set (Finset V)) : closure s = closurePower s := by

From 429e89184a8f497f34e23357db86bcd538278e18 Mon Sep 17 00:00:00 2001
From: Lulu <140055027+quizas211@users.noreply.github.com>
Date: Fri, 19 Apr 2024 17:47:50 +0800
Subject: [PATCH 04/23] update ASC (#9)

---
 .../ForMathlib/AbstractSimplicialComplex.lean | 53 +++++++++++++------
 1 file changed, 36 insertions(+), 17 deletions(-)

diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index af1ddad4..51f1288b 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -298,8 +298,43 @@ lemma closure_eq_iSup (s : Set (Finset V)) : closure s = ⨆ f : s,  closure {f.
   rw [← closure_union_eq_iSup_closure,
     Set.iUnion_singleton_eq_range, Subtype.range_coe_subtype, Set.setOf_mem_eq]
 
+
 theorem closure_eq_closurePower (s: Set (Finset V)) : closure s = closurePower s := by
-  sorry
+  ext t
+  constructor
+  · intro ts
+    rw[closure] at ts
+    simp at ts
+    unfold closurePower
+    apply ts
+    by_cases h : Nonempty s <;> simp [h]
+    · rw[Set.subset_def]
+      intro x xs
+      simp only [Set.mem_iUnion, Set.mem_setOf_eq, exists_prop]
+      use x
+    · simp at h
+      apply Set.eq_empty_of_forall_not_mem at h
+      intro g hg
+      rw [h] at hg
+      contradiction
+  · intro ts
+    rw[closurePower] at ts
+    by_cases h : Nonempty s <;> simp [h]
+    · simp [closurePower,h] at ts
+      intro K sK
+      obtain ⟨f,fs⟩ := ts
+      rw[Set.subset_def] at sK
+      --have ts : t ∈ s:= by sorry
+      obtain ⟨fs, tf⟩ := fs
+      apply sK at fs
+      exact mem_faces.1 <| K.lower' tf <| fs
+    · simp [closurePower,h] at ts
+      intro K _
+      apply mem_faces.1
+      rw [ts]
+      exact K.empty_mem
+
+
 
 /--
 Lemma: Let F be an ASC. Then the closure of the set of faces is just F.
@@ -320,20 +355,4 @@ lemma closure_le {F : AbstractSimplicialComplex V} (h: s ⊆ F.faces) : closure
   simp only [sInf_def, Set.mem_setOf_eq, Set.mem_iInter, mem_faces, Set.coe_setOf, Subtype.forall] at h2
   exact h2 F h
 
-/--
-Definition: G is a cone over F with cone point x if
-x ∈ G.vertices - F.vertices
-s ∈ F ⇔ s ∪ {x} ∈ G.
--/
-def Cone (F G: AbstractSimplicialComplex V) (x : V) :=
-  x ∈ G.vertices \ F.vertices ∧
-  ∀ s, s ∈ F.faces ↔ s ∪ {x} ∈ G.faces
-
-def isCone (G: AbstractSimplicialComplex V) := ∃ F x, Cone F G x
-
-lemma cons_pure (hc : Cone F G x) (hp : Pure F) : Pure G := by sorry
-
-/- the following lemma is not true -/
--- lemma cons_pure' (hc : isCone G) : Pure G := by sorry
-
 end AbstractSimplicialComplex

From ddf6972f94655706ec4b16fbb6c5b0547950294f Mon Sep 17 00:00:00 2001
From: Lei Bichang <leibichang58@ruc.edu.cn>
Date: Fri, 19 Apr 2024 18:37:01 +0800
Subject: [PATCH 05/23] formulate some lemmas

---
 Coxeter/ForMathlib/ASCShelling.lean           |  9 +++---
 .../ForMathlib/AbstractSimplicialComplex.lean | 31 ++++++++++++-------
 2 files changed, 24 insertions(+), 16 deletions(-)

diff --git a/Coxeter/ForMathlib/ASCShelling.lean b/Coxeter/ForMathlib/ASCShelling.lean
index c0d48f8f..e1124893 100644
--- a/Coxeter/ForMathlib/ASCShelling.lean
+++ b/Coxeter/ForMathlib/ASCShelling.lean
@@ -11,7 +11,7 @@ A shelling of `F` is an linear ordering `l₁`, ⋯ , `lₘ` of all (maximal) fa
  `lᵢ ⊓ (⨆ {j < i}, lⱼ)`  is an abstract simplicial complex pure of rank `d`.
 -/
 def Shelling {F : AbstractSimplicialComplex V} [hpure : Pure F] {m : ℕ} (l : Fin m ≃ Facets F) := F.rank > 0 ∧
-  ∀ i : Fin m, 1 < i.val → IsPure' ((⨆ j : {j // j < i}, closure {(l j).val}) ⊓ (closure {(l i).val})) (F.rank - 1)
+  ∀ i : Fin m, 0 < i.val → IsPure' ((⨆ j : {j // j < i}, closure {(l j).val}) ⊓ (closure {(l i).val})) (F.rank - 1)
 
 /--
 Definition': Let `F` be a pure abstract simplicial complex of rank `d + 1`.
@@ -26,14 +26,15 @@ def Shelling' [DecidableEq V] {F :  AbstractSimplicialComplex V} [hpure : Pure F
 
 /-- Lemma: The two definitions of shellings are equivalent.
 -/
-lemma shelling_iff_shelling' [DecidableEq V] {F : AbstractSimplicialComplex V}  [hpure: Pure F]    {m : ℕ} (l : Fin m ≃ Facets F) :
+lemma shelling_iff_shelling' [DecidableEq V] {F : AbstractSimplicialComplex V}  [hpure: Pure F] {m : ℕ} (l : Fin m ≃ Facets F) :
     Shelling l ↔ Shelling' l := by
     constructor
     · refine fun a ↦ ⟨a.1, ?_⟩
       intro k i ilek
       unfold Shelling at a
-      have kge1 : 1 < k.1 := by
-
+      have : k.val > 0 := by sorry
+      let b := a.2 k this
+      unfold IsPure' at b
 
       sorry
     · refine fun a ↦ ⟨a.1, ?_⟩
diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index ecd63162..f4f64fda 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -110,6 +110,9 @@ where
   inf_le_left := fun _ _ _ ha => ha.1
   __ := completeLatticeOfInf (AbstractSimplicialComplex V) sInf_isGLB
 
+@[simp]
+lemma inf_def (F G : AbstractSimplicialComplex V) : (F ⊓ G).faces = F.faces ∩ G.faces := rfl
+
 def unionSubset {s : Set <| AbstractSimplicialComplex V} (hs : s.Nonempty) : AbstractSimplicialComplex V where
   faces := ⋃ F : s, F.1.faces
   empty_mem := by
@@ -151,7 +154,7 @@ Definition: For any ASC F, we denote by vertices F the set of vertices of F.
 def vertices (F : AbstractSimplicialComplex V) : Set V := ⋃ s : F.faces, s.1.toSet
 
 /--
-Definition: Let F be an ASC. A maximal face of F is called a facet of F.
+Definition: Let `F` be an ASC. A maximal face of F is called a facet of F.
 -/
 def IsFacet (F : AbstractSimplicialComplex V) (s : Finset V) := s ∈ F ∧ ∀ t ∈ F, s ⊆ t → s = t
 
@@ -204,7 +207,6 @@ If the size of simplices in F is unbounded, it has rank `0` by definition.
 
 Remark: We should general be careful with the unbounded case.
 -/
-
 noncomputable def rank (F : AbstractSimplicialComplex V) : ℕ := iSup fun s : F.faces => s.1.card
 
 /-- Definition: For a collection s of subsets of V, we denote by closure s the smallest ASC over V containing all elements in s
@@ -219,6 +221,9 @@ lemma subset_closure_faces (s : Set (Finset V)) : s ⊆ (closure s).faces := by
   simp only [sInf_def, Set.coe_setOf, Set.mem_setOf_eq, Set.subset_iInter_iff, Subtype.forall,
     imp_self, forall_const]
 
+lemma closure_faces_eq_self (F : AbstractSimplicialComplex V) : closure F.faces = F := by
+  sorry
+
 lemma closure_mono {s t: Set (Finset V)} : s ⊆ t → closure s ≤ closure t := by
   intro hst
   apply sInf_le_sInf
@@ -289,20 +294,22 @@ theorem closure_iUnion_eq_iSup_closure {ι : Type*} (p : ι → Set (Finset V))
     intro i
     apply closure_mono <| Set.subset_iUnion p i
 
-lemma closure_union_eq_sup_closure {f g : Set (Finset V)} :
-  closure (f ∪ g) = closure f ⊔ closure g := by
-  sorry
+lemma closure_inter_eq_inf_closure {f g : Set (Finset V)} :
+  closure (f ∩ g) = closure f ⊓ closure g := by
+  apply le_antisymm
+  · apply sInf_le
+    simp [inf_def]
+    constructor <;> exact fun a ha ↦ subset_trans (by simp) ha
+  · simp; intro x hx
+    -- rw [Set.inter_iInter, Set.iInter_inter]
+    -- simp; intro C hC x hx
+    -- obtain ⟨xf, xg⟩ := (Set.mem_inter_iff _ _ _).mp hx
 
-theorem closure_iInter_eq_iInf_closure {ι : Type*} (p : ι → Set (Finset V)) :
-  closure (⋂ i : ι, p i) = ⨅ i : ι, closure (p i) := by
-  sorry
+    sorry
 
-lemma closure_inter_eq_inf_closure {f g : Set (Finset V)} :
-  closure (f ∩ g) = closure f ⊔ closure g := by
-  sorry
 
 /--
-Lemma: Let s be a collection of finsets in V. Then the closure of s is just the union of the closure of elements in s.
+Lemma: Let `s` be a collection of finsets in `V`. Then the closure of `s` is just the union of the closure of elements in `s`.
 
 Remark: So taking closure commuts with taking union.
 -/

From 083a820199c667caa7d289bc6451df624b353ccc Mon Sep 17 00:00:00 2001
From: Lei Bichang <leibichang58@ruc.edu.cn>
Date: Mon, 22 Apr 2024 17:07:26 +0800
Subject: [PATCH 06/23] State many lemmas in ASC and redefine Shelling

Be careful, because I might have made some mistakes
---
 Coxeter/ForMathlib/ASCShelling.lean           | 29 ++++-----
 .../ForMathlib/AbstractSimplicialComplex.lean | 65 ++++++++++++-------
 2 files changed, 55 insertions(+), 39 deletions(-)

diff --git a/Coxeter/ForMathlib/ASCShelling.lean b/Coxeter/ForMathlib/ASCShelling.lean
index e1124893..7375b045 100644
--- a/Coxeter/ForMathlib/ASCShelling.lean
+++ b/Coxeter/ForMathlib/ASCShelling.lean
@@ -11,40 +11,37 @@ A shelling of `F` is an linear ordering `l₁`, ⋯ , `lₘ` of all (maximal) fa
  `lᵢ ⊓ (⨆ {j < i}, lⱼ)`  is an abstract simplicial complex pure of rank `d`.
 -/
 def Shelling {F : AbstractSimplicialComplex V} [hpure : Pure F] {m : ℕ} (l : Fin m ≃ Facets F) := F.rank > 0 ∧
-  ∀ i : Fin m, 0 < i.val → IsPure' ((⨆ j : {j // j < i}, closure {(l j).val}) ⊓ (closure {(l i).val})) (F.rank - 1)
+  ∀ k : Fin m, 0 < k.1 → IsPure' ((⨆ j : {j // j < k}, closure {(l j).1}) ⊓ (closure {(l k).1})) (F.rank - 1)
+
+open Classical
 
 /--
 Definition': Let `F` be a pure abstract simplicial complex of rank `d + 1`.
 A shelling of `F` is an linear ordering `l₁`, ⋯ , `lₘ` of all (maximal) facets of `F` such that
  for any `i < k`, there exists `j < k`, such that `lᵢ ∩ lₖ ⊆ lⱼ ∩ lₖ` and `|lⱼ ∩ lₖ| = d`.
 -/
-def Shelling' [DecidableEq V] {F :  AbstractSimplicialComplex V} [hpure : Pure F] {m : ℕ} (l : Fin m ≃ Facets F) :=
+def Shelling' {F :  AbstractSimplicialComplex V} [hpure : Pure F] {m : ℕ} (l : Fin m ≃ Facets F) :=
   F.rank > 0 ∧
   ∀ k i : Fin m, i < k → ∃ j : Fin m, j < k ∧
-    ((l i).val ∩ (l k).val ⊆ (l j).val ∩ (l k).val) ∧
-    ((l j).val ∩ (l k).val).card + 1 = F.rank
+    (closure {(l i).1} ⊓ closure {(l k).1} ≤ closure {(l j).1} ⊓ closure {(l k).1}) ∧
+    (closure {(l j).1} ⊓ closure {(l k).1}).rank + 1 = F.rank
 
 /-- Lemma: The two definitions of shellings are equivalent.
 -/
-lemma shelling_iff_shelling' [DecidableEq V] {F : AbstractSimplicialComplex V}  [hpure: Pure F] {m : ℕ} (l : Fin m ≃ Facets F) :
+lemma shelling_iff_shelling' {F : AbstractSimplicialComplex V}  [hpure: Pure F] {m : ℕ} (l : Fin m ≃ Facets F) :
     Shelling l ↔ Shelling' l := by
     constructor
-    · refine fun a ↦ ⟨a.1, ?_⟩
-      intro k i ilek
-      unfold Shelling at a
-      have : k.val > 0 := by sorry
-      let b := a.2 k this
-      unfold IsPure' at b
-
-      sorry
-    · refine fun a ↦ ⟨a.1, ?_⟩
-      intro i ige1
+    · sorry
+    · refine fun ⟨a, b⟩ ↦ ⟨a, ?_⟩
+      intro k kge0
+      intro s hs
+      rw [iSup_inf_eq (a := closure {(l k).1})] at hs
       sorry
 
 /-- Definition: An abstract simplicial complex `F` is called shellable, if it admits a shelling. -/
 def Shellable (F : AbstractSimplicialComplex F) [Pure F] := ∃ (m: ℕ) (l : Fin m ≃ Facets F), Shelling l
 
-lemma cone_Shellabe_iff [DecidableEq V] {F G : AbstractSimplicialComplex V} {r : ℕ} [Pure F] [Pure G] (x : V)  (hcone: Cone F G x) :
+lemma cone_Shellabe_iff {F G : AbstractSimplicialComplex V} {r : ℕ} [Pure F] [Pure G] (x : V) (hcone: Cone F G x) :
   Shellable F ↔ Shellable G  := by sorry
 
 end AbstractSimplicialComplex
diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index f7f44da4..753bd2d6 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -66,7 +66,7 @@ instance partialOrder : PartialOrder (AbstractSimplicialComplex V) where
 lemma le_def {G F : AbstractSimplicialComplex V} : G ≤ F ↔ G.faces ⊆ F.faces := by rfl
 
 /--
-Definition: The simplex with verteces s ⊆ V is the complex of all finite subsets of s.
+Definition: The simplex with verteces `s ⊆ V` is the complex of all finite subsets of `s`.
 -/
 def simplex (s : Set V) : AbstractSimplicialComplex V where
   faces := {t | t.toSet ⊆ s}
@@ -94,13 +94,13 @@ lemma sInf_isGLB (s : Set (AbstractSimplicialComplex V)) : IsGLB s (sInf s) := b
     simp only [subset_of_eq]
   . intro x hx
     simp_rw [mem_lowerBounds,le_def] at hx
-    rw [le_def,sInf_def]
+    rw [le_def, sInf_def]
     simp only [Set.subset_iInter_iff, Subtype.coe_prop, hx, Subtype.forall, implies_true, forall_const]
 
 
-/-- instance: The set of all ASCs on V is a complete lattice with intersections and unions of the set of faces.
+/-- instance: The set of all ASCs on `V` is a complete lattice with intersections and unions of the set of faces.
 -/
-instance complete_lattice : CompleteLattice (AbstractSimplicialComplex V)
+instance instCompleteLatticeToAbstractSimplicialComplex : CompleteLattice (AbstractSimplicialComplex V)
 where
   inf := fun F G => ⟨F.faces ∩ G.faces, Set.mem_inter F.empty_mem G.empty_mem, IsLowerSet.inter F.lower' G.lower'⟩
   le_inf := fun _ _ _ hab hac _ ha =>
@@ -111,7 +111,7 @@ where
   __ := completeLatticeOfInf (AbstractSimplicialComplex V) sInf_isGLB
 
 @[simp]
-lemma inf_def (F G : AbstractSimplicialComplex V) : (F ⊓ G).faces = F.faces ∩ G.faces := rfl
+lemma inf_faces (F G : AbstractSimplicialComplex V) : (F ⊓ G).faces = F.faces ∩ G.faces := rfl
 
 def unionSubset {s : Set <| AbstractSimplicialComplex V} (hs : s.Nonempty) : AbstractSimplicialComplex V where
   faces := ⋃ F : s, F.1.faces
@@ -141,6 +141,7 @@ lemma bot_eq_ofEmpty : (⊥ : AbstractSimplicialComplex V) = ofEmpty := by
   rw [eq_bot_iff, le_def, show ofEmpty.faces = {∅} by rfl, Set.singleton_subset_iff]
   apply (⊥ : AbstractSimplicialComplex V).empty_mem
 
+@[simp]
 lemma bot_faces_eq_empty : (⊥ : AbstractSimplicialComplex V).faces = {∅} := by
   rw [bot_eq_ofEmpty]; rfl
 
@@ -148,6 +149,15 @@ lemma bot_faces_eq_empty : (⊥ : AbstractSimplicialComplex V).faces = {∅} :=
 lemma sSup_faces_of_nonempty {s : Set (AbstractSimplicialComplex V)} (h : s.Nonempty) : (sSup s).faces = ⋃ F : s, F.1.faces := by
   rw [sSup_eq_unionSubset h]; rfl
 
+@[simp]
+lemma sup_faces (F G : AbstractSimplicialComplex V) : (F ⊔ G).faces = F.faces ∪ G.faces := by
+  let s : Set (AbstractSimplicialComplex V) := {F, G}
+  rw [show F ⊔ G = sSup s by simp [s], show F.faces ∪ G.faces = ⋃ i : s, i.1.faces by simp [s], sSup_faces_of_nonempty (by simp [s])]
+
+@[simp]
+theorem iSup_faces {ι : Type*} (x : ι → AbstractSimplicialComplex V) : (⨆ i, x i).faces = ⨆ i, (x i).faces := by
+  sorry
+
 /--
 Definition: For any ASC F, we denote by vertices F the set of vertices of F.
 -/
@@ -201,6 +211,9 @@ lemma pure_def {F : AbstractSimplicialComplex V} [Pure F] : ∀ s ∈ F.Facets,
 
 lemma pure_isPure {F : AbstractSimplicialComplex V} [Pure F] : IsPure F := pure_def
 
+theorem isPure_iSup {ι : Type*} {p : ι → AbstractSimplicialComplex V} (hp : ∀i : ι, IsPure (p i)) : IsPure (⨆ i : ι, p i) := by
+  sorry
+
 /--
 The rank of an ASC is defined to be the supremum of the cardinals of its faces.
 If the size of simplices in F is unbounded, it has rank `0` by definition.
@@ -231,7 +244,7 @@ lemma closure_mono {s t: Set (Finset V)} : s ⊆ t → closure s ≤ closure t :
   intro _ h; exact Set.Subset.trans hst h
 
 /--
-Lemma: For a finset f, the closure of {f} is the simplex of f.
+Lemma: For a `f : Finset V`, the closure of `{f}` is the simplex of `f`.
 -/
 lemma closure_simplex (f : Finset V) : closure {f} =  simplex f := by
   have h1 : (closure {f}).faces = (simplex f).faces:= by
@@ -266,7 +279,7 @@ def closureSingleton (f : Finset V) : AbstractSimplicialComplex V where
 def closurePower (s : Set (Finset V)) : AbstractSimplicialComplex V where
   faces :=
     if Nonempty s then
-      ⨆ f : s, {t | t.toSet ⊆ f}
+      ⋃ f : s, {t | t.toSet ⊆ f}
     else
       {∅}
   empty_mem := by
@@ -294,20 +307,6 @@ theorem closure_iUnion_eq_iSup_closure {ι : Type*} (p : ι → Set (Finset V))
     intro i
     apply closure_mono <| Set.subset_iUnion p i
 
-lemma closure_inter_eq_inf_closure {f g : Set (Finset V)} :
-  closure (f ∩ g) = closure f ⊓ closure g := by
-  apply le_antisymm
-  · apply sInf_le
-    simp [inf_def]
-    constructor <;> exact fun a ha ↦ subset_trans (by simp) ha
-  · simp; intro x hx
-    -- rw [Set.inter_iInter, Set.iInter_inter]
-    -- simp; intro C hC x hx
-    -- obtain ⟨xf, xg⟩ := (Set.mem_inter_iff _ _ _).mp hx
-
-    sorry
-
-
 /--
 Lemma: Let `s` be a collection of finsets in `V`. Then the closure of `s` is just the union of the closure of elements in `s`.
 
@@ -343,7 +342,6 @@ theorem closure_eq_closurePower (s: Set (Finset V)) : closure s = closurePower s
       intro K sK
       obtain ⟨f,fs⟩ := ts
       rw[Set.subset_def] at sK
-      --have ts : t ∈ s:= by sorry
       obtain ⟨fs, tf⟩ := fs
       apply sK at fs
       exact mem_faces.1 <| K.lower' tf <| fs
@@ -353,7 +351,7 @@ theorem closure_eq_closurePower (s: Set (Finset V)) : closure s = closurePower s
       rw [ts]
       exact K.empty_mem
 
-
+instance instNonemptyToAbstractSimplicialComplexContainingSet (s : Set (Finset V)) : Nonempty {x : AbstractSimplicialComplex V // s ⊆ x.faces} := ⟨closure s, subset_closure_faces _⟩
 
 /--
 Lemma: Let F be an ASC. Then the closure of the set of faces is just F.
@@ -374,4 +372,25 @@ lemma closure_le {F : AbstractSimplicialComplex V} (h: s ⊆ F.faces) : closure
   simp only [sInf_def, Set.mem_setOf_eq, Set.mem_iInter, mem_faces, Set.coe_setOf, Subtype.forall] at h2
   exact h2 F h
 
+instance instCompleteDistribLatticeToAbstractSimplicialComplex : CompleteDistribLattice (AbstractSimplicialComplex V) := {
+  instCompleteLatticeToAbstractSimplicialComplex with
+  inf_sSup_le_iSup_inf := by
+    intro a s
+    by_cases hs : s.Nonempty
+    · simp [hs, Set.inter_iUnion]
+      intro i is f hf
+      rw [Set.mem_iUnion]
+      use i
+      simp [is, hf]
+    · simp [Set.not_nonempty_iff_eq_empty.mp hs]
+  iInf_sup_le_sup_sInf := by
+    intro a s
+    by_cases hs : s.Nonempty
+    · simp [Set.union_iInter]
+      intro i is f hf
+      sorry
+      -- rw [Set.mem_iInter]
+    · sorry
+}
+
 end AbstractSimplicialComplex

From 4fd4af46cb2a82cf247d4fd43dd1439e6414fab0 Mon Sep 17 00:00:00 2001
From: Lei Bichang <leibichang58@ruc.edu.cn>
Date: Mon, 22 Apr 2024 17:28:45 +0800
Subject: [PATCH 07/23] Add more lemmas

---
 Coxeter/ForMathlib/ASCShelling.lean             |  3 +--
 .../ForMathlib/AbstractSimplicialComplex.lean   | 17 +++++++++++------
 2 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/Coxeter/ForMathlib/ASCShelling.lean b/Coxeter/ForMathlib/ASCShelling.lean
index 7375b045..80f562a2 100644
--- a/Coxeter/ForMathlib/ASCShelling.lean
+++ b/Coxeter/ForMathlib/ASCShelling.lean
@@ -33,8 +33,7 @@ lemma shelling_iff_shelling' {F : AbstractSimplicialComplex V}  [hpure: Pure F]
     constructor
     · sorry
     · refine fun ⟨a, b⟩ ↦ ⟨a, ?_⟩
-      intro k kge0
-      intro s hs
+      intro k kge0 s hs
       rw [iSup_inf_eq (a := closure {(l k).1})] at hs
       sorry
 
diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index 753bd2d6..d08ac1f7 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -154,6 +154,10 @@ lemma sup_faces (F G : AbstractSimplicialComplex V) : (F ⊔ G).faces = F.faces
   let s : Set (AbstractSimplicialComplex V) := {F, G}
   rw [show F ⊔ G = sSup s by simp [s], show F.faces ∪ G.faces = ⋃ i : s, i.1.faces by simp [s], sSup_faces_of_nonempty (by simp [s])]
 
+@[simp]
+theorem iInf_faces {ι : Type*} (x : ι → AbstractSimplicialComplex V) : (⨅ i, x i).faces = ⨅ i, (x i).faces := by --might be wrong
+  sorry
+
 @[simp]
 theorem iSup_faces {ι : Type*} (x : ι → AbstractSimplicialComplex V) : (⨆ i, x i).faces = ⨆ i, (x i).faces := by
   sorry
@@ -294,6 +298,7 @@ def closurePower (s : Set (Finset V)) : AbstractSimplicialComplex V where
       congr
     · exact Finset.isLowerSet_singleton_empty V
 
+/-- Similar statement for `⨅` is not true.-/
 theorem closure_iUnion_eq_iSup_closure {ι : Type*} (p : ι → Set (Finset V)) :
   closure (⋃ i : ι, p i) = ⨆ i : ι, closure (p i) := by
   apply le_antisymm
@@ -385,12 +390,12 @@ instance instCompleteDistribLatticeToAbstractSimplicialComplex : CompleteDistrib
     · simp [Set.not_nonempty_iff_eq_empty.mp hs]
   iInf_sup_le_sup_sInf := by
     intro a s
-    by_cases hs : s.Nonempty
-    · simp [Set.union_iInter]
-      intro i is f hf
-      sorry
-      -- rw [Set.mem_iInter]
-    · sorry
+    simp [Set.union_iInter]
+    intro i is f hf
+    rw [Set.mem_iInter] at hf
+    replace hf := hf i
+    simp [is] at hf
+    simp [hf]
 }
 
 end AbstractSimplicialComplex

From 066428a6369292db8456fa187daf36f0121b6afd Mon Sep 17 00:00:00 2001
From: Clarence Chew <62918570+clarence-chew@users.noreply.github.com>
Date: Tue, 23 Apr 2024 10:30:16 +0800
Subject: [PATCH 08/23] Begin some ASC Shelling propositions

---
 Coxeter/ForMathlib/ASCShellingProps.lean      | 67 +++++++++++++++++++
 .../ForMathlib/AbstractSimplicialComplex.lean |  3 +-
 2 files changed, 68 insertions(+), 2 deletions(-)
 create mode 100644 Coxeter/ForMathlib/ASCShellingProps.lean

diff --git a/Coxeter/ForMathlib/ASCShellingProps.lean b/Coxeter/ForMathlib/ASCShellingProps.lean
new file mode 100644
index 00000000..6f709c4d
--- /dev/null
+++ b/Coxeter/ForMathlib/ASCShellingProps.lean
@@ -0,0 +1,67 @@
+import Mathlib.Data.Set.Card
+import Coxeter.ForMathlib.ASCShelling
+
+namespace ASCShellingProps
+
+open AbstractSimplicialComplex
+open Classical
+
+variable {V : Type*} --[DecidableEq V]
+
+def Deletion (F : AbstractSimplicialComplex V) (x : V) : Set F.faces :=
+  {f | x ∉ f.1 }
+
+def DeletionSimplex (F : AbstractSimplicialComplex V) (x : V) : AbstractSimplicialComplex V where
+  faces := Deletion F x
+  empty_mem := by
+    simp only [Deletion, Set.mem_image, Set.mem_setOf_eq, Subtype.exists, mem_faces,
+      exists_and_left, exists_prop, exists_eq_right_right, Finset.not_mem_empty, not_false_eq_true,
+      true_and]
+    exact F.empty_mem
+  lower' := by
+    simp only [Deletion]
+    intro _ _ hab ha
+    simp only [Set.mem_image, Set.mem_setOf_eq, Subtype.exists, mem_faces, exists_and_left,
+      exists_prop, exists_eq_right_right] at ha ⊢
+    constructor
+    · have := ha.1
+      contrapose! this
+      exact hab this
+    · exact F.lower' hab ha.2
+
+def Link (F : AbstractSimplicialComplex V) (x : V) : Set F.faces :=
+  {f | x ∉ f.1 ∧ {x} ∪ f.1 ∈ F.faces }
+
+def LinkSimplex (F : AbstractSimplicialComplex V) (x : V) (h : {x} ∈ F.faces) : AbstractSimplicialComplex V where
+  faces := Link F x
+  empty_mem := by
+    simp only [Set.mem_image, Subtype.exists, mem_faces, exists_and_right, exists_eq_right, Link]
+    use F.empty_mem
+    simp only [Set.mem_setOf_eq, Finset.not_mem_empty, not_false_eq_true, Finset.union_empty,
+      true_and]
+    exact h
+  lower' := sorry
+
+
+def LinkFace (F : AbstractSimplicialComplex V) (s : F.faces) : Set F.faces :=
+  {f | s.1 ∩ f.1 = ∅ ∧ s.1 ∪ f.1 ∈ F.faces }
+
+def Star (F : AbstractSimplicialComplex V) (s : F.faces) : Set F.faces :=
+  {f | s.1 ∪ f.1 ∈ F.faces }
+
+lemma LinkFace_subset_Star (F : AbstractSimplicialComplex V) (s : F.faces) :
+  LinkFace F s ⊆ Star F s := fun _ h ↦ h.2
+
+
+-- see if we can remove Fintype V
+-- something is off, need to check empty set
+/-def VertexDecomposable [Fintype V] (F : AbstractSimplicialComplex V) (hp : Pure F) : Prop :=
+  (∃ (f : Finset V), F = simplex f) ∨
+  (∃ (x : V), (DeletionSimplex F x).rank = F.rank ∧ VertexDecomposable (DeletionSimplex F x) ∧
+  (LinkSimplex F x).rank + 1 = F.rank)-/
+
+
+-- Page 83: define VertexDecomposable, SheddingVertex
+-- create new file to do property 1, import ASC shelling, merge to master before taking
+
+end ASCShellingProps
diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index 5e9e0bdb..a3970ebf 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -325,8 +325,7 @@ x ∈ G.vertices - F.vertices
 s ∈ F ⇔ s ∪ {x} ∈ G.
 -/
 def Cone (F G: AbstractSimplicialComplex V) (x : V) :=
-  x ∈ G.vertices \ F.vertices ∧
-  ∀ s, s ∈ F.faces ↔ s ∪ {x} ∈ G.faces
+  ¬(x ∈ F.vertices) ∧ ∀ s, s ∈ F.faces ↔ s ∈ G.faces ∧ s ∪ {x} ∈ G.faces
 
 def isCone (G: AbstractSimplicialComplex V) := ∃ F x, Cone F G x
 

From 266fcc37b2c05297be07cfce712d90c73d879ab5 Mon Sep 17 00:00:00 2001
From: Lei Bichang <leibichang58@ruc.edu.cn>
Date: Tue, 23 Apr 2024 13:51:06 +0800
Subject: [PATCH 09/23] Update AbstractSimplicialComplex.lean

---
 .../ForMathlib/AbstractSimplicialComplex.lean | 48 +++++++++++--------
 1 file changed, 27 insertions(+), 21 deletions(-)

diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index d08ac1f7..593eeaab 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -155,16 +155,18 @@ lemma sup_faces (F G : AbstractSimplicialComplex V) : (F ⊔ G).faces = F.faces
   rw [show F ⊔ G = sSup s by simp [s], show F.faces ∪ G.faces = ⋃ i : s, i.1.faces by simp [s], sSup_faces_of_nonempty (by simp [s])]
 
 @[simp]
-theorem iInf_faces {ι : Type*} (x : ι → AbstractSimplicialComplex V) : (⨅ i, x i).faces = ⨅ i, (x i).faces := by --might be wrong
+theorem iInf_faces {ι : Type*} (x : ι → AbstractSimplicialComplex V) : (⨅ i, x i).faces = ⨅ i, (x i).faces := by
   sorry
 
 @[simp]
 theorem iSup_faces {ι : Type*} (x : ι → AbstractSimplicialComplex V) : (⨆ i, x i).faces = ⨆ i, (x i).faces := by
   sorry
 
-/--
-Definition: For any ASC F, we denote by vertices F the set of vertices of F.
--/
+@[simp]
+theorem iSup_faces_of_isEmpty {ι : Type*} [IsEmpty ι] (x : ι → AbstractSimplicialComplex V) : (⨆ i, x i).faces = {∅} := by
+  sorry
+
+/-- Definition: For any ASC `F`, we denote by `vertices F` the set of vertices of F. -/
 def vertices (F : AbstractSimplicialComplex V) : Set V := ⋃ s : F.faces, s.1.toSet
 
 /--
@@ -207,7 +209,7 @@ lemma isPure_iff_isPure' {F : AbstractSimplicialComplex V} : F.IsPure ↔ ∃ d,
       use d
     · intro
       simp only [nonempty_subtype, not_exists] at hemp
-      intro s hs t _
+      intro s hs
       exfalso
       exact hemp s hs
 
@@ -215,7 +217,16 @@ lemma pure_def {F : AbstractSimplicialComplex V} [Pure F] : ∀ s ∈ F.Facets,
 
 lemma pure_isPure {F : AbstractSimplicialComplex V} [Pure F] : IsPure F := pure_def
 
+theorem iSup_Facets_le {ι : Type*} {p : ι → AbstractSimplicialComplex V} : (⨆ i : ι, p i).Facets ≤ ⋃ i : ι, (p i).Facets := by
+  intro a ha
+  rw [Set.mem_iUnion]
+  rcases ha with ⟨ha_mem, ha_max⟩
+  by_cases hi : Nonempty ι
+  · sorry
+  · sorry
+
 theorem isPure_iSup {ι : Type*} {p : ι → AbstractSimplicialComplex V} (hp : ∀i : ι, IsPure (p i)) : IsPure (⨆ i : ι, p i) := by
+  intro s hs t ht
   sorry
 
 /--
@@ -239,7 +250,9 @@ lemma subset_closure_faces (s : Set (Finset V)) : s ⊆ (closure s).faces := by
     imp_self, forall_const]
 
 lemma closure_faces_eq_self (F : AbstractSimplicialComplex V) : closure F.faces = F := by
-  sorry
+  apply le_antisymm
+  · apply sInf_le; simp; rfl
+  · simp
 
 lemma closure_mono {s t: Set (Finset V)} : s ⊆ t → closure s ≤ closure t := by
   intro hst
@@ -247,18 +260,14 @@ lemma closure_mono {s t: Set (Finset V)} : s ⊆ t → closure s ≤ closure t :
   rw [Set.setOf_subset_setOf]
   intro _ h; exact Set.Subset.trans hst h
 
-/--
-Lemma: For a `f : Finset V`, the closure of `{f}` is the simplex of `f`.
--/
+/-- Lemma: For a `f : Finset V`, the closure of `{f}` is the simplex of `f`.-/
 lemma closure_simplex (f : Finset V) : closure {f} =  simplex f := by
   have h1 : (closure {f}).faces = (simplex f).faces:= by
-    apply Set.Subset.antisymm
-    · rw [sInf_def]
-      rintro s h1
+    apply Set.Subset.antisymm <;> rw [sInf_def]
+    · rintro s h1
       simp only [Set.singleton_subset_iff, mem_faces, Set.mem_setOf_eq, Set.mem_iInter, Set.coe_setOf, Subtype.forall] at h1
       exact h1 (simplex ↑f) fun ⦃_⦄ a => a
-    · rw [sInf_def]
-      rintro s h1
+    · rintro s h1
       apply simplex_face.1 at h1
       simp only [Finset.coe_subset] at h1
       simp only [Set.singleton_subset_iff, mem_faces, Set.mem_setOf_eq, Set.mem_iInter, Set.coe_setOf, Subtype.forall]
@@ -292,8 +301,7 @@ def closurePower (s : Set (Finset V)) : AbstractSimplicialComplex V where
   lower' := by
     by_cases h : Nonempty s <;> simp [h]
     · refine isLowerSet_iUnion₂ ?_
-      intro t _
-      intro a b h1 h2
+      intro t _ a b h1 h2
       refine' Set.Subset.trans ?_ h2
       congr
     · exact Finset.isLowerSet_singleton_empty V
@@ -324,9 +332,8 @@ lemma closure_eq_iSup (s : Set (Finset V)) : closure s = ⨆ f : s,  closure {f.
 
 theorem closure_eq_closurePower (s: Set (Finset V)) : closure s = closurePower s := by
   ext t
-  constructor
-  · intro ts
-    rw[closure] at ts
+  constructor <;> intro ts
+  · rw [closure] at ts
     simp at ts
     unfold closurePower
     apply ts
@@ -340,8 +347,7 @@ theorem closure_eq_closurePower (s: Set (Finset V)) : closure s = closurePower s
       intro g hg
       rw [h] at hg
       contradiction
-  · intro ts
-    rw[closurePower] at ts
+  · rw[closurePower] at ts
     by_cases h : Nonempty s <;> simp [h]
     · simp [closurePower,h] at ts
       intro K sK

From da3cd9dd175b4d11c467b21a4a8750834b072333 Mon Sep 17 00:00:00 2001
From: Haotian Liu <98384450+HaotianLiu123@users.noreply.github.com>
Date: Tue, 23 Apr 2024 13:53:30 +0800
Subject: [PATCH 10/23] update ASC (#11)

* update ASC
---
 Coxeter/ForMathlib/AbstractSimplicialComplex.lean | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index d08ac1f7..6d88887c 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -156,11 +156,18 @@ lemma sup_faces (F G : AbstractSimplicialComplex V) : (F ⊔ G).faces = F.faces
 
 @[simp]
 theorem iInf_faces {ι : Type*} (x : ι → AbstractSimplicialComplex V) : (⨅ i, x i).faces = ⨅ i, (x i).faces := by --might be wrong
-  sorry
+  unfold iInf
+  simp only [sInf_def, Set.iInter_coe_set, Set.mem_range, Set.iInter_exists, Set.iInter_iInter_eq',
+    Set.sInf_eq_sInter, Set.sInter_range]
 
 @[simp]
-theorem iSup_faces {ι : Type*} (x : ι → AbstractSimplicialComplex V) : (⨆ i, x i).faces = ⨆ i, (x i).faces := by
-  sorry
+theorem iSup_faces_of_nonempty {ι : Type*} (x : ι → AbstractSimplicialComplex V) [Nonempty ι] : (⨆ i, x i).faces = ⨆ i, (x i).faces := by
+  unfold iSup
+  rw [sSup_faces_of_nonempty]
+  · simp
+  · by_contra h
+    apply Set.not_nonempty_iff_eq_empty.1 at h
+    simp at h
 
 /--
 Definition: For any ASC F, we denote by vertices F the set of vertices of F.

From 82c201e4d54b7f1e5e42709632d463e89154e651 Mon Sep 17 00:00:00 2001
From: Lulu <140055027+quizas211@users.noreply.github.com>
Date: Tue, 23 Apr 2024 13:53:53 +0800
Subject: [PATCH 11/23]  Unify the Of_empty (#10)

* Unify the Of_empty
---
 Coxeter/ForMathlib/ASCShelling.lean           |  4 +-
 .../ForMathlib/AbstractSimplicialComplex.lean | 43 +++++++------------
 2 files changed, 18 insertions(+), 29 deletions(-)

diff --git a/Coxeter/ForMathlib/ASCShelling.lean b/Coxeter/ForMathlib/ASCShelling.lean
index 80f562a2..46a64808 100644
--- a/Coxeter/ForMathlib/ASCShelling.lean
+++ b/Coxeter/ForMathlib/ASCShelling.lean
@@ -40,7 +40,7 @@ lemma shelling_iff_shelling' {F : AbstractSimplicialComplex V}  [hpure: Pure F]
 /-- Definition: An abstract simplicial complex `F` is called shellable, if it admits a shelling. -/
 def Shellable (F : AbstractSimplicialComplex F) [Pure F] := ∃ (m: ℕ) (l : Fin m ≃ Facets F), Shelling l
 
-lemma cone_Shellabe_iff {F G : AbstractSimplicialComplex V} {r : ℕ} [Pure F] [Pure G] (x : V) (hcone: Cone F G x) :
-  Shellable F ↔ Shellable G  := by sorry
+-- lemma cone_Shellabe_iff {F G : AbstractSimplicialComplex V} {r : ℕ} [Pure F] [Pure G] (x : V) (hcone: Cone F G x) :
+--   Shellable F ↔ Shellable G  := by sorry
 
 end AbstractSimplicialComplex
diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index 6d88887c..2ddf3bc7 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -131,19 +131,6 @@ lemma sSup_eq_unionSubset {s : Set <| AbstractSimplicialComplex V} (hs : s.Nonem
   · rw [le_sSup_iff]
     exact fun _ hb ↦ Set.iUnion_subset fun i ↦ hb i.2
 
-def ofEmpty : AbstractSimplicialComplex V where
-  faces := {∅}
-  empty_mem := rfl
-  lower' := Finset.isLowerSet_singleton_empty V
-
-lemma bot_eq_ofEmpty : (⊥ : AbstractSimplicialComplex V) = ofEmpty := by
-  symm
-  rw [eq_bot_iff, le_def, show ofEmpty.faces = {∅} by rfl, Set.singleton_subset_iff]
-  apply (⊥ : AbstractSimplicialComplex V).empty_mem
-
-@[simp]
-lemma bot_faces_eq_empty : (⊥ : AbstractSimplicialComplex V).faces = {∅} := by
-  rw [bot_eq_ofEmpty]; rfl
 
 @[simp]
 lemma sSup_faces_of_nonempty {s : Set (AbstractSimplicialComplex V)} (h : s.Nonempty) : (sSup s).faces = ⋃ F : s, F.1.faces := by
@@ -273,19 +260,6 @@ lemma closure_simplex (f : Finset V) : closure {f} =  simplex f := by
       apply mem_faces.1 <| i.lower' h1 <| mem_faces.2 fi
   exact instSetLikeAbstractSimplicialComplexFinset.proof_1 (closure {f}) (simplex ↑f) h1
 
-def closureSingleton (f : Finset V) : AbstractSimplicialComplex V where
-  faces :=
-    if Nonempty f then
-      {t | t.toSet ⊆ f}
-    else
-      {∅}
-  empty_mem := by
-    by_cases h : Nonempty f <;> simp [h]
-  lower' := by
-    by_cases h : Nonempty f <;> simp [h]
-    · exact antitone_le
-    · exact Finset.isLowerSet_singleton_empty V
-
 /-- Explicit construction of `closure s` for `s : Set (Finset V)`-/
 def closurePower (s : Set (Finset V)) : AbstractSimplicialComplex V where
   faces :=
@@ -328,7 +302,6 @@ lemma closure_eq_iSup (s : Set (Finset V)) : closure s = ⨆ f : s,  closure {f.
   rw [← closure_iUnion_eq_iSup_closure,
     Set.iUnion_singleton_eq_range, Subtype.range_coe_subtype, Set.setOf_mem_eq]
 
-
 theorem closure_eq_closurePower (s: Set (Finset V)) : closure s = closurePower s := by
   ext t
   constructor
@@ -405,4 +378,20 @@ instance instCompleteDistribLatticeToAbstractSimplicialComplex : CompleteDistrib
     simp [hf]
 }
 
+lemma bot_eq_ofEmpty' : (⊥ : AbstractSimplicialComplex V) = closurePower ∅ := by
+  symm
+  rw [eq_bot_iff, le_def, show (closurePower ∅).faces = {∅} by simp[closurePower], Set.singleton_subset_iff]
+  apply (⊥ : AbstractSimplicialComplex V).empty_mem
+
+lemma bot_eq_ofEmpty : (⊥ : AbstractSimplicialComplex V) = closure ∅ := by
+  symm
+  rw[closure_eq_closurePower]
+  rw [eq_bot_iff, le_def, show (closurePower ∅).faces = {∅} by simp[closurePower], Set.singleton_subset_iff]
+  apply (⊥ : AbstractSimplicialComplex V).empty_mem
+
+@[simp]
+lemma bot_faces_eq_empty : (⊥ : AbstractSimplicialComplex V).faces = {∅} := by
+  rw [bot_eq_ofEmpty']
+  simp[closurePower]
+
 end AbstractSimplicialComplex

From bfcdf2228999f112b20aa46a9e61b39aa594808c Mon Sep 17 00:00:00 2001
From: Clarence Chew <62918570+clarence-chew@users.noreply.github.com>
Date: Tue, 23 Apr 2024 14:16:43 +0800
Subject: [PATCH 12/23] Add definitions

---
 Coxeter/ForMathlib/ASCShellingProps.lean      | 25 +++++++++++--------
 .../ForMathlib/AbstractSimplicialComplex.lean | 13 ++++++++++
 2 files changed, 27 insertions(+), 11 deletions(-)

diff --git a/Coxeter/ForMathlib/ASCShellingProps.lean b/Coxeter/ForMathlib/ASCShellingProps.lean
index 6f709c4d..61607da5 100644
--- a/Coxeter/ForMathlib/ASCShellingProps.lean
+++ b/Coxeter/ForMathlib/ASCShellingProps.lean
@@ -9,7 +9,7 @@ open Classical
 variable {V : Type*} --[DecidableEq V]
 
 def Deletion (F : AbstractSimplicialComplex V) (x : V) : Set F.faces :=
-  {f | x ∉ f.1 }
+  {f | x ∉ f.1}
 
 def DeletionSimplex (F : AbstractSimplicialComplex V) (x : V) : AbstractSimplicialComplex V where
   faces := Deletion F x
@@ -29,20 +29,19 @@ def DeletionSimplex (F : AbstractSimplicialComplex V) (x : V) : AbstractSimplici
       exact hab this
     · exact F.lower' hab ha.2
 
-def Link (F : AbstractSimplicialComplex V) (x : V) : Set F.faces :=
-  {f | x ∉ f.1 ∧ {x} ∪ f.1 ∈ F.faces }
+def Link (F : AbstractSimplicialComplex V) (x : vertices F) : Set F.faces :=
+  {f | x.1 ∉ f.1 ∧ {x.1} ∪ f.1 ∈ F.faces}
 
-def LinkSimplex (F : AbstractSimplicialComplex V) (x : V) (h : {x} ∈ F.faces) : AbstractSimplicialComplex V where
+def LinkSimplex (F : AbstractSimplicialComplex V) (x : vertices F) : AbstractSimplicialComplex V where
   faces := Link F x
   empty_mem := by
     simp only [Set.mem_image, Subtype.exists, mem_faces, exists_and_right, exists_eq_right, Link]
     use F.empty_mem
     simp only [Set.mem_setOf_eq, Finset.not_mem_empty, not_false_eq_true, Finset.union_empty,
       true_and]
-    exact h
+    exact (vertices_iff_singleton_set_face F x).mpr x.2
   lower' := sorry
 
-
 def LinkFace (F : AbstractSimplicialComplex V) (s : F.faces) : Set F.faces :=
   {f | s.1 ∩ f.1 = ∅ ∧ s.1 ∪ f.1 ∈ F.faces }
 
@@ -52,13 +51,17 @@ def Star (F : AbstractSimplicialComplex V) (s : F.faces) : Set F.faces :=
 lemma LinkFace_subset_Star (F : AbstractSimplicialComplex V) (s : F.faces) :
   LinkFace F s ⊆ Star F s := fun _ h ↦ h.2
 
-
 -- see if we can remove Fintype V
 -- something is off, need to check empty set
-/-def VertexDecomposable [Fintype V] (F : AbstractSimplicialComplex V) (hp : Pure F) : Prop :=
-  (∃ (f : Finset V), F = simplex f) ∨
-  (∃ (x : V), (DeletionSimplex F x).rank = F.rank ∧ VertexDecomposable (DeletionSimplex F x) ∧
-  (LinkSimplex F x).rank + 1 = F.rank)-/
+def VertexDecomposable [Fintype V] (F : AbstractSimplicialComplex V) : Prop :=
+  (Pure F) ∧ ((∃ (f : Finset V), F = simplex f) ∨
+  (∃ (x : vertices F), (DeletionSimplex F x.1).rank = F.rank ∧ VertexDecomposable (DeletionSimplex F x) ∧
+  (LinkSimplex F x).rank + 1 = F.rank ∧ VertexDecomposable (LinkSimplex F x)))
+termination_by (F.rank, (vertices F).ncard)
+decreasing_by
+  all_goals simp_wf
+  sorry
+  sorry
 
 
 -- Page 83: define VertexDecomposable, SheddingVertex
diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index a3970ebf..abb39d3c 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -150,6 +150,19 @@ Definition: For any ASC F, we denote by vertices F the set of vertices of F.
 -/
 def vertices (F : AbstractSimplicialComplex V) : Set V := ⋃ s : F.faces, s.1.toSet
 
+lemma vertices_iff_singleton_set_face (F : AbstractSimplicialComplex V) (x : V) :
+    {x} ∈ F.faces ↔ x ∈ vertices F := by
+  constructor
+  · intro hx
+    simp only [vertices, Set.iUnion_coe_set, mem_faces,
+      Set.mem_iUnion, Finset.mem_coe, exists_prop]
+    exact ⟨{x}, And.intro hx (Finset.mem_singleton.mpr rfl)⟩
+  · rintro ⟨sx, ⟨⟨a, ha⟩, hxsx⟩⟩
+    rw [← ha] at hxsx
+    refine @lower' V F a.1 _ ?_ a.2
+    simp only [Finset.le_eq_subset, Finset.singleton_subset_iff]
+    exact hxsx
+
 /--
 Definition: Let F be an ASC. A maximal face of F is called a facet of F.
 -/

From ee076f7e8e6f469c805c41f09b669f6bcd03a767 Mon Sep 17 00:00:00 2001
From: Lei Bichang <leibichang58@ruc.edu.cn>
Date: Tue, 23 Apr 2024 14:19:19 +0800
Subject: [PATCH 13/23] Reorder the lemmas

---
 .../ForMathlib/AbstractSimplicialComplex.lean | 35 ++++++++++---------
 1 file changed, 19 insertions(+), 16 deletions(-)

diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index cf8b9b57..3b9ac7b0 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -156,10 +156,6 @@ theorem iSup_faces_of_nonempty {ι : Type*} (x : ι → AbstractSimplicialComple
     apply Set.not_nonempty_iff_eq_empty.1 at h
     simp at h
 
-@[simp]
-theorem iSup_faces_of_isEmpty {ι : Type*} [IsEmpty ι] (x : ι → AbstractSimplicialComplex V) : (⨆ i, x i).faces = {∅} := by
-  sorry
-
 /-- Definition: For any ASC `F`, we denote by `vertices F` the set of vertices of F. -/
 def vertices (F : AbstractSimplicialComplex V) : Set V := ⋃ s : F.faces, s.1.toSet
 
@@ -211,18 +207,6 @@ lemma pure_def {F : AbstractSimplicialComplex V} [Pure F] : ∀ s ∈ F.Facets,
 
 lemma pure_isPure {F : AbstractSimplicialComplex V} [Pure F] : IsPure F := pure_def
 
-theorem iSup_Facets_le {ι : Type*} {p : ι → AbstractSimplicialComplex V} : (⨆ i : ι, p i).Facets ≤ ⋃ i : ι, (p i).Facets := by
-  intro a ha
-  rw [Set.mem_iUnion]
-  rcases ha with ⟨ha_mem, ha_max⟩
-  by_cases hi : Nonempty ι
-  · sorry
-  · sorry
-
-theorem isPure_iSup {ι : Type*} {p : ι → AbstractSimplicialComplex V} (hp : ∀i : ι, IsPure (p i)) : IsPure (⨆ i : ι, p i) := by
-  intro s hs t ht
-  sorry
-
 /--
 The rank of an ASC is defined to be the supremum of the cardinals of its faces.
 If the size of simplices in F is unbounded, it has rank `0` by definition.
@@ -400,4 +384,23 @@ lemma bot_faces_eq_empty : (⊥ : AbstractSimplicialComplex V).faces = {∅} :=
   rw [bot_eq_ofEmpty']
   simp[closurePower]
 
+@[simp]
+theorem iSup_faces_of_isEmpty {ι : Type*} [IsEmpty ι] (x : ι → AbstractSimplicialComplex V) : (⨆ i, x i).faces = {∅} := by
+  simp [iSup_of_empty]
+
+theorem iSup_Facets_le {ι : Type*} {p : ι → AbstractSimplicialComplex V} : (⨆ i : ι, p i).Facets ≤ ⋃ i : ι, (p i).Facets := by
+  intro a ha
+  rw [Set.mem_iUnion]
+  rcases ha with ⟨ha_mem, ha_max⟩
+  by_cases hi : Nonempty ι
+  · sorry
+  · sorry
+
+theorem isPure_iSup {ι : Type*} {p : ι → AbstractSimplicialComplex V} (hp : ∀i : ι, IsPure (p i)) : IsPure (⨆ i : ι, p i) := by
+  intro s hs t ht
+  sorry
+
+
+
+
 end AbstractSimplicialComplex

From 08c85867b6ed3e540e0cc34dcc1f69fc90249658 Mon Sep 17 00:00:00 2001
From: Lei Bichang <leibichang58@ruc.edu.cn>
Date: Tue, 23 Apr 2024 15:43:14 +0800
Subject: [PATCH 14/23] Prove iSup_Facets_le_of_nonempty

---
 .../ForMathlib/AbstractSimplicialComplex.lean | 52 +++++++++++++++----
 1 file changed, 41 insertions(+), 11 deletions(-)

diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index 3b9ac7b0..22b23b20 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -142,13 +142,13 @@ lemma sup_faces (F G : AbstractSimplicialComplex V) : (F ⊔ G).faces = F.faces
   rw [show F ⊔ G = sSup s by simp [s], show F.faces ∪ G.faces = ⋃ i : s, i.1.faces by simp [s], sSup_faces_of_nonempty (by simp [s])]
 
 @[simp]
-theorem iInf_faces {ι : Type*} (x : ι → AbstractSimplicialComplex V) : (⨅ i, x i).faces = ⨅ i, (x i).faces := by --might be wrong
+theorem iInf_faces {ι : Type*} (x : ι → AbstractSimplicialComplex V) : (⨅ i, x i).faces = ⋂ i, (x i).faces := by
   unfold iInf
   simp only [sInf_def, Set.iInter_coe_set, Set.mem_range, Set.iInter_exists, Set.iInter_iInter_eq',
     Set.sInf_eq_sInter, Set.sInter_range]
 
 @[simp]
-theorem iSup_faces_of_nonempty {ι : Type*} (x : ι → AbstractSimplicialComplex V) [Nonempty ι] : (⨆ i, x i).faces = ⨆ i, (x i).faces := by
+theorem iSup_faces_of_nonempty {ι : Type*} (x : ι → AbstractSimplicialComplex V) [Nonempty ι] : (⨆ i, x i).faces = ⋃ i, (x i).faces := by
   unfold iSup
   rw [sSup_faces_of_nonempty]
   · simp
@@ -368,6 +368,9 @@ instance instCompleteDistribLatticeToAbstractSimplicialComplex : CompleteDistrib
     simp [hf]
 }
 
+/-- WARNING : Not sure about correctness -/
+theorem isPure_closure_singelton (f : Finset V) : IsPure (closure {f}) := by sorry
+
 lemma bot_eq_ofEmpty' : (⊥ : AbstractSimplicialComplex V) = closurePower ∅ := by
   symm
   rw [eq_bot_iff, le_def, show (closurePower ∅).faces = {∅} by simp[closurePower], Set.singleton_subset_iff]
@@ -375,30 +378,57 @@ lemma bot_eq_ofEmpty' : (⊥ : AbstractSimplicialComplex V) = closurePower ∅ :
 
 lemma bot_eq_ofEmpty : (⊥ : AbstractSimplicialComplex V) = closure ∅ := by
   symm
-  rw[closure_eq_closurePower]
+  rw [closure_eq_closurePower]
   rw [eq_bot_iff, le_def, show (closurePower ∅).faces = {∅} by simp[closurePower], Set.singleton_subset_iff]
   apply (⊥ : AbstractSimplicialComplex V).empty_mem
 
 @[simp]
 lemma bot_faces_eq_empty : (⊥ : AbstractSimplicialComplex V).faces = {∅} := by
   rw [bot_eq_ofEmpty']
-  simp[closurePower]
+  simp only [closurePower, nonempty_subtype, Set.mem_empty_iff_false, exists_const, ↓reduceIte]
+
+@[simp]
+theorem bot_Facets : (⊥ : AbstractSimplicialComplex V).Facets = {∅} := by
+  ext x; constructor <;> intro hx
+  · rw [← bot_faces_eq_empty, mem_faces]
+    exact hx.1
+  · rw [Set.mem_singleton_iff.mp hx]
+    refine ⟨(⊥ : AbstractSimplicialComplex V).empty_mem, ?_⟩
+    intro t ht _
+    rw [← mem_faces, bot_faces_eq_empty, Set.mem_singleton_iff] at ht
+    exact ht.symm
+
+@[simp]
+theorem isPure_bot : IsPure (⊥ : AbstractSimplicialComplex V) := by
+  intro s hs t ht
+  rw [bot_Facets, Set.mem_singleton_iff] at *
+  rw [hs, ht]
 
 @[simp]
 theorem iSup_faces_of_isEmpty {ι : Type*} [IsEmpty ι] (x : ι → AbstractSimplicialComplex V) : (⨆ i, x i).faces = {∅} := by
-  simp [iSup_of_empty]
+  simp only [iSup_of_empty, bot_faces_eq_empty]
 
-theorem iSup_Facets_le {ι : Type*} {p : ι → AbstractSimplicialComplex V} : (⨆ i : ι, p i).Facets ≤ ⋃ i : ι, (p i).Facets := by
+theorem iSup_Facets_le_of_nonempty {ι : Type*} [Nonempty ι] {p : ι → AbstractSimplicialComplex V} : (⨆ i : ι, p i).Facets ≤ ⋃ i : ι, (p i).Facets := by
   intro a ha
   rw [Set.mem_iUnion]
   rcases ha with ⟨ha_mem, ha_max⟩
-  by_cases hi : Nonempty ι
-  · sorry
-  · sorry
+  rw [← mem_faces, iSup_faces_of_nonempty, Set.mem_iUnion] at ha_mem
+  rcases ha_mem with ⟨i, hi⟩
+  use i
+  constructor
+  · exact mem_faces.mpr hi
+  · intro t ht
+    apply ha_max
+    rw [← mem_faces, iSup_faces_of_nonempty]
+    apply Set.mem_iUnion_of_mem i ht
 
 theorem isPure_iSup {ι : Type*} {p : ι → AbstractSimplicialComplex V} (hp : ∀i : ι, IsPure (p i)) : IsPure (⨆ i : ι, p i) := by
-  intro s hs t ht
-  sorry
+  by_cases hemp : Nonempty ι
+  · intro s hs t ht
+    sorry
+  · rw [not_nonempty_iff] at hemp
+    rw [iSup_of_empty]
+    sorry
 
 
 

From 36875f2eb946319ec4eda26b72709ec2f7d7ad9e Mon Sep 17 00:00:00 2001
From: Clarence Chew <62918570+clarence-chew@users.noreply.github.com>
Date: Tue, 23 Apr 2024 16:32:49 +0800
Subject: [PATCH 15/23] Define VertexDecomposable

---
 Coxeter/ForMathlib/ASCShellingProps.lean | 69 ++++++++++++++++++++----
 1 file changed, 60 insertions(+), 9 deletions(-)

diff --git a/Coxeter/ForMathlib/ASCShellingProps.lean b/Coxeter/ForMathlib/ASCShellingProps.lean
index 61607da5..8dc9f6f4 100644
--- a/Coxeter/ForMathlib/ASCShellingProps.lean
+++ b/Coxeter/ForMathlib/ASCShellingProps.lean
@@ -51,18 +51,69 @@ def Star (F : AbstractSimplicialComplex V) (s : F.faces) : Set F.faces :=
 lemma LinkFace_subset_Star (F : AbstractSimplicialComplex V) (s : F.faces) :
   LinkFace F s ⊆ Star F s := fun _ h ↦ h.2
 
--- see if we can remove Fintype V
--- something is off, need to check empty set
-def VertexDecomposable [Fintype V] (F : AbstractSimplicialComplex V) : Prop :=
-  (Pure F) ∧ ((∃ (f : Finset V), F = simplex f) ∨
-  (∃ (x : vertices F), (DeletionSimplex F x.1).rank = F.rank ∧ VertexDecomposable (DeletionSimplex F x) ∧
-  (LinkSimplex F x).rank + 1 = F.rank ∧ VertexDecomposable (LinkSimplex F x)))
-termination_by (F.rank, (vertices F).ncard)
-decreasing_by
-  all_goals simp_wf
+lemma delete_vertex (F : AbstractSimplicialComplex V) (x : vertices F) :
+    vertices F \ {x.1} = (vertices (DeletionSimplex F x.1)) := by
+  ext t
+  simp [DeletionSimplex, Deletion]
+  constructor
+  · intro h
+    simp [Set.image]
+    use {t}
+    simp only [id_eq, Set.coe_setOf, Set.mem_setOf_eq, Set.mem_range, Finset.coe_eq_singleton,
+      Subtype.exists, exists_prop, exists_eq_right, Finset.mem_singleton, Set.mem_singleton_iff,
+      and_true]
+    refine And.intro ?_ ((vertices_iff_singleton_set_face F t).mpr h.1)
+    by_contra a
+    rw [a] at h
+    exact h.2 rfl
+  · rintro ⟨s, ⟨⟨a, ha⟩, hts⟩⟩
+    refine And.intro ⟨s, And.intro ?_ hts⟩ ?_
+    · simp only [Set.image, Set.range, Set.mem_setOf_eq]
+      have := a.2
+      simp only [id_eq, Set.mem_image, Set.mem_setOf_eq, Subtype.exists, mem_faces, exists_and_left,
+        exists_prop, exists_eq_right_right] at this
+      refine ⟨⟨a.1, this.2⟩, ?_⟩
+      rw [← ha]
+    · by_contra tx
+      rw [tx, ← ha] at hts
+      --apply a.2.2.1
+      sorry
+      /-have : x.1 ∈ a.1 := by
+        sorry
+      sorry
+      --simp [ha]-/
+
+lemma terminating_size [Fintype V] (F : AbstractSimplicialComplex V) (x : vertices F) :
+    (vertices (DeletionSimplex F x.1)).ncard < (vertices F).ncard := by
   sorry
+
+-- Consider replacing Fintype V -> Fintype (vertices F)
+def VertexDecomposableInductive (r n : ℕ) [Fintype V] (F : AbstractSimplicialComplex V)
+    (h1 : r = F.rank) (h2 : n = (vertices F).ncard) : Prop :=
+  match r, n with
+  | 0, _ => True
+  --| _, 0 => True
+  | r' + 1, _ => (Pure F) ∧ (∃ (f : Finset V), F = simplex f) ∨
+      (∃ (x : vertices F), (by
+    let nd := (vertices (DeletionSimplex F x.1)).ncard
+    let nl := (vertices (LinkSimplex F x)).ncard
+    by_cases h : ((DeletionSimplex F x.1).rank = r' + 1) ∧ (LinkSimplex F x).rank = r'
+    · have := terminating_size F x
+      refine VertexDecomposableInductive (r' + 1) nd (DeletionSimplex F x) h.1.symm rfl ∧
+        VertexDecomposableInductive r' nl (LinkSimplex F x) h.2.symm rfl
+    · exact False
+      ))
+
+lemma fin_vertex_iff_fin_faces (F : AbstractSimplicialComplex V) : Finite F.faces ↔ Finite (vertices F) := by
   sorry
 
+def VertexDecomposable [Fintype V] (F : AbstractSimplicialComplex V) : Prop :=
+  VertexDecomposableInductive F.rank (vertices F).ncard F rfl rfl
+
+-- see if we can remove Fintype V
+-- something is off, need to check empty set
+
+
 
 -- Page 83: define VertexDecomposable, SheddingVertex
 -- create new file to do property 1, import ASC shelling, merge to master before taking

From f25bea060cf309363f1f95228329406bee36e141 Mon Sep 17 00:00:00 2001
From: Lei Bichang <leibichang58@ruc.edu.cn>
Date: Tue, 23 Apr 2024 16:55:30 +0800
Subject: [PATCH 16/23] Add some suspicious lemmas

---
 .../ForMathlib/AbstractSimplicialComplex.lean | 49 ++++++++++++++++---
 1 file changed, 41 insertions(+), 8 deletions(-)

diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index 22b23b20..bed1b613 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -257,7 +257,7 @@ lemma closure_simplex (f : Finset V) : closure {f} =  simplex f := by
 def closurePower (s : Set (Finset V)) : AbstractSimplicialComplex V where
   faces :=
     if Nonempty s then
-      ⋃ f : s, {t | t.toSet ⊆ f}
+      ⋃ f : s, {t | t ⊆ f}
     else
       {∅}
   empty_mem := by
@@ -297,12 +297,12 @@ lemma closure_eq_iSup (s : Set (Finset V)) : closure s = ⨆ f : s,  closure {f.
 theorem closure_eq_closurePower (s: Set (Finset V)) : closure s = closurePower s := by
   ext t
   constructor <;> intro ts
-  · rw [closure] at ts
-    simp at ts
+  · simp only [sInf_def, Set.coe_setOf, Set.mem_setOf_eq, Set.mem_iInter, mem_faces,
+    Subtype.forall] at ts
     unfold closurePower
     apply ts
     by_cases h : Nonempty s <;> simp [h]
-    · rw[Set.subset_def]
+    · rw [Set.subset_def]
       intro x xs
       simp only [Set.mem_iUnion, Set.mem_setOf_eq, exists_prop]
       use x
@@ -311,12 +311,12 @@ theorem closure_eq_closurePower (s: Set (Finset V)) : closure s = closurePower s
       intro g hg
       rw [h] at hg
       contradiction
-  · rw[closurePower] at ts
+  · rw [closurePower] at ts
     by_cases h : Nonempty s <;> simp [h]
     · simp [closurePower,h] at ts
       intro K sK
       obtain ⟨f,fs⟩ := ts
-      rw[Set.subset_def] at sK
+      rw [Set.subset_def] at sK
       obtain ⟨fs, tf⟩ := fs
       apply sK at fs
       exact mem_faces.1 <| K.lower' tf <| fs
@@ -326,6 +326,15 @@ theorem closure_eq_closurePower (s: Set (Finset V)) : closure s = closurePower s
       rw [ts]
       exact K.empty_mem
 
+lemma closure_faces (s : Set (Finset V)) : (closure s).faces = if Nonempty s then ⋃ f : s, {t : Finset V | t ⊆ f} else {∅} := by
+  rw [closure_eq_closurePower]; rfl
+
+lemma closure_singleton_faces (f : Finset V) : (closure {f}).faces = {t : Finset V | t ⊆ f} := by
+  letI : Nonempty ({f} : Set (Finset V)) := by sorry
+  rw [closure_faces]
+  simp only [nonempty_subtype, Set.mem_singleton_iff, exists_eq, ↓reduceIte, Set.iUnion_coe_set,
+    Set.iUnion_iUnion_eq_left]
+
 instance instNonemptyToAbstractSimplicialComplexContainingSet (s : Set (Finset V)) : Nonempty {x : AbstractSimplicialComplex V // s ⊆ x.faces} := ⟨closure s, subset_closure_faces _⟩
 
 /--
@@ -347,6 +356,9 @@ lemma closure_le {F : AbstractSimplicialComplex V} (h: s ⊆ F.faces) : closure
   simp only [sInf_def, Set.mem_setOf_eq, Set.mem_iInter, mem_faces, Set.coe_setOf, Subtype.forall] at h2
   exact h2 F h
 
+@[deprecated]
+theorem isPure_inf_of_Pure {F G : AbstractSimplicialComplex V} (hF : IsPure F) (hG : IsPure G) : IsPure (F ⊓ G) := by sorry
+
 instance instCompleteDistribLatticeToAbstractSimplicialComplex : CompleteDistribLattice (AbstractSimplicialComplex V) := {
   instCompleteLatticeToAbstractSimplicialComplex with
   inf_sSup_le_iSup_inf := by
@@ -368,8 +380,28 @@ instance instCompleteDistribLatticeToAbstractSimplicialComplex : CompleteDistrib
     simp [hf]
 }
 
-/-- WARNING : Not sure about correctness -/
-theorem isPure_closure_singelton (f : Finset V) : IsPure (closure {f}) := by sorry
+@[simp]
+theorem closure_singleton_Facets (f : Finset V) : (closure {f}).Facets = {f} := by
+  -- rw [closure_eq_closurePower]
+  ext g; constructor <;> intro hg
+  · rcases hg with ⟨hg_mem, hg_max⟩
+    rw [Set.mem_singleton_iff]
+    contrapose! hg_max
+    use f
+    constructor
+    · apply mem_faces.mp
+      apply Set.mem_of_subset_of_mem <| subset_closure_faces {f}
+      rfl
+    · refine ⟨?_, hg_max⟩
+      rw [← mem_faces, closure_faces] at hg_mem
+      sorry
+  · sorry
+
+
+theorem isPure_closure_singelton (f : Finset V) : IsPure (closure {f}) := by
+  intro s hs t ht
+  rw [closure_singleton_Facets, Set.mem_singleton_iff] at *
+  rw [hs, ht]
 
 lemma bot_eq_ofEmpty' : (⊥ : AbstractSimplicialComplex V) = closurePower ∅ := by
   symm
@@ -422,6 +454,7 @@ theorem iSup_Facets_le_of_nonempty {ι : Type*} [Nonempty ι] {p : ι → Abstra
     rw [← mem_faces, iSup_faces_of_nonempty]
     apply Set.mem_iUnion_of_mem i ht
 
+@[deprecated]
 theorem isPure_iSup {ι : Type*} {p : ι → AbstractSimplicialComplex V} (hp : ∀i : ι, IsPure (p i)) : IsPure (⨆ i : ι, p i) := by
   by_cases hemp : Nonempty ι
   · intro s hs t ht

From 1c408375e791a90fb6bd6c972856b4f9d2878ba9 Mon Sep 17 00:00:00 2001
From: Lei Bichang <leibichang58@ruc.edu.cn>
Date: Wed, 24 Apr 2024 10:16:40 +0800
Subject: [PATCH 17/23] =?UTF-8?q?Prove=20closure=20{f=20=E2=88=A9=20g}=20?=
 =?UTF-8?q?=3D=20closure=20{f}=20=E2=8A=93=20closure=20{g}?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../ForMathlib/AbstractSimplicialComplex.lean | 51 +++++++++++++------
 1 file changed, 36 insertions(+), 15 deletions(-)

diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index bed1b613..190aab49 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -47,6 +47,9 @@ instance : SetLike (AbstractSimplicialComplex V) (Finset V) where
 theorem mem_faces {F : AbstractSimplicialComplex V} {x : Finset V} : x ∈ F.faces ↔ x ∈ F :=
   Iff.rfl
 
+lemma eq_iff_faces (F G : AbstractSimplicialComplex V) : F = G ↔ F.faces = G.faces := by
+  constructor <;> (intro h; ext; rw [h])
+
 @[simp]
 def le (G F : AbstractSimplicialComplex V) := G.faces ⊆ F.faces
 
@@ -320,7 +323,7 @@ theorem closure_eq_closurePower (s: Set (Finset V)) : closure s = closurePower s
       obtain ⟨fs, tf⟩ := fs
       apply sK at fs
       exact mem_faces.1 <| K.lower' tf <| fs
-    · simp [closurePower,h] at ts
+    · simp [closurePower, h] at ts
       intro K _
       apply mem_faces.1
       rw [ts]
@@ -330,11 +333,13 @@ lemma closure_faces (s : Set (Finset V)) : (closure s).faces = if Nonempty s the
   rw [closure_eq_closurePower]; rfl
 
 lemma closure_singleton_faces (f : Finset V) : (closure {f}).faces = {t : Finset V | t ⊆ f} := by
-  letI : Nonempty ({f} : Set (Finset V)) := by sorry
   rw [closure_faces]
   simp only [nonempty_subtype, Set.mem_singleton_iff, exists_eq, ↓reduceIte, Set.iUnion_coe_set,
     Set.iUnion_iUnion_eq_left]
 
+-- lemma closure_singleton_faces' (f : Finset V) : (closure {f}).faces = Finset.powerset f := by
+--   rw [closure_singleton_faces]
+
 instance instNonemptyToAbstractSimplicialComplexContainingSet (s : Set (Finset V)) : Nonempty {x : AbstractSimplicialComplex V // s ⊆ x.faces} := ⟨closure s, subset_closure_faces _⟩
 
 /--
@@ -356,9 +361,6 @@ lemma closure_le {F : AbstractSimplicialComplex V} (h: s ⊆ F.faces) : closure
   simp only [sInf_def, Set.mem_setOf_eq, Set.mem_iInter, mem_faces, Set.coe_setOf, Subtype.forall] at h2
   exact h2 F h
 
-@[deprecated]
-theorem isPure_inf_of_Pure {F G : AbstractSimplicialComplex V} (hF : IsPure F) (hG : IsPure G) : IsPure (F ⊓ G) := by sorry
-
 instance instCompleteDistribLatticeToAbstractSimplicialComplex : CompleteDistribLattice (AbstractSimplicialComplex V) := {
   instCompleteLatticeToAbstractSimplicialComplex with
   inf_sSup_le_iSup_inf := by
@@ -368,34 +370,42 @@ instance instCompleteDistribLatticeToAbstractSimplicialComplex : CompleteDistrib
       intro i is f hf
       rw [Set.mem_iUnion]
       use i
-      simp [is, hf]
-    · simp [Set.not_nonempty_iff_eq_empty.mp hs]
+      simp only [is, iSup_pos, inf_faces, hf]
+    · simp only [Set.not_nonempty_iff_eq_empty.mp hs, sSup_empty, ge_iff_le, bot_le,
+      inf_of_le_right, Set.mem_empty_iff_false, not_false_eq_true, iSup_neg, iSup_bot, le_refl]
   iInf_sup_le_sup_sInf := by
     intro a s
-    simp [Set.union_iInter]
+    simp only [le_def, iInf_faces, sup_faces, sInf_def, Set.iInter_coe_set, Set.union_iInter,
+      Set.subset_iInter_iff]
     intro i is f hf
     rw [Set.mem_iInter] at hf
     replace hf := hf i
-    simp [is] at hf
-    simp [hf]
+    simp only [is, iInf_pos, sup_faces, Set.mem_union, mem_faces] at hf
+    simp only [Set.mem_union, mem_faces, hf]
 }
 
 @[simp]
 theorem closure_singleton_Facets (f : Finset V) : (closure {f}).Facets = {f} := by
-  -- rw [closure_eq_closurePower]
   ext g; constructor <;> intro hg
   · rcases hg with ⟨hg_mem, hg_max⟩
     rw [Set.mem_singleton_iff]
     contrapose! hg_max
-    use f
-    constructor
+    use f; constructor
     · apply mem_faces.mp
       apply Set.mem_of_subset_of_mem <| subset_closure_faces {f}
       rfl
     · refine ⟨?_, hg_max⟩
       rw [← mem_faces, closure_faces] at hg_mem
-      sorry
-  · sorry
+      simpa only [nonempty_subtype, Set.mem_singleton_iff, exists_eq, ↓reduceIte,
+        Set.iUnion_coe_set, Set.iUnion_iUnion_eq_left, Set.mem_setOf_eq] using hg_mem
+  · rw [Set.mem_singleton_iff] at hg
+    subst hg; constructor
+    · apply Set.mem_of_subset_of_mem <| subset_closure_faces {g}; rfl
+    · intro t ht
+      rw [← mem_faces, closure_faces] at ht
+      simp only [nonempty_subtype, Set.mem_singleton_iff, exists_eq, ↓reduceIte, Set.iUnion_coe_set,
+        Set.iUnion_iUnion_eq_left, Set.mem_setOf_eq] at ht
+      apply fun h ↦ subset_antisymm h ht
 
 
 theorem isPure_closure_singelton (f : Finset V) : IsPure (closure {f}) := by
@@ -403,6 +413,17 @@ theorem isPure_closure_singelton (f : Finset V) : IsPure (closure {f}) := by
   rw [closure_singleton_Facets, Set.mem_singleton_iff] at *
   rw [hs, ht]
 
+theorem closure_singleton_inter_eq_inf {f g : Finset V} : closure {f ∩ g} = closure {f} ⊓ closure {g} := by
+  simp only [eq_iff_faces, inf_faces, closure_singleton_faces]
+  ext x; constructor <;> {
+    intro h
+    simpa only [Set.mem_inter_iff, Set.mem_setOf_eq, Finset.subset_inter_iff] using h
+  }
+
+theorem isPure_inf_closure_singleton {f g : Finset V} : IsPure (closure {f} ⊓ closure {g}) := by
+  rw [← closure_singleton_inter_eq_inf]
+  apply isPure_closure_singelton
+
 lemma bot_eq_ofEmpty' : (⊥ : AbstractSimplicialComplex V) = closurePower ∅ := by
   symm
   rw [eq_bot_iff, le_def, show (closurePower ∅).faces = {∅} by simp[closurePower], Set.singleton_subset_iff]

From efa5ed686f6dbae164a5f39cd9a45fa52015cdce Mon Sep 17 00:00:00 2001
From: Lei Bichang <leibichang58@ruc.edu.cn>
Date: Wed, 24 Apr 2024 10:33:16 +0800
Subject: [PATCH 18/23] Restate isPure_iSup

---
 Coxeter/ForMathlib/AbstractSimplicialComplex.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index 190aab49..6fd83324 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -222,6 +222,8 @@ noncomputable def rank (F : AbstractSimplicialComplex V) : ℕ := iSup fun s : F
 as faces.
 
 Remark: Here we secretly consider the ambient space as the simplex with vertex set V.
+
+Maybe don't use `abbrev` will be better? Because sometimes we don't want `simp` to expand this construction.
 -/
 abbrev closure (s : Set (Finset V))
   : AbstractSimplicialComplex V := sInf {K | s ⊆  K.faces}
@@ -476,10 +478,9 @@ theorem iSup_Facets_le_of_nonempty {ι : Type*} [Nonempty ι] {p : ι → Abstra
     apply Set.mem_iUnion_of_mem i ht
 
 @[deprecated]
-theorem isPure_iSup {ι : Type*} {p : ι → AbstractSimplicialComplex V} (hp : ∀i : ι, IsPure (p i)) : IsPure (⨆ i : ι, p i) := by
+theorem isPure_iSup {ι : Type*} {p : ι → AbstractSimplicialComplex V} {d : ℕ} (hp : ∀i : ι, IsPure' (p i) d) : IsPure' (⨆ i : ι, p i) d := by
   by_cases hemp : Nonempty ι
-  · intro s hs t ht
-    sorry
+  · sorry
   · rw [not_nonempty_iff] at hemp
     rw [iSup_of_empty]
     sorry

From 3009f323d4d7bbccf9105a3478344f905dd7a4fe Mon Sep 17 00:00:00 2001
From: Lei Bichang <leibichang58@ruc.edu.cn>
Date: Wed, 24 Apr 2024 15:48:34 +0800
Subject: [PATCH 19/23] Change PartialOrder.Shellable to Change
 PartialOrder.ShellableDelta

---
 Coxeter/ForMathlib/ASCShelling.lean               | 13 ++++++-------
 Coxeter/ForMathlib/AbstractSimplicialComplex.lean | 13 -------------
 Coxeter/ForMathlib/ELlabeling.lean                | 10 +++++-----
 Coxeter/ForMathlib/PosetShelling.lean             |  6 +++---
 4 files changed, 14 insertions(+), 28 deletions(-)

diff --git a/Coxeter/ForMathlib/ASCShelling.lean b/Coxeter/ForMathlib/ASCShelling.lean
index 46a64808..cb4d32b6 100644
--- a/Coxeter/ForMathlib/ASCShelling.lean
+++ b/Coxeter/ForMathlib/ASCShelling.lean
@@ -1,26 +1,24 @@
---import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Set.Card
 import Coxeter.ForMathlib.AbstractSimplicialComplex
 
 namespace AbstractSimplicialComplex
-variable {V : Type*} --[DecidableEq V]
+variable {V : Type*}
 
 /--
 Definition: Let `F` be a pure abstract simplicial complex of rank `d + 1` with finite facets.
 A shelling of `F` is an linear ordering `l₁`, ⋯ , `lₘ` of all (maximal) facets of F such that
  `lᵢ ⊓ (⨆ {j < i}, lⱼ)`  is an abstract simplicial complex pure of rank `d`.
 -/
-def Shelling {F : AbstractSimplicialComplex V} [hpure : Pure F] {m : ℕ} (l : Fin m ≃ Facets F) := F.rank > 0 ∧
+def Shelling {F : AbstractSimplicialComplex V} {m : ℕ} (l : Fin m ≃ Facets F) := F.rank > 0 ∧
   ∀ k : Fin m, 0 < k.1 → IsPure' ((⨆ j : {j // j < k}, closure {(l j).1}) ⊓ (closure {(l k).1})) (F.rank - 1)
 
 open Classical
-
 /--
 Definition': Let `F` be a pure abstract simplicial complex of rank `d + 1`.
 A shelling of `F` is an linear ordering `l₁`, ⋯ , `lₘ` of all (maximal) facets of `F` such that
  for any `i < k`, there exists `j < k`, such that `lᵢ ∩ lₖ ⊆ lⱼ ∩ lₖ` and `|lⱼ ∩ lₖ| = d`.
 -/
-def Shelling' {F :  AbstractSimplicialComplex V} [hpure : Pure F] {m : ℕ} (l : Fin m ≃ Facets F) :=
+def Shelling' {F :  AbstractSimplicialComplex V} {m : ℕ} (l : Fin m ≃ Facets F) :=
   F.rank > 0 ∧
   ∀ k i : Fin m, i < k → ∃ j : Fin m, j < k ∧
     (closure {(l i).1} ⊓ closure {(l k).1} ≤ closure {(l j).1} ⊓ closure {(l k).1}) ∧
@@ -34,11 +32,12 @@ lemma shelling_iff_shelling' {F : AbstractSimplicialComplex V}  [hpure: Pure F]
     · sorry
     · refine fun ⟨a, b⟩ ↦ ⟨a, ?_⟩
       intro k kge0 s hs
-      rw [iSup_inf_eq (a := closure {(l k).1})] at hs
+      have : ∃j : Fin m, j < k ∧ ∀i : Fin m, i < k → closure {(l i).1} ⊓ closure {(l k).1} ≤ closure {(l j).1} ⊓ closure {(l k).1} := by sorry
+      rw [iSup_inf_eq] at hs
       sorry
 
 /-- Definition: An abstract simplicial complex `F` is called shellable, if it admits a shelling. -/
-def Shellable (F : AbstractSimplicialComplex F) [Pure F] := ∃ (m: ℕ) (l : Fin m ≃ Facets F), Shelling l
+def Shellable (F : AbstractSimplicialComplex F) := ∃ (m : ℕ) (l : Fin m ≃ Facets F), Shelling l
 
 -- lemma cone_Shellabe_iff {F G : AbstractSimplicialComplex V} {r : ℕ} [Pure F] [Pure G] (x : V) (hcone: Cone F G x) :
 --   Shellable F ↔ Shellable G  := by sorry
diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index 6fd83324..f579c4d0 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -339,9 +339,6 @@ lemma closure_singleton_faces (f : Finset V) : (closure {f}).faces = {t : Finset
   simp only [nonempty_subtype, Set.mem_singleton_iff, exists_eq, ↓reduceIte, Set.iUnion_coe_set,
     Set.iUnion_iUnion_eq_left]
 
--- lemma closure_singleton_faces' (f : Finset V) : (closure {f}).faces = Finset.powerset f := by
---   rw [closure_singleton_faces]
-
 instance instNonemptyToAbstractSimplicialComplexContainingSet (s : Set (Finset V)) : Nonempty {x : AbstractSimplicialComplex V // s ⊆ x.faces} := ⟨closure s, subset_closure_faces _⟩
 
 /--
@@ -477,15 +474,5 @@ theorem iSup_Facets_le_of_nonempty {ι : Type*} [Nonempty ι] {p : ι → Abstra
     rw [← mem_faces, iSup_faces_of_nonempty]
     apply Set.mem_iUnion_of_mem i ht
 
-@[deprecated]
-theorem isPure_iSup {ι : Type*} {p : ι → AbstractSimplicialComplex V} {d : ℕ} (hp : ∀i : ι, IsPure' (p i) d) : IsPure' (⨆ i : ι, p i) d := by
-  by_cases hemp : Nonempty ι
-  · sorry
-  · rw [not_nonempty_iff] at hemp
-    rw [iSup_of_empty]
-    sorry
-
-
-
 
 end AbstractSimplicialComplex
diff --git a/Coxeter/ForMathlib/ELlabeling.lean b/Coxeter/ForMathlib/ELlabeling.lean
index ea7cc6c9..9d1e51b2 100644
--- a/Coxeter/ForMathlib/ELlabeling.lean
+++ b/Coxeter/ForMathlib/ELlabeling.lean
@@ -9,16 +9,16 @@ variable {A : Type*} [PartialOrder A]
 instance {x y : P} : Fintype (Set.Icc x y) := sorry -- temperory
 
 /-
-Definition: Let P and A be posets. An edge labelling of P in A is a map from the set of edges of P to the poset A.
+Definition: Let `P` and `A` be posets. An edge labelling of `P` in `A` is a map from the set of edges of `P` to the poset `A`.
 -/
 @[simp]
 abbrev edgeLabeling (P A : Type*) [PartialOrder P] := edges P  → A
 
 /-
-Definition: Let P and A be posets and l be an edge labelling of P in A.
-Then any maximal chain m : x_0 ⋖ x_1 ⋖ ⋯ ⋖ x_n in P, we define a list in A by [l(x_0 ⋖ x_1),l(x_1 ⋖ x_2), ⋯ ,l(x_{n-1} ⋖ x_n)].
+Definition: Let `P` and `A` be posets and `l` be an edge labelling of `P` in `A`.
+Then for any maximal chain `m : x_0 ⋖ x_1 ⋖ ⋯ ⋖ x_n` in `P`, we define a list in `A` by `[l(x_0 ⋖ x_1), l(x_1 ⋖ x_2), ⋯, l (x_{n-1} ⋖ x_n)]`.
 -/
-def mapMaxChain (l : edgeLabeling P A) (m : maximalChains P)  : List A := List.map (fun e => l e) <| edgePairs m
+def mapMaxChain (l : edgeLabeling P A) (m : maximalChains P) : List A := List.map (fun e => l e) <| edgePairs m
 
 /-
 Definition: Let P and A be posets and l be an edge labelling of P in A.
@@ -43,7 +43,7 @@ class ELLabeling (l : edgeLabeling P A) where
 
 /-Theorem: Let P be a graded finite poset with an EL-labelling l to a poset A. Then P is shellable.
 -/
-theorem shellable_of_ELLabeling {P : Type*} [PartialOrder P] [PartialOrder A] [Fintype P] [GradedPoset P] (l : edgeLabeling P A) (h: ELLabeling l): Shellable P :=sorry
+theorem shellable_of_ELLabeling {P : Type*} [PartialOrder P] [PartialOrder A] [Fintype P] [GradedPoset P] (l : edgeLabeling P A) (h: ELLabeling l): ShellableDelta P := sorry
 
 
 end PartialOrder
diff --git a/Coxeter/ForMathlib/PosetShelling.lean b/Coxeter/ForMathlib/PosetShelling.lean
index dfb8c8bc..8fffeca6 100644
--- a/Coxeter/ForMathlib/PosetShelling.lean
+++ b/Coxeter/ForMathlib/PosetShelling.lean
@@ -6,10 +6,10 @@ namespace PartialOrder
 open AbstractSimplicialComplex
 
 /-
-Definition: Let P be a graded poset. We say P is shellable, if the order complex Delta.ASC is shellable.
+Definition: Let `P` be a graded poset. We say `P` is shellable, if the order complex `Delta P` is shellable.
 -/
-def Shellable (P : Type*) [PartialOrder P] [Fintype P] [GradedPoset P] :=
-  shellable (Delta P)
+def ShellableDelta (P : Type*) [PartialOrder P] [Fintype P] [GradedPoset P] :=
+  Shellable (Delta P)
 
 
 

From 7e3f6fcef7d7088dc7571d782240fe689f0f782c Mon Sep 17 00:00:00 2001
From: Lei Bichang <leibichang58@ruc.edu.cn>
Date: Thu, 25 Apr 2024 09:34:38 +0800
Subject: [PATCH 20/23] Prove isPure_iSup_isPure by Liu Haotian

---
 Coxeter/ForMathlib/ASCShelling.lean               | 11 +++++------
 Coxeter/ForMathlib/AbstractSimplicialComplex.lean |  6 ++++++
 2 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/Coxeter/ForMathlib/ASCShelling.lean b/Coxeter/ForMathlib/ASCShelling.lean
index cb4d32b6..2c076020 100644
--- a/Coxeter/ForMathlib/ASCShelling.lean
+++ b/Coxeter/ForMathlib/ASCShelling.lean
@@ -13,6 +13,7 @@ def Shelling {F : AbstractSimplicialComplex V} {m : ℕ} (l : Fin m ≃ Facets F
   ∀ k : Fin m, 0 < k.1 → IsPure' ((⨆ j : {j // j < k}, closure {(l j).1}) ⊓ (closure {(l k).1})) (F.rank - 1)
 
 open Classical
+
 /--
 Definition': Let `F` be a pure abstract simplicial complex of rank `d + 1`.
 A shelling of `F` is an linear ordering `l₁`, ⋯ , `lₘ` of all (maximal) facets of `F` such that
@@ -26,14 +27,12 @@ def Shelling' {F :  AbstractSimplicialComplex V} {m : ℕ} (l : Fin m ≃ Facets
 
 /-- Lemma: The two definitions of shellings are equivalent.
 -/
-lemma shelling_iff_shelling' {F : AbstractSimplicialComplex V}  [hpure: Pure F] {m : ℕ} (l : Fin m ≃ Facets F) :
+lemma shelling_iff_shelling' {F : AbstractSimplicialComplex V} (hF : IsPure F) {m : ℕ} (l : Fin m ≃ Facets F) :
     Shelling l ↔ Shelling' l := by
-    constructor
+    constructor <;> refine fun ⟨a, b⟩ ↦ ⟨a, ?_⟩
     · sorry
-    · refine fun ⟨a, b⟩ ↦ ⟨a, ?_⟩
-      intro k kge0 s hs
-      have : ∃j : Fin m, j < k ∧ ∀i : Fin m, i < k → closure {(l i).1} ⊓ closure {(l k).1} ≤ closure {(l j).1} ⊓ closure {(l k).1} := by sorry
-      rw [iSup_inf_eq] at hs
+    · intro k kge0
+
       sorry
 
 /-- Definition: An abstract simplicial complex `F` is called shellable, if it admits a shelling. -/
diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index f579c4d0..538e955b 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -474,5 +474,11 @@ theorem iSup_Facets_le_of_nonempty {ι : Type*} [Nonempty ι] {p : ι → Abstra
     rw [← mem_faces, iSup_faces_of_nonempty]
     apply Set.mem_iUnion_of_mem i ht
 
+theorem isPure_iSup_isPure {ι : Type*} {p : ι → AbstractSimplicialComplex V} {d : ℕ} (hp : ∀i : ι, IsPure' (p i) d) [Nonempty ι]: IsPure' (⨆ i : ι, p i) d := by
+  intro s hs
+  apply iSup_Facets_le_of_nonempty at hs
+  obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hs
+  apply hp at hi
+  exact hi
 
 end AbstractSimplicialComplex

From ec4029b6e91344d2d6340fe496a7b43604b553e4 Mon Sep 17 00:00:00 2001
From: Lei Bichang <leibichang58@ruc.edu.cn>
Date: Thu, 25 Apr 2024 17:22:02 +0800
Subject: [PATCH 21/23] Add finiteness condition on ASC

1. Re-arange ASC.lean
2. Create LocallyFIniteASC.lean
3. Add [Fintype V] as a hypothesis of shelling_iff_shelling'`
---
 Coxeter/ForMathlib/ASCShelling.lean           |  37 +++-
 .../ForMathlib/AbstractSimplicialComplex.lean | 177 ++++++++++--------
 Coxeter/ForMathlib/LocallyFiniteASC.lean      |  25 +++
 3 files changed, 149 insertions(+), 90 deletions(-)
 create mode 100644 Coxeter/ForMathlib/LocallyFiniteASC.lean

diff --git a/Coxeter/ForMathlib/ASCShelling.lean b/Coxeter/ForMathlib/ASCShelling.lean
index 2c076020..0fab32b9 100644
--- a/Coxeter/ForMathlib/ASCShelling.lean
+++ b/Coxeter/ForMathlib/ASCShelling.lean
@@ -2,7 +2,16 @@ import Mathlib.Data.Set.Card
 import Coxeter.ForMathlib.AbstractSimplicialComplex
 
 namespace AbstractSimplicialComplex
-variable {V : Type*}
+variable {V : Type*} [Fintype V] [DecidableEq V]
+
+/-- If there is *some finiteness condition* on `F : ASC V`, then there every face of `F` is contained in a facet -/
+theorem exists_subset_Facet {F : AbstractSimplicialComplex V} (hf : f ∈ F) : ∃ g ∈ F.Facets, f ⊆ g := by
+  let s := {g ∈ F | f ⊆ g}
+  have : Set.Finite s := Set.Finite.subset (s := F.faces) (Set.toFinite _) fun a ha ↦ ha.1
+  rcases Set.Finite.exists_maximal_wrt (fun (a : Finset V) ↦ a) s this ⟨f, hf, by rfl⟩ with ⟨g, hg1, hg2⟩
+  refine ⟨g, ⟨hg1.1, ?_⟩, hg1.2⟩
+  intro a ha1 ha2
+  apply hg2 a ⟨ha1, (subset_trans hg1.2 ha2)⟩ ha2
 
 /--
 Definition: Let `F` be a pure abstract simplicial complex of rank `d + 1` with finite facets.
@@ -12,8 +21,6 @@ A shelling of `F` is an linear ordering `l₁`, ⋯ , `lₘ` of all (maximal) fa
 def Shelling {F : AbstractSimplicialComplex V} {m : ℕ} (l : Fin m ≃ Facets F) := F.rank > 0 ∧
   ∀ k : Fin m, 0 < k.1 → IsPure' ((⨆ j : {j // j < k}, closure {(l j).1}) ⊓ (closure {(l k).1})) (F.rank - 1)
 
-open Classical
-
 /--
 Definition': Let `F` be a pure abstract simplicial complex of rank `d + 1`.
 A shelling of `F` is an linear ordering `l₁`, ⋯ , `lₘ` of all (maximal) facets of `F` such that
@@ -22,15 +29,29 @@ A shelling of `F` is an linear ordering `l₁`, ⋯ , `lₘ` of all (maximal) fa
 def Shelling' {F :  AbstractSimplicialComplex V} {m : ℕ} (l : Fin m ≃ Facets F) :=
   F.rank > 0 ∧
   ∀ k i : Fin m, i < k → ∃ j : Fin m, j < k ∧
-    (closure {(l i).1} ⊓ closure {(l k).1} ≤ closure {(l j).1} ⊓ closure {(l k).1}) ∧
-    (closure {(l j).1} ⊓ closure {(l k).1}).rank + 1 = F.rank
+    (l i).1 ∩ (l k).1 ⊆ (l j).1 ∩ (l k).1 ∧
+    ((l j).1 ∩ (l k).1).card + 1 = F.rank
 
 /-- Lemma: The two definitions of shellings are equivalent.
 -/
-lemma shelling_iff_shelling' {F : AbstractSimplicialComplex V} (hF : IsPure F) {m : ℕ} (l : Fin m ≃ Facets F) :
+lemma shelling_iff_shelling'_aux {F : AbstractSimplicialComplex V} (hF : IsPure F) {m : ℕ} [NeZero m] (l : Fin m ≃ Facets F) :
     Shelling l ↔ Shelling' l := by
-    constructor <;> refine fun ⟨a, b⟩ ↦ ⟨a, ?_⟩
-    · sorry
+    constructor <;> refine fun ⟨a, h⟩ ↦ ⟨a, ?_⟩
+    · intro k i ilek
+      replace h := h k <| lt_of_le_of_lt (zero_le _) (Fin.lt_def.mp ilek)
+      rw [iSup_inf_eq] at h
+      letI : Nonempty { j // j < k } := ⟨0, lt_of_le_of_lt (Fin.zero_le' _) ilek⟩
+      have : (l i).1 ∩ (l k).1 ∈ ⨆ j : {j // j < k}, closure {(l j).1} ⊓ closure {(l k).1} := by
+        -- rw [← mem_faces, iSup_faces_of_nonempty]
+        sorry
+      -- have : (l i).1 ∩ (l k).1 ∈ F := F.lower' (Finset.inter_subset_left _ _) (l i).2.1
+      rcases exists_subset_Facet this with ⟨f, hf_mem, hf_big⟩
+      rcases exits_mem_faces_of_mem_iSup hf_mem with ⟨j, hj⟩
+      rw [← closure_singleton_inter_eq_inf, closure_singleton_Facets, Set.mem_singleton_iff] at hj
+      subst hj
+      refine ⟨j, j.2, by convert hf_big, ?_⟩ -- have to `covnert` due to previous using of classical
+
+      sorry
     · intro k kge0
 
       sorry
diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index 538e955b..c676bbe1 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -44,12 +44,36 @@ instance : SetLike (AbstractSimplicialComplex V) (Finset V) where
     congr
 
 @[simp, nolint simpNF]
-theorem mem_faces {F : AbstractSimplicialComplex V} {x : Finset V} : x ∈ F.faces ↔ x ∈ F :=
+theorem mem_faces {F : AbstractSimplicialComplex V} : x ∈ F.faces ↔ x ∈ F :=
   Iff.rfl
 
 lemma eq_iff_faces (F G : AbstractSimplicialComplex V) : F = G ↔ F.faces = G.faces := by
   constructor <;> (intro h; ext; rw [h])
 
+/--
+The rank of an ASC is defined to be the supremum of the cardinals of its faces.
+If the size of simplices in F is unbounded, it has rank `0` by definition.
+
+Remark: We should general be careful with the unbounded case.
+-/
+noncomputable def rank (F : AbstractSimplicialComplex V) : ℕ := iSup fun s : F.faces => s.1.card
+
+/-- Definition: For any ASC `F`, we denote by `vertices F` the set of vertices of F. -/
+def vertices (F : AbstractSimplicialComplex V) : Set V := ⋃ s : F.faces, s.1.toSet
+
+/--
+Definition: The simplex with verteces `s ⊆ V` is the complex of all finite subsets of `s`.
+-/
+def simplex (s : Set V) : AbstractSimplicialComplex V where
+  faces := {t | t.toSet ⊆ s}
+  empty_mem := by simp
+  lower' := by
+    intro a b h1 h2
+    refine' Set.Subset.trans ?_ h2
+    congr
+
+section order
+
 @[simp]
 def le (G F : AbstractSimplicialComplex V) := G.faces ⊆ F.faces
 
@@ -68,17 +92,6 @@ instance partialOrder : PartialOrder (AbstractSimplicialComplex V) where
 @[simp]
 lemma le_def {G F : AbstractSimplicialComplex V} : G ≤ F ↔ G.faces ⊆ F.faces := by rfl
 
-/--
-Definition: The simplex with verteces `s ⊆ V` is the complex of all finite subsets of `s`.
--/
-def simplex (s : Set V) : AbstractSimplicialComplex V where
-  faces := {t | t.toSet ⊆ s}
-  empty_mem := by simp
-  lower' := by
-    intro a b h1 h2
-    refine' Set.Subset.trans ?_ h2
-    congr
-
 @[simp]
 lemma simplex_face {s : Set V} {a : Finset V} : a ∈ (simplex s).faces ↔ a.toSet ⊆ s := by rfl
 
@@ -159,64 +172,9 @@ theorem iSup_faces_of_nonempty {ι : Type*} (x : ι → AbstractSimplicialComple
     apply Set.not_nonempty_iff_eq_empty.1 at h
     simp at h
 
-/-- Definition: For any ASC `F`, we denote by `vertices F` the set of vertices of F. -/
-def vertices (F : AbstractSimplicialComplex V) : Set V := ⋃ s : F.faces, s.1.toSet
-
-/--
-Definition: Let `F` be an ASC. A maximal face of F is called a facet of F.
--/
-def IsFacet (F : AbstractSimplicialComplex V) (s : Finset V) := s ∈ F ∧ ∀ t ∈ F, s ⊆ t → s = t
-
-/--
-Definition: For any ASC F, we denote by Facets F the set of facets of F.
--/
-def Facets (F : AbstractSimplicialComplex V) : Set (Finset V) := {s | F.IsFacet s}
-
-/-- Definition: A pure abstract simplicial complex is an abstract simplicial complex
-    where all facets have the same cardinality. -/
-def IsPure (F : AbstractSimplicialComplex V) :=
-  ∀ s ∈ Facets F, ∀ t ∈ Facets F, s.card = t.card
+end order
 
-class Pure (F : AbstractSimplicialComplex V) : Prop where
-  pure : ∀ s ∈ F.Facets, ∀ t ∈ F.Facets, s.card = t.card
-
-/--Definition: We will call an ASC pure of rank `d` if all its facets has `d` elements-/
-def IsPure' (F : AbstractSimplicialComplex V) (d : ℕ) :=
-  ∀ s ∈ F.Facets, s.card = d
-
-class Pure' (F : AbstractSimplicialComplex V) (d : ℕ) : Prop where
-  pure : ∀ s ∈ F.Facets, s.card = d
-
-lemma isPure_iff_isPure' {F : AbstractSimplicialComplex V} : F.IsPure ↔ ∃ d, F.IsPure' d := by
-  by_cases hemp : Nonempty F.Facets
-  · constructor
-    · let s := Classical.choice (hemp)
-      exact fun hIp ↦ ⟨s.1.card, fun t ht ↦ hIp t ht s s.2⟩
-    · rintro ⟨d, hIp'⟩ s hs t ht
-      rw [hIp' s hs, hIp' t ht]
-  · constructor
-    · intro; use 0
-      simp only [IsPure', Finset.card_eq_zero]
-      contrapose! hemp
-      rcases hemp with ⟨d, ⟨_, _⟩⟩
-      use d
-    · intro
-      simp only [nonempty_subtype, not_exists] at hemp
-      intro s hs
-      exfalso
-      exact hemp s hs
-
-lemma pure_def {F : AbstractSimplicialComplex V} [Pure F] : ∀ s ∈ F.Facets, ∀ t ∈ F.Facets, s.card = t.card := Pure.pure
-
-lemma pure_isPure {F : AbstractSimplicialComplex V} [Pure F] : IsPure F := pure_def
-
-/--
-The rank of an ASC is defined to be the supremum of the cardinals of its faces.
-If the size of simplices in F is unbounded, it has rank `0` by definition.
-
-Remark: We should general be careful with the unbounded case.
--/
-noncomputable def rank (F : AbstractSimplicialComplex V) : ℕ := iSup fun s : F.faces => s.1.card
+section closure
 
 /-- Definition: For a collection s of subsets of V, we denote by closure s the smallest ASC over V containing all elements in s
 as faces.
@@ -383,6 +341,58 @@ instance instCompleteDistribLatticeToAbstractSimplicialComplex : CompleteDistrib
     simp only [Set.mem_union, mem_faces, hf]
 }
 
+end closure
+
+section facet_and_pure
+
+/--
+Definition: Let `F` be an ASC. A maximal face of F is called a facet of F.
+-/
+def IsFacet (F : AbstractSimplicialComplex V) (s : Finset V) := s ∈ F ∧ ∀ t ∈ F, s ⊆ t → s = t
+
+/--
+Definition: For any ASC F, we denote by Facets F the set of facets of F.
+-/
+def Facets (F : AbstractSimplicialComplex V) : Set (Finset V) := {s | F.IsFacet s}
+
+/-- Definition: A pure abstract simplicial complex is an abstract simplicial complex
+    where all facets have the same cardinality. -/
+def IsPure (F : AbstractSimplicialComplex V) :=
+  ∀ s ∈ Facets F, ∀ t ∈ Facets F, s.card = t.card
+
+@[deprecated IsPure]
+class Pure (F : AbstractSimplicialComplex V) : Prop where
+  pure : ∀ s ∈ F.Facets, ∀ t ∈ F.Facets, s.card = t.card
+
+/--Definition: We will call an ASC pure of rank `d` if all its facets has `d` elements-/
+def IsPure' (F : AbstractSimplicialComplex V) (d : ℕ) :=
+  ∀ s ∈ F.Facets, s.card = d
+
+@[deprecated IsPure']
+class Pure' (F : AbstractSimplicialComplex V) (d : ℕ) : Prop where
+  pure : ∀ s ∈ F.Facets, s.card = d
+
+/-- The definitions of purity are equivalent. -/
+lemma isPure_iff_isPure' {F : AbstractSimplicialComplex V} : F.IsPure ↔ ∃ d, F.IsPure' d := by
+  by_cases hemp : Nonempty F.Facets
+  · constructor
+    · let s := Classical.choice (hemp)
+      exact fun hIp ↦ ⟨s.1.card, fun t ht ↦ hIp t ht s s.2⟩
+    · rintro ⟨d, hIp'⟩ s hs t ht
+      rw [hIp' s hs, hIp' t ht]
+  · constructor
+    · intro; use 0
+      simp only [IsPure', Finset.card_eq_zero]
+      contrapose! hemp
+      rcases hemp with ⟨d, ⟨_, _⟩⟩
+      use d
+    · intro
+      simp only [nonempty_subtype, not_exists] at hemp
+      intro s hs
+      exfalso
+      exact hemp s hs
+
+/-- The simplex of `f : Finset V` contains a unique facet `f`.-/
 @[simp]
 theorem closure_singleton_Facets (f : Finset V) : (closure {f}).Facets = {f} := by
   ext g; constructor <;> intro hg
@@ -406,12 +416,13 @@ theorem closure_singleton_Facets (f : Finset V) : (closure {f}).Facets = {f} :=
         Set.iUnion_iUnion_eq_left, Set.mem_setOf_eq] at ht
       apply fun h ↦ subset_antisymm h ht
 
-
+/-- Simplexes of finsets are pure. -/
 theorem isPure_closure_singelton (f : Finset V) : IsPure (closure {f}) := by
   intro s hs t ht
   rw [closure_singleton_Facets, Set.mem_singleton_iff] at *
   rw [hs, ht]
 
+/-- The simplex of `f ∩ g` with `f g : Finset V` is equal to the infimum of the simplexes of `f` and `g`. -/
 theorem closure_singleton_inter_eq_inf {f g : Finset V} : closure {f ∩ g} = closure {f} ⊓ closure {g} := by
   simp only [eq_iff_faces, inf_faces, closure_singleton_faces]
   ext x; constructor <;> {
@@ -419,24 +430,21 @@ theorem closure_singleton_inter_eq_inf {f g : Finset V} : closure {f ∩ g} = cl
     simpa only [Set.mem_inter_iff, Set.mem_setOf_eq, Finset.subset_inter_iff] using h
   }
 
-theorem isPure_inf_closure_singleton {f g : Finset V} : IsPure (closure {f} ⊓ closure {g}) := by
-  rw [← closure_singleton_inter_eq_inf]
-  apply isPure_closure_singelton
-
-lemma bot_eq_ofEmpty' : (⊥ : AbstractSimplicialComplex V) = closurePower ∅ := by
+lemma bot_eq_closurePower_empty : (⊥ : AbstractSimplicialComplex V) = closurePower ∅ := by
   symm
   rw [eq_bot_iff, le_def, show (closurePower ∅).faces = {∅} by simp[closurePower], Set.singleton_subset_iff]
   apply (⊥ : AbstractSimplicialComplex V).empty_mem
 
-lemma bot_eq_ofEmpty : (⊥ : AbstractSimplicialComplex V) = closure ∅ := by
+lemma bot_eq_closure_empty : (⊥ : AbstractSimplicialComplex V) = closure ∅ := by
   symm
   rw [closure_eq_closurePower]
   rw [eq_bot_iff, le_def, show (closurePower ∅).faces = {∅} by simp[closurePower], Set.singleton_subset_iff]
   apply (⊥ : AbstractSimplicialComplex V).empty_mem
 
+/-- The bottom of ASC is the singleton of emptyset. -/
 @[simp]
 lemma bot_faces_eq_empty : (⊥ : AbstractSimplicialComplex V).faces = {∅} := by
-  rw [bot_eq_ofEmpty']
+  rw [bot_eq_closurePower_empty]
   simp only [closurePower, nonempty_subtype, Set.mem_empty_iff_false, exists_const, ↓reduceIte]
 
 @[simp]
@@ -460,6 +468,7 @@ theorem isPure_bot : IsPure (⊥ : AbstractSimplicialComplex V) := by
 theorem iSup_faces_of_isEmpty {ι : Type*} [IsEmpty ι] (x : ι → AbstractSimplicialComplex V) : (⨆ i, x i).faces = {∅} := by
   simp only [iSup_of_empty, bot_faces_eq_empty]
 
+/-- Given a nonempty family `p i` of ASCs, every facet of their supremum `⨆ i, p i` is a facet of some `p i`. -/
 theorem iSup_Facets_le_of_nonempty {ι : Type*} [Nonempty ι] {p : ι → AbstractSimplicialComplex V} : (⨆ i : ι, p i).Facets ≤ ⋃ i : ι, (p i).Facets := by
   intro a ha
   rw [Set.mem_iUnion]
@@ -474,11 +483,15 @@ theorem iSup_Facets_le_of_nonempty {ι : Type*} [Nonempty ι] {p : ι → Abstra
     rw [← mem_faces, iSup_faces_of_nonempty]
     apply Set.mem_iUnion_of_mem i ht
 
-theorem isPure_iSup_isPure {ι : Type*} {p : ι → AbstractSimplicialComplex V} {d : ℕ} (hp : ∀i : ι, IsPure' (p i) d) [Nonempty ι]: IsPure' (⨆ i : ι, p i) d := by
+lemma exits_mem_faces_of_mem_iSup {ι : Type*} [Nonempty ι] {p : ι → AbstractSimplicialComplex V}  (hf : f ∈ (⨆ i : ι, p i).Facets) : ∃ i : ι, f ∈ (p i).Facets :=
+  Set.mem_iUnion.mp (iSup_Facets_le_of_nonempty hf)
+
+/-- The supremum of a nonempty pure ASC family is pure. -/
+theorem isPure_iSup_isPure {ι : Type*} [Nonempty ι] {p : ι → AbstractSimplicialComplex V} {d : ℕ} (hp : ∀i : ι, IsPure' (p i) d) : IsPure' (⨆ i : ι, p i) d := by
   intro s hs
-  apply iSup_Facets_le_of_nonempty at hs
-  obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hs
-  apply hp at hi
-  exact hi
+  obtain ⟨i, hi⟩ := exits_mem_faces_of_mem_iSup hs
+  apply hp i s hi
+
+end facet_and_pure
 
 end AbstractSimplicialComplex
diff --git a/Coxeter/ForMathlib/LocallyFiniteASC.lean b/Coxeter/ForMathlib/LocallyFiniteASC.lean
new file mode 100644
index 00000000..835a28df
--- /dev/null
+++ b/Coxeter/ForMathlib/LocallyFiniteASC.lean
@@ -0,0 +1,25 @@
+import Coxeter.ForMathlib.AbstractSimplicialComplex
+
+namespace AbstractSimplicialComplex
+variable {V : Type*}
+
+section dendrite
+
+/-- An ASC is dendrite, if every face of it is contained in a facet.
+
+Should be made into instance? -/
+def Dendrite (F : AbstractSimplicialComplex V) :=
+  ∀ f ∈ F, ∃ g ∈ F.Facets, f ⊆ g
+
+end dendrite
+
+section loc_finite
+
+/-- An ASC `F` is locally finite, if for every face `f` of it, there is only finitely many faces `g` containing `f`.
+Might be a BAD definition.
+
+Should be made into instance? -/
+def LocallyFinite (F : AbstractSimplicialComplex V) :=
+  ∀ f ∈ F, Finite {g ∈ F | f ⊆ g}
+
+end loc_finite

From f22891ad17ac051ba9720eae55a423e58d5844a3 Mon Sep 17 00:00:00 2001
From: Clarence Chew <62918570+clarence-chew@users.noreply.github.com>
Date: Thu, 25 Apr 2024 21:35:29 +0800
Subject: [PATCH 22/23] Remove cone

---
 Coxeter/ForMathlib/AbstractSimplicialComplex.lean | 15 ---------------
 1 file changed, 15 deletions(-)

diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index abb39d3c..52bf793e 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -332,19 +332,4 @@ lemma closure_le {F : AbstractSimplicialComplex V} (h: s ⊆ F.faces) : closure
   simp only [sInf_def, Set.mem_setOf_eq, Set.mem_iInter, mem_faces, Set.coe_setOf, Subtype.forall] at h2
   exact h2 F h
 
-/--
-Definition: G is a cone over F with cone point x if
-x ∈ G.vertices - F.vertices
-s ∈ F ⇔ s ∪ {x} ∈ G.
--/
-def Cone (F G: AbstractSimplicialComplex V) (x : V) :=
-  ¬(x ∈ F.vertices) ∧ ∀ s, s ∈ F.faces ↔ s ∈ G.faces ∧ s ∪ {x} ∈ G.faces
-
-def isCone (G: AbstractSimplicialComplex V) := ∃ F x, Cone F G x
-
-lemma cons_pure (hc : Cone F G x) (hp : Pure F) : Pure G := by sorry
-
-/- the following lemma is not true -/
--- lemma cons_pure' (hc : isCone G) : Pure G := by sorry
-
 end AbstractSimplicialComplex

From 153ede120ba7528cdc238c196b56aa37253ffaa4 Mon Sep 17 00:00:00 2001
From: Clarence Chew <62918570+clarence-chew@users.noreply.github.com>
Date: Thu, 25 Apr 2024 22:34:11 +0800
Subject: [PATCH 23/23] Fix merge

---
 .../ForMathlib/AbstractSimplicialComplex.lean | 51 -------------------
 1 file changed, 51 deletions(-)

diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index 47c91923..5c228ae2 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -152,11 +152,6 @@ lemma sSup_eq_unionSubset {s : Set <| AbstractSimplicialComplex V} (hs : s.Nonem
 lemma sSup_faces_of_nonempty {s : Set (AbstractSimplicialComplex V)} (h : s.Nonempty) : (sSup s).faces = ⋃ F : s, F.1.faces := by
   rw [sSup_eq_unionSubset h]; rfl
 
-/--
-Definition: For any ASC F, we denote by vertices F the set of vertices of F.
--/
-def vertices (F : AbstractSimplicialComplex V) : Set V := ⋃ s : F.faces, s.1.toSet
-
 lemma vertices_iff_singleton_set_face (F : AbstractSimplicialComplex V) (x : V) :
     {x} ∈ F.faces ↔ x ∈ vertices F := by
   constructor
@@ -170,52 +165,6 @@ lemma vertices_iff_singleton_set_face (F : AbstractSimplicialComplex V) (x : V)
     simp only [Finset.le_eq_subset, Finset.singleton_subset_iff]
     exact hxsx
 
-/--
-Definition: Let F be an ASC. A maximal face of F is called a facet of F.
--/
-def IsFacet (F : AbstractSimplicialComplex V) (s : Finset V) := s ∈ F ∧ ∀ t ∈ F, s ⊆ t → s = t
-
-/--
-Definition: For any ASC F, we denote by Facets F the set of facets of F.
--/
-def Facets (F : AbstractSimplicialComplex V) : Set (Finset V) := {s | F.IsFacet s}
-
-/-- Definition: A pure abstract simplicial complex is an abstract simplicial complex
-    where all facets have the same cardinality. -/
-def IsPure (F : AbstractSimplicialComplex V) :=
-  ∀ s ∈ Facets F, ∀ t ∈ Facets F, s.card = t.card
-
-class Pure (F : AbstractSimplicialComplex V) : Prop where
-  pure : ∀ s ∈ F.Facets, ∀ t ∈ F.Facets, s.card = t.card
-
-/--Definition: We will call an ASC pure of rank `d` if all its facets has `d` elements-/
-def IsPure' (F : AbstractSimplicialComplex V) (d : ℕ) :=
-  ∀ s ∈ F.Facets, s.card = d
-
-class Pure' (F : AbstractSimplicialComplex V) (d : ℕ) : Prop where
-  pure : ∀ s ∈ F.Facets, s.card = d
-
-lemma isPure_iff_isPure' {F : AbstractSimplicialComplex V} : F.IsPure ↔ ∃ d, F.IsPure' d := by
-  by_cases hemp : Nonempty F.Facets
-  · constructor
-    · let s := Classical.choice (hemp)
-      exact fun hIp ↦ ⟨s.1.card, fun t ht ↦ hIp t ht s s.2⟩
-    · rintro ⟨d, hIp'⟩ s hs t ht
-      rw [hIp' s hs, hIp' t ht]
-  · constructor
-    · intro; use 0
-      simp only [IsPure', Finset.card_eq_zero]
-      contrapose! hemp
-      rcases hemp with ⟨d, ⟨_, _⟩⟩
-      use d
-    · intro
-      simp only [nonempty_subtype, not_exists] at hemp
-      intro s hs t _
-      exfalso
-      exact hemp s hs
-
-lemma pure_def {F : AbstractSimplicialComplex V} [Pure F] : ∀ s ∈ F.Facets, ∀ t ∈ F.Facets, s.card = t.card := Pure.pure
-
 @[simp]
 lemma sup_faces (F G : AbstractSimplicialComplex V) : (F ⊔ G).faces = F.faces ∪ G.faces := by
   let s : Set (AbstractSimplicialComplex V) := {F, G}