diff --git a/Coxeter/ForMathlib/ASCShelling.lean b/Coxeter/ForMathlib/ASCShelling.lean
index aca63313..0fab32b9 100644
--- a/Coxeter/ForMathlib/ASCShelling.lean
+++ b/Coxeter/ForMathlib/ASCShelling.lean
@@ -1,45 +1,65 @@
---import Mathlib.Data.Finset.Basic
 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.
--/
+variable {V : Type*} [Fintype V] [DecidableEq V]
 
-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)
+/-- 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.
+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} {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)
 
-/-
-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' {F :  AbstractSimplicialComplex V} {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
-
+    (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: 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
+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, 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
 
-/- 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
+      sorry
+    · intro k kge0
+
+      sorry
+
+/-- Definition: An abstract simplicial complex `F` is called shellable, if it admits a shelling. -/
+def Shellable (F : AbstractSimplicialComplex 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 {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/ASCShellingProps.lean b/Coxeter/ForMathlib/ASCShellingProps.lean
new file mode 100644
index 00000000..8dc9f6f4
--- /dev/null
+++ b/Coxeter/ForMathlib/ASCShellingProps.lean
@@ -0,0 +1,121 @@
+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 : vertices F) : Set F.faces :=
+  {f | x.1 ∉ f.1 ∧ {x.1} ∪ f.1 ∈ F.faces}
+
+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 (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 }
+
+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
+
+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
+
+end ASCShellingProps
diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index 5e9e0bdb..5c228ae2 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -44,9 +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
 
@@ -65,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
 
@@ -94,13 +110,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 =>
@@ -110,6 +126,9 @@ where
   inf_le_left := fun _ _ _ ha => ha.1
   __ := completeLatticeOfInf (AbstractSimplicialComplex V) sInf_isGLB
 
+@[simp]
+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
   empty_mem := by
@@ -128,88 +147,54 @@ 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
-
-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
   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
-
-/--
-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 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
 
-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}
+  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])]
 
-lemma pure_isPure {F : AbstractSimplicialComplex V} [Pure F] : IsPure F := pure_def
+@[simp]
+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]
 
-/--
-If the size of simplices in F is unbounded, it has rank 0 by definition.
+@[simp]
+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
 
-Remark: We should general be careful with the unbounded case.
--/
+end order
 
-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.
 
 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}
@@ -218,24 +203,25 @@ 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
+  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
   apply sInf_le_sInf
   rw [Set.setOf_subset_setOf]
   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
-    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]
@@ -243,24 +229,11 @@ 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 :=
     if Nonempty s then
-      ⨆ f : s, {t | t.toSet ⊆ f}
+      ⋃ f : s, {t | t ⊆ f}
     else
       {∅}
   empty_mem := by
@@ -269,13 +242,13 @@ 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
 
-theorem closure_union_eq_iSup_closure {ι : Type*} (p : ι → Set (Finset 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
   · apply sInf_le
@@ -289,16 +262,55 @@ theorem closure_union_eq_iSup_closure {ι : Type*} (p : ι → Set (Finset V)) :
     apply closure_mono <| Set.subset_iUnion p i
 
 /--
-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.
 -/
 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
-  sorry
+  ext t
+  constructor <;> intro 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]
+      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
+  · 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
+      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 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
+  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 _⟩
 
 /--
 Lemma: Let F be an ASC. Then the closure of the set of faces is just F.
@@ -319,20 +331,180 @@ 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 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 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 only [is, iInf_pos, sup_faces, Set.mem_union, mem_faces] at hf
+    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: G is a cone over F with cone point x if
-x ∈ G.vertices - F.vertices
-s ∈ F ⇔ s ∪ {x} ∈ G.
+Definition: For any ASC F, we denote by Facets F the set of facets of F.
 -/
-def Cone (F G: AbstractSimplicialComplex V) (x : V) :=
-  x ∈ G.vertices \ F.vertices ∧
-  ∀ s, s ∈ F.faces ↔ s ∪ {x} ∈ G.faces
+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
+  · 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
+      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
+
+/-- 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 <;> {
+    intro h
+    simpa only [Set.mem_inter_iff, Set.mem_setOf_eq, Finset.subset_inter_iff] using h
+  }
+
+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
 
-def isCone (G: AbstractSimplicialComplex V) := ∃ F x, Cone F G x
+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_closurePower_empty]
+  simp only [closurePower, nonempty_subtype, Set.mem_empty_iff_false, exists_const, ↓reduceIte]
 
-lemma cons_pure (hc : Cone F G x) (hp : Pure F) : Pure G := by sorry
+@[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]
 
-/- the following lemma is not true -/
--- lemma cons_pure' (hc : isCone G) : Pure G := by sorry
+@[simp]
+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]
+  rcases ha with ⟨ha_mem, ha_max⟩
+  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
+
+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
+  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/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/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
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)