From 02a9f40e05bb99c1cb114e10c51a39577b0fcc28 Mon Sep 17 00:00:00 2001
From: Haocheng Wang <152980872+hcWang942@users.noreply.github.com>
Date: Thu, 18 Apr 2024 18:14:44 +0800
Subject: [PATCH 1/5] Update AbstractSimplicialComplex.lean

---
 .../ForMathlib/AbstractSimplicialComplex.lean | 214 ++++++------------
 1 file changed, 73 insertions(+), 141 deletions(-)

diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index b241751e..0894a893 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -13,7 +13,7 @@ structure AbstractSimplicialComplex (V : Type*)  where
   empty_mem : ∅ ∈ faces
   lower' : IsLowerSet faces -- The set of faces is a lower set under the inclusion relation.
 
-theorem AbstractSimplicialComplex.nonempty {V : Type*} {F : AbstractSimplicialComplex V} : F.faces.Nonempty := Set.nonempty_of_mem F.empty_mem
+theorem abstract_simplicial_complex_nonempty {V : Type*} {F : AbstractSimplicialComplex V} : F.faces.Nonempty := Set.nonempty_of_mem F.empty_mem
 
 theorem isLowerSet_singleton_empty (α : Type*):
 IsLowerSet {(∅ : Set α)} := by
@@ -80,28 +80,28 @@ def simplex (s : Set V) : AbstractSimplicialComplex V where
 @[simp]
 lemma simplex_face {s : Set V} {a : Finset V} : a ∈ (simplex s).faces ↔ a.toSet ⊆ s := by rfl
 
-instance inf_set : InfSet (AbstractSimplicialComplex V) where
-  sInf := fun s => ⟨⋂ F : s, F.1.faces,
-    Set.mem_iInter.mpr (fun F => F.1.empty_mem),
-    isLowerSet_iInter (fun F => F.1.lower')⟩
+instance infSet : InfSet (AbstractSimplicialComplex V) where
+  sInf := fun s => ⟨⋂ F ∈ s, F.faces,
+    Set.mem_biInter (fun F _ => F.empty_mem) ,
+    isLowerSet_iInter₂ (fun F _ => F.lower')⟩
 
 @[simp]
-lemma sInf_def (s : Set (AbstractSimplicialComplex V)) : (sInf s).faces = ⋂ F : s, F.1.faces := rfl
+lemma sInf_def (s : Set (AbstractSimplicialComplex V)) : (sInf s).faces = ⋂ F ∈ s, F.faces := by rfl
 
 lemma sInf_isGLB (s : Set (AbstractSimplicialComplex V)) : IsGLB s (sInf s) := by
   constructor
-  . intro x hx
-    refine Set.iInter_subset_of_subset ⟨x, hx⟩ ?_
-    simp only [subset_of_eq]
-  . intro x hx
-    simp_rw [mem_lowerBounds,le_def] at hx
+  . intro F hF
+    simp only [sInf, le_def, Set.biInter_subset_of_mem hF]
+  . intro G hG
+    simp_rw [mem_lowerBounds,le_def] at hG
     rw [le_def,sInf_def]
-    simp only [Set.subset_iInter_iff, Subtype.coe_prop, hx, Subtype.forall, implies_true, forall_const]
+    simp only [Set.subset_iInter_iff]
+    exact hG
 
 
 /-- 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 completeLattice : 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 =>
@@ -112,100 +112,109 @@ where
   __ := completeLatticeOfInf (AbstractSimplicialComplex V) sInf_isGLB
 
 def unionSubset {s : Set <| AbstractSimplicialComplex V} (hs : s.Nonempty) : AbstractSimplicialComplex V where
-  faces := ⋃ F : s, F.1.faces
+  faces := ⋃ F ∈ s, F.faces
   empty_mem := by
     simp [Set.mem_iUnion]
     rcases hs with ⟨e, he⟩
     exact ⟨e, he, e.empty_mem⟩
-  lower' := isLowerSet_iUnion fun i ↦ i.1.lower'
+  lower' := isLowerSet_iUnion fun i ↦ isLowerSet_iUnion fun _ ↦ i.lower'
 
-lemma sSup_eq_unionSubset {s : Set <| AbstractSimplicialComplex V} (hs : s.Nonempty) : sSup s = unionSubset hs := by
+lemma sSup_eq_unionSubset {s : Set <| AbstractSimplicialComplex V} (hs : s.Nonempty) : sSup s = unionSubset hs  := by
   apply le_antisymm
   · apply sSup_le
     intro b bs
-    rw [le_def, show (unionSubset hs).faces = ⋃ F : s, F.1.faces by rfl]
-    apply Set.subset_iUnion_of_subset ⟨b, bs⟩
-    simp only [subset_of_eq]
+    refine Set.subset_iUnion_of_subset b (Set.subset_iUnion_of_subset bs (by rfl))
   · rw [le_sSup_iff]
     intro b hb
     rw [le_def]
-    exact Set.iUnion_subset fun i ↦ hb i.2
+    exact Set.iUnion_subset fun i ↦ Set.iUnion_subset fun hi ↦ hb hi
 
-def OfEmpty : AbstractSimplicialComplex V where
+def ofEmpty : AbstractSimplicialComplex V where
   faces := {∅}
   empty_mem := rfl
   lower' := Finset.isLowerSet_singleton_empty V
 
-lemma bot_eq_ofEmpty : (⊥ : AbstractSimplicialComplex V) = OfEmpty := by
+lemma bot_eq_ofEmpty : (⊥ : AbstractSimplicialComplex V) = ofEmpty := by
   symm
-  rw [eq_bot_iff, le_def, show OfEmpty.faces = {∅} by rfl, Set.singleton_subset_iff]
+  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
+theorem 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
+lemma sSup_faces_of_nonempty {s : Set (AbstractSimplicialComplex V)} (h : s.Nonempty) : (sSup s).faces = ⋃ F ∈ s, F.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
+def vertices (F : AbstractSimplicialComplex V) : Set V := ⋃ s ∈ F.faces, s.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
+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}
+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
+def isPure (F : AbstractSimplicialComplex V) :=
+  ∀ s∈ Facets F, ∀ t ∈ Facets F, s.card = t.card
 
 class Pure (F : AbstractSimplicialComplex V) where
-  pure : ∀ s ∈ F.Facets, ∀ t ∈ F.Facets, s.card = t.card
+  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 : ℕ) :=
+def isPure' (F : AbstractSimplicialComplex V) (d : ℕ):=
+  --∀ s ∈ F.faces, s.card = d
+  --这个我真心感觉错了，怎么可能Pure‘里面是Facets这里isPure'变成了faces
   ∀ s ∈ F.Facets, s.card = d
 
 class Pure' (F : AbstractSimplicialComplex V) (d :ℕ) where
   pure : ∀ s ∈ F.Facets, s.card = d
 
-lemma isPure_iff_isPure' {F : AbstractSimplicialComplex V} : F.IsPure ↔ ∃ d, F.IsPure' d := by
+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
+      intro hIp
+      use s.1.card
+      intro t ht
+      exact hIp t ht s s.2
+    · intro hIp'
+      obtain ⟨d, hIp'⟩ := hIp'
+      -- rcases hIp' with ⟨d, hIp'⟩ 在这里用rcases和obtain效果是完全一样的
+      intro s hs t ht
       rw [hIp' s hs, hIp' t ht]
   · constructor
-    · intro; use 0
-      simp only [IsPure', Finset.card_eq_zero]
+    · intro
+      use 0
+      simp only [isPure', Finset.card_eq_zero]
       contrapose! hemp
-      rcases hemp with ⟨d, ⟨a, _⟩⟩
+      rcases hemp with ⟨d, ⟨a, b⟩⟩
       use d
-    · intro
+    · intro h
+      rcases h with ⟨d, a⟩
       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
 
-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
+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.
 
 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
@@ -216,12 +225,6 @@ Remark: Here we secretly consider the ambient space as the simplex with vertex s
 abbrev closure (s : Set (Finset V))
   : AbstractSimplicialComplex V := sInf { K | s ⊆  K.faces}
 
-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.
 -/
@@ -231,101 +234,25 @@ lemma closure_simplex (f : Finset V) : closure {f} =  simplex f := by
     · rw [sInf_def]
       rintro s h1
       simp only [Set.singleton_subset_iff, mem_faces, Set.mem_setOf_eq, Set.mem_iInter] at h1
-      sorry
-      -- exact h1 (simplex ↑f) fun ⦃a⦄ a => a
+      exact h1 (simplex ↑f) fun ⦃a⦄ a => a
     · 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]
-      intro i
-      sorry
-      -- apply mem_faces.1 <| i.lower' h1 <| mem_faces.2 fi
+      intro i fi
+      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
-
-def ClosurePower (s: Set (Finset V)) : AbstractSimplicialComplex V where
-  faces :=
-    if Nonempty s then
-      ⨆ f : s, {t | t.toSet ⊆ f}
-    else
-      {∅}
-  empty_mem := by
-    by_cases h : Nonempty s <;> simp [h]
-    exact nonempty_subtype.mp h
-  lower' := by
-    by_cases h : Nonempty s <;> simp [h]
-    · refine isLowerSet_iUnion₂ ?_
-      intro t _
-      intro a b h1 h2
-      refine' Set.Subset.trans ?_ h2
-      congr
-    · exact Finset.isLowerSet_singleton_empty V
-
-theorem Closure_eq_ClosurePower (s: Set (Finset V)) : closure s = ClosurePower s := by
-  sorry
-
--- #check Set.mem_iUnion
-lemma face_closure_eq_iSup (s : Set (Finset V)) : (closure s).faces = ⨆ f ∈ s, (closure {f}).faces := by
-  apply le_antisymm
-  · rw [le_iSup_iff]
-    intro X hX
-    sorry
-
-  · intro X hX
-    have : ∀ (K: AbstractSimplicialComplex V), ∀ (f: Finset V), (f ∈ s) ∧ (s ⊆ K.faces) → {f} ⊆ K.faces := by
-      intro K f hs
-      simp only [Set.singleton_subset_iff]
-      obtain ⟨hs1, hs2⟩ := hs
-      exact hs2 hs1
-    have : ∀ (f: Finset V), (f ∈ s) → (closure {f}).faces ⊆ (closure s).faces := by
-      intro f fs
-      rw [← le_def, le_sInf_iff]
-      intro K Ks
-      apply sInf_le
-      · apply this
-        · rw [Set.iSup_eq_iUnion] at hX
-          simp only [Set.mem_iUnion] at hX
-          exact ⟨fs, Ks⟩
-    rw [Set.iSup_eq_iUnion] at hX
-    simp only [Set.mem_iUnion] at hX
-    rcases hX with ⟨f, hf⟩
-    rw [Set.iSup_eq_iUnion] at hf
-    simp only [Set.mem_iUnion] at hf
-    rcases hf with ⟨f, Xf⟩
-    exact Set.mem_of_subset_of_mem this f Xf
-
-lemma iSup_of_faces_eq_faces_of_iSup  (s : Set (Finset V)) : (⨆ f ∈ s, closure {f}).faces = ⨆ f : s, (closure {f.1}).faces := 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.
 -/
-lemma closure_eq_iSup (s : Set (Finset V)) : closure s = ⨆ f : s,  closure {f.1} := by
-  apply le_antisymm
-  · rw [le_iSup_iff]
-    intro x hx
-    rw [le_def, closure, sInf_def, ← Set.iInf_eq_iInter, ← Set.le_iff_subset, iInf_le_iff]
-    intro t ht
-    sorry
-  · apply iSup_le
-    intro i
-    apply closure_mono <| Set.singleton_subset_iff.mpr i.2
-
+lemma closure_eq_iSup (s : Set (Finset V)) : closure s =  ⨆ f ∈ s,  closure {f} := by sorry
+  
 
 /--
 Lemma: Let F be an ASC. Then the closure of the set of faces is just F.
@@ -335,34 +262,39 @@ lemma closure_self {F : AbstractSimplicialComplex V} : closure (F.faces) = F :=
     apply Set.Subset.antisymm
     · rw [sInf_def]
       rintro s h1; simp only [Set.mem_setOf_eq, Set.mem_iInter, mem_faces] at h1
-      sorry
-      -- exact h1 F fun ⦃_⦄ a => a
+      exact h1 F fun ⦃_⦄ a => a
     · rw [sInf_def]
       rintro s h1; simp only [Set.mem_setOf_eq, Set.mem_iInter, mem_faces]
-      sorry
-      -- exact fun _ i => i h1
+      exact fun _ i => i h1
   exact instSetLikeAbstractSimplicialComplexFinset.proof_1 (closure F.faces) F h1
 
+
+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 closure_le {F : AbstractSimplicialComplex V} (h: s ⊆ F.faces) : closure s ≤ F := by
   rintro s2 h2
-  simp only [sInf_def, Set.mem_setOf_eq, Set.mem_iInter, mem_faces] at h2
-  sorry
-  -- exact h2 F h
-
+  simp 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
 
--- instance cons_pure {h : Cone F G x} : Pure G := by sorry
+-- instance consPure {h : Cone F G x} : Pure G := by sorry
 
--- instance cons_pure' {h : isCone G} : Pure G := by sorry
+-- instance consPure' {h : isCone G} : Pure G := by sorry
 
 end AbstractSimplicialComplex

From 103e86570e8c440d895b3be2fa3db4aa6df54dab Mon Sep 17 00:00:00 2001
From: Haocheng Wang <152980872+hcWang942@users.noreply.github.com>
Date: Thu, 18 Apr 2024 18:25:22 +0800
Subject: [PATCH 2/5] Update AbstractSimplicialComplex.lean

---
 .../ForMathlib/AbstractSimplicialComplex.lean | 190 ++++++++++++------
 1 file changed, 126 insertions(+), 64 deletions(-)

diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index 0894a893..7e959788 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -13,7 +13,7 @@ structure AbstractSimplicialComplex (V : Type*)  where
   empty_mem : ∅ ∈ faces
   lower' : IsLowerSet faces -- The set of faces is a lower set under the inclusion relation.
 
-theorem abstract_simplicial_complex_nonempty {V : Type*} {F : AbstractSimplicialComplex V} : F.faces.Nonempty := Set.nonempty_of_mem F.empty_mem
+theorem AbstractSimplicialComplex.nonempty {V : Type*} {F : AbstractSimplicialComplex V} : F.faces.Nonempty := Set.nonempty_of_mem F.empty_mem
 
 theorem isLowerSet_singleton_empty (α : Type*):
 IsLowerSet {(∅ : Set α)} := by
@@ -80,23 +80,23 @@ def simplex (s : Set V) : AbstractSimplicialComplex V where
 @[simp]
 lemma simplex_face {s : Set V} {a : Finset V} : a ∈ (simplex s).faces ↔ a.toSet ⊆ s := by rfl
 
-instance infSet : InfSet (AbstractSimplicialComplex V) where
-  sInf := fun s => ⟨⋂ F ∈ s, F.faces,
-    Set.mem_biInter (fun F _ => F.empty_mem) ,
-    isLowerSet_iInter₂ (fun F _ => F.lower')⟩
+instance inf_set : InfSet (AbstractSimplicialComplex V) where
+  sInf := fun s => ⟨⋂ F : s, F.1.faces,
+    Set.mem_iInter.mpr (fun F => F.1.empty_mem),
+    isLowerSet_iInter (fun F => F.1.lower')⟩
 
 @[simp]
-lemma sInf_def (s : Set (AbstractSimplicialComplex V)) : (sInf s).faces = ⋂ F ∈ s, F.faces := by rfl
+lemma sInf_def (s : Set (AbstractSimplicialComplex V)) : (sInf s).faces = ⋂ F : s, F.1.faces := rfl
 
 lemma sInf_isGLB (s : Set (AbstractSimplicialComplex V)) : IsGLB s (sInf s) := by
   constructor
-  . intro F hF
-    simp only [sInf, le_def, Set.biInter_subset_of_mem hF]
-  . intro G hG
-    simp_rw [mem_lowerBounds,le_def] at hG
+  . intro x hx
+    refine Set.iInter_subset_of_subset ⟨x, hx⟩ ?_
+    simp only [subset_of_eq]
+  . intro x hx
+    simp_rw [mem_lowerBounds,le_def] at hx
     rw [le_def,sInf_def]
-    simp only [Set.subset_iInter_iff]
-    exact hG
+    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.
@@ -112,22 +112,24 @@ where
   __ := completeLatticeOfInf (AbstractSimplicialComplex V) sInf_isGLB
 
 def unionSubset {s : Set <| AbstractSimplicialComplex V} (hs : s.Nonempty) : AbstractSimplicialComplex V where
-  faces := ⋃ F ∈ s, F.faces
+  faces := ⋃ F : s, F.1.faces
   empty_mem := by
     simp [Set.mem_iUnion]
     rcases hs with ⟨e, he⟩
     exact ⟨e, he, e.empty_mem⟩
-  lower' := isLowerSet_iUnion fun i ↦ isLowerSet_iUnion fun _ ↦ i.lower'
+  lower' := isLowerSet_iUnion fun i ↦ i.1.lower'
 
-lemma sSup_eq_unionSubset {s : Set <| AbstractSimplicialComplex V} (hs : s.Nonempty) : sSup s = unionSubset hs  := by
+lemma sSup_eq_unionSubset {s : Set <| AbstractSimplicialComplex V} (hs : s.Nonempty) : sSup s = unionSubset hs := by
   apply le_antisymm
   · apply sSup_le
     intro b bs
-    refine Set.subset_iUnion_of_subset b (Set.subset_iUnion_of_subset bs (by rfl))
+    rw [le_def, show (unionSubset hs).faces = ⋃ F : s, F.1.faces by rfl]
+    apply Set.subset_iUnion_of_subset ⟨b, bs⟩
+    simp only [subset_of_eq]
   · rw [le_sSup_iff]
     intro b hb
     rw [le_def]
-    exact Set.iUnion_subset fun i ↦ Set.iUnion_subset fun hi ↦ hb hi
+    exact Set.iUnion_subset fun i ↦ hb i.2
 
 def ofEmpty : AbstractSimplicialComplex V where
   faces := {∅}
@@ -139,41 +141,38 @@ 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
 
-theorem bot_faces_eq_empty : (⊥ : AbstractSimplicialComplex V).faces = {∅} := by
+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.faces := by
+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.toSet
+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
+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}  
+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
+  ∀ s ∈ Facets F, ∀ t ∈ Facets F, s.card = t.card
 
 class Pure (F : AbstractSimplicialComplex V) where
-  pure : ∀ s ∈ F.Facets, ∀ t ∈  F.Facets, s.card = t.card
+  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.faces, s.card = d
-  --这个我真心感觉错了，怎么可能Pure‘里面是Facets这里isPure'变成了faces
+def isPure' (F : AbstractSimplicialComplex V) (d : ℕ) :=
   ∀ s ∈ F.Facets, s.card = d
 
 class Pure' (F : AbstractSimplicialComplex V) (d :ℕ) where
@@ -183,29 +182,22 @@ lemma isPure_iff_isPure' {F : AbstractSimplicialComplex V} : F.isPure ↔ ∃ d,
   by_cases hemp : Nonempty F.Facets
   · constructor
     · let s := Classical.choice (hemp)
-      intro hIp
-      use s.1.card
-      intro t ht
-      exact hIp t ht s s.2
-    · intro hIp'
-      obtain ⟨d, hIp'⟩ := hIp'
-      -- rcases hIp' with ⟨d, hIp'⟩ 在这里用rcases和obtain效果是完全一样的
-      intro s hs t ht
+      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
+    · intro; use 0
       simp only [isPure', Finset.card_eq_zero]
       contrapose! hemp
-      rcases hemp with ⟨d, ⟨a, b⟩⟩
+      rcases hemp with ⟨d, ⟨a, _⟩⟩
       use d
-    · intro h
-      rcases h with ⟨d, a⟩
+    · 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
+
+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
 
@@ -214,7 +206,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
@@ -225,6 +216,12 @@ Remark: Here we secretly consider the ambient space as the simplex with vertex s
 abbrev closure (s : Set (Finset V))
   : AbstractSimplicialComplex V := sInf { K | s ⊆  K.faces}
 
+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.
 -/
@@ -233,26 +230,100 @@ lemma closure_simplex (f : Finset V) : closure {f} =  simplex f := by
     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] at 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 => a
     · 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]
+      simp only [Set.singleton_subset_iff, mem_faces, Set.mem_setOf_eq, Set.mem_iInter, Set.coe_setOf, Subtype.forall]
       intro i fi
       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
+
+def closurePower (s: Set (Finset V)) : AbstractSimplicialComplex V where
+  faces :=
+    if Nonempty s then
+      ⨆ f : s, {t | t.toSet ⊆ f}
+    else
+      {∅}
+  empty_mem := by
+    by_cases h : Nonempty s <;> simp [h]
+    exact nonempty_subtype.mp h
+  lower' := by
+    by_cases h : Nonempty s <;> simp [h]
+    · refine isLowerSet_iUnion₂ ?_
+      intro t _
+      intro a b h1 h2
+      refine' Set.Subset.trans ?_ h2
+      congr
+    · exact Finset.isLowerSet_singleton_empty V
+
+theorem Closure_eq_closurePower (s: Set (Finset V)) : closure s = closurePower s := by
+  sorry
+
+-- #check Set.mem_iUnion
+lemma face_closure_eq_iSup (s : Set (Finset V)) : (closure s).faces = ⨆ f ∈ s, (closure {f}).faces := by
+  apply le_antisymm
+  · rw [le_iSup_iff]
+    intro X hX
+    sorry
+
+  · intro X hX
+    have : ∀ (K: AbstractSimplicialComplex V), ∀ (f: Finset V), (f ∈ s) ∧ (s ⊆ K.faces) → {f} ⊆ K.faces := by
+      intro K f hs
+      simp only [Set.singleton_subset_iff]
+      obtain ⟨hs1, hs2⟩ := hs
+      exact hs2 hs1
+    have : ∀ (f: Finset V), (f ∈ s) → (closure {f}).faces ⊆ (closure s).faces := by
+      intro f fs
+      rw [← le_def, le_sInf_iff]
+      intro K Ks
+      apply sInf_le
+      · apply this
+        · rw [Set.iSup_eq_iUnion] at hX
+          simp only [Set.mem_iUnion] at hX
+          exact ⟨fs, Ks⟩
+    rw [Set.iSup_eq_iUnion] at hX
+    simp only [Set.mem_iUnion] at hX
+    rcases hX with ⟨f, hf⟩
+    rw [Set.iSup_eq_iUnion] at hf
+    simp only [Set.mem_iUnion] at hf
+    rcases hf with ⟨f, Xf⟩
+    exact Set.mem_of_subset_of_mem this f Xf
+
+lemma iSup_of_faces_eq_faces_of_iSup  (s : Set (Finset V)) : (⨆ f ∈ s, closure {f}).faces = ⨆ f : s, (closure {f.1}).faces := 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.
 -/
-lemma closure_eq_iSup (s : Set (Finset V)) : closure s =  ⨆ f ∈ s,  closure {f} := by sorry
-  
+lemma closure_eq_iSup (s : Set (Finset V)) : closure s = ⨆ f : s,  closure {f.1} := by
+  apply le_antisymm
+  · rw [le_iSup_iff]
+    intro x hx
+    rw [le_def, closure, sInf_def, ← Set.iInf_eq_iInter, ← Set.le_iff_subset, iInf_le_iff]
+    intro t ht
+    sorry
+  · apply iSup_le
+    intro i
+    apply closure_mono <| Set.singleton_subset_iff.mpr i.2
+
 
 /--
 Lemma: Let F be an ASC. Then the closure of the set of faces is just F.
@@ -261,40 +332,31 @@ lemma closure_self {F : AbstractSimplicialComplex V} : closure (F.faces) = F :=
   have h1 : (closure (F.faces)).faces = F.faces:= by
     apply Set.Subset.antisymm
     · rw [sInf_def]
-      rintro s h1; simp only [Set.mem_setOf_eq, Set.mem_iInter, mem_faces] at h1
+      rintro s h1; simp only [Set.mem_setOf_eq, Set.mem_iInter, mem_faces, Set.coe_setOf, Subtype.forall] at h1
       exact h1 F fun ⦃_⦄ a => a
     · rw [sInf_def]
-      rintro s h1; simp only [Set.mem_setOf_eq, Set.mem_iInter, mem_faces]
+      rintro s h1; simp only [Set.mem_setOf_eq, Set.mem_iInter, mem_faces, Set.coe_setOf, Subtype.forall]
       exact fun _ i => i h1
   exact instSetLikeAbstractSimplicialComplexFinset.proof_1 (closure F.faces) F h1
 
-
-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 closure_le {F : AbstractSimplicialComplex V} (h: s ⊆ F.faces) : closure s ≤ F := by
   rintro s2 h2
-  simp at h2; exact h2 F h
+  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
 
--- instance consPure {h : Cone F G x} : Pure G := by sorry
+-- instance cons_pure {h : Cone F G x} : Pure G := by sorry
 
--- instance consPure' {h : isCone G} : Pure G := by sorry
+-- instance cons_pure' {h : isCone G} : Pure G := by sorry
 
 end AbstractSimplicialComplex

From 6f629455e84521ebaed3927100716f10e75ac9ad Mon Sep 17 00:00:00 2001
From: Haocheng Wang <152980872+hcWang942@users.noreply.github.com>
Date: Wed, 24 Apr 2024 17:41:57 +0800
Subject: [PATCH 3/5] Update AbstractSimplicialComplex.lean

---
 .../ForMathlib/AbstractSimplicialComplex.lean | 44 +++++++++++++++++++
 1 file changed, 44 insertions(+)

diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index 92e7f344..bcda4198 100644
--- a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
+++ b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
@@ -522,5 +522,49 @@ 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
 
+/--
+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 ∪ {x} ∈ G.faces
+
+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 --exact Finset.inter_eq_right.mpr h1
+      · left
+        have : b ⊆ s := by
+          intro y hy
+          have : y ∈ a := h1 hy
+          /-rw [← heq] at this        
+          simp at this
+          refine Or.resolve_right this ?_
+          contrapose! hy
+          rw [hy]
+          exact xinb-/ 
+          aesop
+        exact F.lower' this hs
+        
+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 739d9c45217ef15dafcfa5d16710b0cf0f7ab01f Mon Sep 17 00:00:00 2001
From: Haocheng Wang <152980872+hcWang942@users.noreply.github.com>
Date: Wed, 24 Apr 2024 17:42:57 +0800
Subject: [PATCH 4/5] Update ASCShelling.lean

---
 Coxeter/ForMathlib/ASCShelling.lean | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/Coxeter/ForMathlib/ASCShelling.lean b/Coxeter/ForMathlib/ASCShelling.lean
index cb4d32b6..b13bb1f9 100644
--- a/Coxeter/ForMathlib/ASCShelling.lean
+++ b/Coxeter/ForMathlib/ASCShelling.lean
@@ -39,7 +39,17 @@ 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) := ∃ (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
+def cone_facet_bijection {F G : AbstractSimplicialComplex V} (h : Cone F G x) : Facets F ≃ Facets G := by  
+  sorry
+  
+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??
+    
 
 end AbstractSimplicialComplex

From 62cf7193b355831290c2200a63d68948e4eb6121 Mon Sep 17 00:00:00 2001
From: Wang Haocheng <lpya942@foxmail.com>
Date: Fri, 26 Apr 2024 13:54:26 +0800
Subject: [PATCH 5/5] update cons_cone

---
 Coxeter/ForMathlib/ASCShelling.lean           |  34 ++-
 .../ForMathlib/AbstractSimplicialComplex.lean | 244 ++++++------------
 2 files changed, 100 insertions(+), 178 deletions(-)

diff --git a/Coxeter/ForMathlib/ASCShelling.lean b/Coxeter/ForMathlib/ASCShelling.lean
index cb4d32b6..1d4c58fa 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,32 @@ 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
 
+
 /-- 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
+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??
 
 end AbstractSimplicialComplex
diff --git a/Coxeter/ForMathlib/AbstractSimplicialComplex.lean b/Coxeter/ForMathlib/AbstractSimplicialComplex.lean
index 92e7f344..e8457584 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
 
@@ -103,11 +100,7 @@ lemma sInf_isGLB (s : Set (AbstractSimplicialComplex V)) : IsGLB s (sInf s) := b
 
 /-- instance: The set of all ASCs on `V` is a complete lattice with intersections and unions of the set of faces.
 -/
-<<<<<<< HEAD
-instance completeLattice : CompleteLattice (AbstractSimplicialComplex V)
-=======
 instance instCompleteLatticeToAbstractSimplicialComplex : CompleteLattice (AbstractSimplicialComplex V)
->>>>>>> 3009f323d4d7bbccf9105a3478344f905dd7a4fe
 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 =>
@@ -138,21 +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
 
-<<<<<<< HEAD
-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
-=======
->>>>>>> 3009f323d4d7bbccf9105a3478344f905dd7a4fe
 
 @[simp]
 lemma sSup_faces_of_nonempty {s : Set (AbstractSimplicialComplex V)} (h : s.Nonempty) : (sSup s).faces = ⋃ F : s, F.1.faces := by
@@ -164,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
@@ -178,39 +156,37 @@ 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
 
 /--
 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
+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.
 -/
-<<<<<<< HEAD
-def Facets (F : AbstractSimplicialComplex V) : Set (Finset V) := { s | F.isFacet s}
-=======
 def Facets (F : AbstractSimplicialComplex V) : Set (Finset V) := {s | F.IsFacet s}
->>>>>>> 3009f323d4d7bbccf9105a3478344f905dd7a4fe
 
 /-- Definition: A pure abstract simplicial complex is an abstract simplicial complex
     where all facets have the same cardinality. -/
-def isPure (F : AbstractSimplicialComplex V) :=
+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 : ℕ) :=
+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
+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)
@@ -219,19 +195,22 @@ lemma isPure_iff_isPure' {F : AbstractSimplicialComplex V} : F.isPure ↔ ∃ d,
       rw [hIp' s hs, hIp' t ht]
   · constructor
     · intro; use 0
-      simp only [isPure', Finset.card_eq_zero]
+      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
+      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
 
-lemma pure_isPure {F : AbstractSimplicialComplex V} [Pure F] : isPure F := pure_def
+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.
@@ -245,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}
@@ -256,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
@@ -266,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]
@@ -281,28 +260,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
 
-<<<<<<< HEAD
-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
-
-def closurePower (s: Set (Finset V)) : AbstractSimplicialComplex V where
-=======
 /-- Explicit construction of `closure s` for `s : Set (Finset V)`-/
 def closurePower (s : Set (Finset V)) : AbstractSimplicialComplex V where
->>>>>>> 3009f323d4d7bbccf9105a3478344f905dd7a4fe
   faces :=
     if Nonempty s then
-      ⋃ f : s, {t | t ⊆ f}
+      ⋃ f : s, {t | t.toSet ⊆ f}
     else
       {∅}
   empty_mem := by
@@ -311,22 +273,15 @@ 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
 
-<<<<<<< HEAD
-theorem Closure_eq_closurePower (s: Set (Finset V)) : closure s = closurePower s := by
-  sorry
-
--- #check Set.mem_iUnion
-lemma face_closure_eq_iSup (s : Set (Finset V)) : (closure s).faces = ⨆ f ∈ s, (closure {f}).faces := by
-=======
 /-- 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
->>>>>>> 3009f323d4d7bbccf9105a3478344f905dd7a4fe
   apply le_antisymm
   · apply sInf_le
     simp only [Set.iUnion_subset_iff, Set.mem_setOf_eq]
@@ -349,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
@@ -364,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 _⟩
 
 /--
@@ -417,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]
@@ -478,49 +385,50 @@ 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