diff --git a/Coxeter/ForMathlib/ASCShelling.lean b/Coxeter/ForMathlib/ASCShelling.lean
index cb4d32b..09c61ef 100644
--- a/Coxeter/ForMathlib/ASCShelling.lean
+++ b/Coxeter/ForMathlib/ASCShelling.lean
@@ -1,24 +1,26 @@
+--import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Set.Card
 import Coxeter.ForMathlib.AbstractSimplicialComplex
 
 namespace AbstractSimplicialComplex
-variable {V : Type*}
+variable {V : Type*} --[DecidableEq V]
 
 /--
 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)
+def Shelling {F : AbstractSimplicialComplex V} [hpure : Pure F] {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} {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 ∧
     (closure {(l i).1} ⊓ closure {(l k).1} ≤ closure {(l j).1} ⊓ closure {(l k).1}) ∧
@@ -26,20 +28,42 @@ 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) :
     Shelling l ↔ Shelling' l := by
     constructor
     · 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
+      rw [iSup_inf_eq (a := closure {(l k).1})] at hs
       sorry
 
+
+<<<<<<< HEAD
 /-- 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
+def Shellable (F : AbstractSimplicialComplex F) [Pure F] := ∃ (m: ℕ) (l : Fin m ≃ Facets F), Shelling l
+
+def cone_facet_bijection {F G : AbstractSimplicialComplex V} (h : Cone F G x) : Facets F ≃ Facets G := by
+  simp [Cone] at h
+
+  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
+=======
+def cone_facet_bijection {F G : AbstractSimplicialComplex V} (h : Cone F G x) : Facets F ≃ Facets G := by  
+  sorry
+  
+>>>>>>> 739d9c45217ef15dafcfa5d16710b0cf0f7ab01f
+lemma cone_Shellable_iff {F G : AbstractSimplicialComplex V} {r : ℕ} [Pure F] [Pure G] (x : V) (hcone: Cone F G x) :
+    Shellable F ↔ Shellable G := by
+  simp [Shellable, Shelling]
+  constructor
+  · rintro ⟨hrf, ⟨m, l, hml⟩⟩
+    -- add x to each set??
+  · rintro ⟨hrf, h⟩
+    -- remove x from each set??
+<<<<<<< HEAD
+=======
+    
+>>>>>>> 739d9c45217ef15dafcfa5d16710b0cf0f7ab01f
 
 end AbstractSimplicialComplex
diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index f579c4d..658f42a 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -47,9 +47,6 @@ 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
 
@@ -145,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
+theorem iInf_faces {ι : Type*} (x : ι → AbstractSimplicialComplex V) : (⨅ i, x i).faces = ⨅ i, (x i).faces := by --might be wrong
   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
@@ -159,7 +156,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. -/
+/--
+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
 
 /--
@@ -202,7 +201,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
+      intro s hs t _
       exfalso
       exact hemp s hs
 
@@ -210,6 +209,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.
@@ -222,8 +224,6 @@ 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}
@@ -233,9 +233,7 @@ 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
-  apply le_antisymm
-  · apply sInf_le; simp; rfl
-  · simp
+  sorry
 
 lemma closure_mono {s t: Set (Finset V)} : s ⊆ t → closure s ≤ closure t := by
   intro hst
@@ -243,14 +241,18 @@ 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
-    · rintro s h1
+    · rw [sInf_def]
+      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]
@@ -262,7 +264,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 ⊆ f}
+      ⋃ f : s, {t | t.toSet ⊆ f}
     else
       {∅}
   empty_mem := by
@@ -271,7 +273,8 @@ def closurePower (s : Set (Finset V)) : AbstractSimplicialComplex V where
   lower' := by
     by_cases h : Nonempty s <;> simp [h]
     · refine isLowerSet_iUnion₂ ?_
-      intro t _ a b h1 h2
+      intro t _
+      intro a b h1 h2
       refine' Set.Subset.trans ?_ h2
       congr
     · exact Finset.isLowerSet_singleton_empty V
@@ -301,13 +304,14 @@ 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
-  · simp only [sInf_def, Set.coe_setOf, Set.mem_setOf_eq, Set.mem_iInter, mem_faces,
-    Subtype.forall] at ts
+  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]
+    · rw[Set.subset_def]
       intro x xs
       simp only [Set.mem_iUnion, Set.mem_setOf_eq, exists_prop]
       use x
@@ -316,29 +320,22 @@ theorem closure_eq_closurePower (s: Set (Finset V)) : closure s = closurePower s
       intro g hg
       rw [h] at hg
       contradiction
-  · rw [closurePower] at ts
+  · 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
+      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
+    · 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 _⟩
 
 /--
@@ -369,60 +366,18 @@ instance instCompleteDistribLatticeToAbstractSimplicialComplex : CompleteDistrib
       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]
+      simp [is, hf]
+    · simp [Set.not_nonempty_iff_eq_empty.mp hs]
   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]
+    simp [Set.union_iInter]
     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]
+    simp [is] at hf
+    simp [hf]
 }
 
-@[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
-
-
-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]
-
-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]
@@ -430,49 +385,51 @@ 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 only [closurePower, nonempty_subtype, Set.mem_empty_iff_false, exists_const, ↓reduceIte]
+  simp[closurePower]
 
-@[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
+/--
+Definition: G is a cone over F with cone point x if
+x ∈ G.vertices - F.vertices
+s ∈ F ⇔ s ∪ {x} ∈ G.
+-/
 
-@[simp]
-theorem isPure_bot : IsPure (⊥ : AbstractSimplicialComplex V) := by
-  intro s hs t ht
-  rw [bot_Facets, Set.mem_singleton_iff] at *
-  rw [hs, ht]
+def Cone (F G: AbstractSimplicialComplex V) (x : V) :=
+  ¬(x ∈ F.vertices) ∧ ∀ s, s ∈ F.faces ↔  s ∪ {x} ∈ G.faces
 
-@[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]
-
-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
 
+def Cone_cons (F: AbstractSimplicialComplex V) (x : V) (h : x ∉ vertices F) : AbstractSimplicialComplex V where
+  faces := F.faces ∪ {s ∪ {x} | s ∈ F.faces}
+  empty_mem := Or.inl F.empty_mem
+  lower' := by
+    intro a b h1 h2
+    refine (Set.mem_union b F.faces {y | ∃ s ∈ F.faces, s ∪ {x} = y}).mpr ?_
+    simp only [mem_faces, Set.mem_setOf_eq]
+    rcases h2 with hl | hr
+    · exact Or.inl (F.lower' h1 hl)
+    · obtain ⟨s, hs, heq⟩ := hr
+      by_cases xinb : x ∈ b
+      · refine Or.inr ⟨s ∩ b, And.intro ?_ ?_⟩
+        exact F.lower' (Finset.inter_subset_left s b) hs
+        rw [← (Finset.singleton_inter_of_mem xinb),
+          ← Finset.union_inter_distrib_right, heq]
+        aesop
+      · left
+        have : b ⊆ s := by
+          intro y hy
+          have : y ∈ a := h1 hy
+          aesop
+        exact F.lower' this hs
+        
+
+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
 
 end AbstractSimplicialComplex