Thomason model structures and nerve detection in all positive strict dimensions

import Mathlib/-! Definitions for the Thomason model structures and their Street-nerve detection statement. -/noncomputable sectionuniverse u v wsectionnamespace OAI.Thomasonstructure OmegaCategory where  Cell : Type u  source : ℕ → Cell → Cell  target : ℕ → Cell → Cell  source_source (i j : ℕ) (x : Cell) : source i (source j x) = source (min i j) x  target_target (i j : ℕ) (x : Cell) : target i (target j x) = target (min i j) x  source_target (i j : ℕ) (x : Cell) :    source i (target j x) = if i < j then source i x else target j x  target_source (i j : ℕ) (x : Cell) :    target i (source j x) = if i < j then target i x else source j x  comp (k : ℕ) (x y : Cell) : target k x = source k y → Cell  source_comp_le (i k : ℕ) (hik : i ≤ k) (x y : Cell)      (h : target k x = source k y) : source i (comp k x y h) = source i x  target_comp_le (i k : ℕ) (hik : i ≤ k) (x y : Cell)      (h : target k x = source k y) : target i (comp k x y h) = target i y  source_comp_gt (i k : ℕ) (hki : k < i) (x y : Cell)      (h : target k x = source k y)      (hs : target k (source i x) = source k (source i y)) :    source i (comp k x y h) = comp k (source i x) (source i y) hs  target_comp_gt (i k : ℕ) (hki : k < i) (x y : Cell)      (h : target k x = source k y)      (ht : target k (target i x) = source k (target i y)) :    target i (comp k x y h) = comp k (target i x) (target i y) ht  unit_left (k : ℕ) (x : Cell) (h : target k (source k x) = source k x) :    comp k (source k x) x h = x  unit_right (k : ℕ) (x : Cell) (h : target k x = source k (target k x)) :    comp k x (target k x) h = x  assoc (k : ℕ) (x y z : Cell)      (hxy : target k x = source k y) (hyz : target k y = source k z)      (hxy_z : target k (comp k x y hxy) = source k z)      (hx_yz : target k x = source k (comp k y z hyz)) :    comp k (comp k x y hxy) z hxy_z = comp k x (comp k y z hyz) hx_yz  interchange (k l : ℕ) (hkl : k < l) (a b c d : Cell)      (hab : target l a = source l b) (hcd : target l c = source l d)      (hac : target k a = source k c) (hbd : target k b = source k d)      (hab_cd : target k (comp l a b hab) = source k (comp l c d hcd))      (hac_bd : target l (comp k a c hac) = source l (comp k b d hbd)) :    comp k (comp l a b hab) (comp l c d hcd) hab_cd =      comp l (comp k a c hac) (comp k b d hbd) hac_bd  finite_dimension (x : Cell) : ∃ k, source k x = xend OAI.Thomasonendsectionnamespace OAI.Thomason.OmegaCategoryvariable (C : OmegaCategory.{u})@[ext]structure Functor (C : OAI.Thomason.OmegaCategory.{u}) (D : OAI.Thomason.OmegaCategory.{v}) where  map : C.Cell → D.Cell  map_source (k : ℕ) (x : C.Cell) : map (C.source k x) = D.source k (map x)  map_target (k : ℕ) (x : C.Cell) : map (C.target k x) = D.target k (map x)  map_comp (k : ℕ) (x y : C.Cell) (h : C.target k x = C.source k y)      (h' : D.target k (map x) = D.source k (map y)) :    map (C.comp k x y h) = D.comp k (map x) (map y) h'end OAI.Thomason.OmegaCategoryendsectionnamespace OAI.Thomason.OmegaCategory.Functorvariable (C : OmegaCategory.{u})variable {C : OmegaCategory.{u}} {D : OmegaCategory.{v}} {B : OmegaCategory.{w}}noncomputable def id (C : OAI.Thomason.OmegaCategory.{u}) : OAI.Thomason.OmegaCategory.Functor C C where  map x := x  map_source _ _ := rfl  map_target _ _ := rfl  map_comp _ _ _ _ _ := rflnoncomputable def comp (F : OAI.Thomason.OmegaCategory.Functor C D) (G : OAI.Thomason.OmegaCategory.Functor D B) : OAI.Thomason.OmegaCategory.Functor C B := by  classical  have proof_map_composable_0 {C : OAI.Thomason.OmegaCategory.{u}} {D : OAI.Thomason.OmegaCategory.{v}}  (F : OAI.Thomason.OmegaCategory.Functor C D) {k : ℕ} {x y : C.Cell}      (h : C.target k x = C.source k y) :      D.target k (F.map x) = D.source k (F.map y) := by    rw [← F.map_target, ← F.map_source, h]  exact {    map x := G.map (F.map x)    map_source k x := by rw [F.map_source, G.map_source]    map_target k x := by rw [F.map_target, G.map_target]    map_comp k x y h h' := by      rw [F.map_comp k x y h (proof_map_composable_0 F h), G.map_comp]  }end OAI.Thomason.OmegaCategory.Functorendsectionnamespace OAI.Thomason.OmegaCategoryvariable (C : OmegaCategory.{u})noncomputable instance : CategoryTheory.Category OAI.Thomason.OmegaCategory.{u} where  Hom C D := OAI.Thomason.OmegaCategory.Functor C D  id := OAI.Thomason.OmegaCategory.Functor.id  comp := OAI.Thomason.OmegaCategory.Functor.compnoncomputable def IsTruncated (n : ℕ) : Prop := ∀ x : C.Cell, C.source n x = xnoncomputable def NCategory (n : ℕ) := {C : OAI.Thomason.OmegaCategory.{u} // C.IsTruncated n}noncomputable instance (n : ℕ) : CategoryTheory.Category (OAI.Thomason.OmegaCategory.NCategory.{u} n) where  Hom C D := OAI.Thomason.OmegaCategory.Functor C.val D.val  id C := OAI.Thomason.OmegaCategory.Functor.id C.val  comp := OAI.Thomason.OmegaCategory.Functor.compend OAI.Thomason.OmegaCategoryendsectionnamespace OAI.Thomasonstructure DirectedComplex where  Chain : ℕ → Type u  group : ∀ p, AddCommGroup (Chain p)  d : (p : ℕ) → Chain (p+1) →+ Chain p  d_d (p : ℕ) (x : Chain (p+2)) : d p (d (p+1) x) = 0  augmentation : Chain 0 →+ ℤ  augmentation_d (x : Chain 1) : augmentation (d 0 x) = 0  positive : (p : ℕ) → AddSubmonoid (Chain p)end OAI.Thomasonendattribute [instance] OAI.Thomason.DirectedComplex.groupsectionnamespace OAI.Thomason.DirectedComplex@[ext]structure Hom (K : OAI.Thomason.DirectedComplex.{u}) (L : OAI.Thomason.DirectedComplex.{v}) where  map (p : ℕ) : K.Chain p →+ L.Chain p  map_d (p : ℕ) (x : K.Chain (p+1)) : map p (K.d p x) = L.d p (map (p+1) x)  map_augmentation (x : K.Chain 0) : L.augmentation (map 0 x) = K.augmentation x  map_positive (p : ℕ) (x : K.Chain p) : x ∈ K.positive p → map p x ∈ L.positive pend OAI.Thomason.DirectedComplexendsectionnamespace OAI.Thomason.DirectedComplex.Homvariable {K : DirectedComplex.{u}} {L : DirectedComplex.{v}} {M : DirectedComplex.{w}}noncomputable def id (K : OAI.Thomason.DirectedComplex.{u}) : OAI.Thomason.DirectedComplex.Hom K K where  map _ := AddMonoidHom.id _  map_d _ _ := rfl  map_augmentation _ := rfl  map_positive _ _ h := hnoncomputable def comp (f : OAI.Thomason.DirectedComplex.Hom K L) (g : OAI.Thomason.DirectedComplex.Hom L M) : OAI.Thomason.DirectedComplex.Hom K M where  map p := (g.map p).comp (f.map p)  map_d p x := by simp only [AddMonoidHom.comp_apply, f.map_d, g.map_d]  map_augmentation x := by simp only [AddMonoidHom.comp_apply,    g.map_augmentation, f.map_augmentation]  map_positive p x hx := g.map_positive p _ (f.map_positive p x hx)end OAI.Thomason.DirectedComplex.Homendsectionnamespace OAI.Thomason.DirectedComplexnoncomputable instance : CategoryTheory.Category OAI.Thomason.DirectedComplex.{u} where  Hom := OAI.Thomason.DirectedComplex.Hom  id := OAI.Thomason.DirectedComplex.Hom.id  comp := OAI.Thomason.DirectedComplex.Hom.comp@[ext]structure Table (K : OAI.Thomason.DirectedComplex.{u}) where  row : (p : ℕ) → Bool → K.Chain p  positive (p : ℕ) (b : Bool) : row p b ∈ K.positive p  boundary (p : ℕ) (b : Bool) :    K.d p (row (p+1) b) = row p true - row p false  augmentation (b : Bool) : K.augmentation (row 0 b) = 1  bounded : ∃ k, ∀ p, k < p → ∀ b, row p b = 0end OAI.Thomason.DirectedComplexendsectionnamespace OAI.Thomason.DirectedComplex.Tablevariable {K : DirectedComplex.{u}}noncomputable def truncate (k : ℕ) (e : Bool) (x : OAI.Thomason.DirectedComplex.Table K) : OAI.Thomason.DirectedComplex.Table K where  row p b := if p < k then x.row p b else if p = k then x.row p e else 0  positive p b := by    split_ifs <;> first | exact x.positive _ _ | exact (K.positive _).zero_mem  boundary p b := by    by_cases hp : p < k    · by_cases hp' : p+1 < k      · simp only [hp, hp', ite_eq_left]        exact x.boundary p b      · have he : p+1 = k := by omega        simp only [ite_eq_left hp, ite_eq_right hp', ite_eq_left he]        exact x.boundary p e    · by_cases he : p = k      · have hp' : ¬p+1 < k := by omega        have he' : ¬p+1 = k := by omega        simp only [ite_eq_right hp, ite_eq_right hp', ite_eq_right he', ite_eq_left he, map_zero, sub_self]      · have hp' : ¬p+1 < k := by omega        have he' : ¬p+1 = k := by omega        simp only [hp, hp', he', he, ite_false, map_zero, sub_self]  augmentation b := by    by_cases hk : k = 0    · subst k      simpa using x.augmentation e    · have hk' : 0 < k := Nat.pos_of_ne_zero hk      simpa only [hk', ite_eq_left] using x.augmentation b  bounded := by    refine ⟨k, ?_⟩    intro p hp b    simp only [show ¬p < k by omega, show ¬p = k by omega, ite_false]noncomputable def comp (k : ℕ) (x y : OAI.Thomason.DirectedComplex.Table K)    (h : OAI.Thomason.DirectedComplex.Table.truncate k true x = OAI.Thomason.DirectedComplex.Table.truncate k false y) : OAI.Thomason.DirectedComplex.Table K := by  classical  have proof_truncate_row_3 {K : OAI.Thomason.DirectedComplex.{u}}  (k : ℕ) (e : Bool) (x : OAI.Thomason.DirectedComplex.Table K) (p : ℕ) (b : Bool) :      (OAI.Thomason.DirectedComplex.Table.truncate k e x).row p b =        if p < k then x.row p b else if p = k then x.row p e else 0 := rfl  have proof_lower_rows_eq_1 {K : OAI.Thomason.DirectedComplex.{u}}  {k : ℕ} {x y : OAI.Thomason.DirectedComplex.Table K}      (h : OAI.Thomason.DirectedComplex.Table.truncate k true x = OAI.Thomason.DirectedComplex.Table.truncate k false y) {p : ℕ} (hp : p < k) (b : Bool) :      x.row p b = y.row p b := by    have hr := congrArg (fun z : OAI.Thomason.DirectedComplex.Table K => z.row p b) h    simpa only [OAI.Thomason.DirectedComplex.Table.truncate, hp, ite_eq_left] using hr  have proof_matching_row_eq_2 {K : OAI.Thomason.DirectedComplex.{u}}  {k : ℕ} {x y : OAI.Thomason.DirectedComplex.Table K}      (h : OAI.Thomason.DirectedComplex.Table.truncate k true x = OAI.Thomason.DirectedComplex.Table.truncate k false y) : x.row k true = y.row k false := by    have hr := congrArg (fun z : OAI.Thomason.DirectedComplex.Table K => z.row k false) h    simpa [OAI.Thomason.DirectedComplex.Table.truncate] using hr  exact {    row p b := if p < k then x.row p b else if p = k then      (if b then y.row p true else x.row p false) else x.row p b + y.row p b    positive p b := by      split_ifs <;> first        | exact x.positive _ _        | exact y.positive _ _        | exact (K.positive _).add_mem (x.positive _ _) (y.positive _ _)    boundary p b := by      by_cases hp : p < k      · by_cases hp' : p+1 < k        · simp only [ite_eq_left hp, ite_eq_left hp']          exact x.boundary p b        · have he : p+1 = k := by omega          simp only [ite_eq_left hp, ite_eq_right hp', ite_eq_left he]          cases b with          | false => exact x.boundary p false          | true =>            change K.d p (y.row (p+1) true) = x.row p true - x.row p false            rw [y.boundary, proof_lower_rows_eq_1 h hp true, proof_lower_rows_eq_1 h hp false]      · by_cases he : p = k        · subst p          have hp' : ¬k+1 < k := by omega          have he' : ¬k+1 = k := by omega          simp only [ite_eq_right (Nat.lt_irrefl k), ite_eq_right hp', ite_eq_right he',            ↓reduceIte, map_add, x.boundary, y.boundary]          rw [proof_matching_row_eq_2 h]          abel_nf          exact add_comm _ _        · have hp' : ¬p+1 < k := by omega          have he' : ¬p+1 = k := by omega          simp only [ite_eq_right hp, ite_eq_right hp', ite_eq_right he', ite_eq_right he, map_add,            x.boundary, y.boundary]          abel    augmentation b := by      by_cases hk : 0 < k      · simp only [ite_eq_left hk]        exact x.augmentation b      · have he : 0 = k := by omega        simp only [ite_eq_right hk, ite_eq_left he]        cases b <;> first | exact x.augmentation _ | exact y.augmentation _    bounded := by      obtain ⟨nx, hx⟩ := x.bounded      obtain ⟨ny, hy⟩ := y.bounded      refine ⟨max nx ny, ?_⟩      intro p hp b      have hx' := hx p (lt_of_le_of_lt (le_max_left _ _) hp)      have hy' := hy p (lt_of_le_of_lt (le_max_right _ _) hp)      split_ifs <;> simp only [hx', hy', zero_add]  }end OAI.Thomason.DirectedComplex.Tableendsectionnamespace OAI.Thomason.DirectedComplexnoncomputable def nu (K : OAI.Thomason.DirectedComplex.{u}) : OAI.Thomason.OmegaCategory.{u} := by  classical  have proof_truncate_row_3 {K : OAI.Thomason.DirectedComplex.{u}}  (k : ℕ) (e : Bool) (x : OAI.Thomason.DirectedComplex.Table K) (p : ℕ) (b : Bool) :      (OAI.Thomason.DirectedComplex.Table.truncate k e x).row p b =        if p < k then x.row p b else if p = k then x.row p e else 0 := rfl  have proof_truncate_truncate_5 {K : OAI.Thomason.DirectedComplex.{u}}  (i j : ℕ) (e f : Bool) (x : OAI.Thomason.DirectedComplex.Table K) :      OAI.Thomason.DirectedComplex.Table.truncate i e (OAI.Thomason.DirectedComplex.Table.truncate j f x) =        if i < j then OAI.Thomason.DirectedComplex.Table.truncate i e x else OAI.Thomason.DirectedComplex.Table.truncate j f x := by    ext p b    by_cases hij : i < j    · simp only [hij, ite_eq_left, OAI.Thomason.DirectedComplex.Table.truncate]      by_cases hpi : p < i      · have hpj : p < j := lt_trans hpi hij        simp [hpi, hpj]      · by_cases hpe : p = i        · subst p          simp [hij]        · simp [hpi, hpe]    · simp only [hij, ite_false, OAI.Thomason.DirectedComplex.Table.truncate]      by_cases hpj : p < j      · have hpi : p < i := by omega        simp [hpj, hpi]      · by_cases hpje : p = j        · subst p          by_cases hji : j < i          · simp [hji]          · have hi : i = j := by omega            subst i            simp []        · by_cases hpi : p < i          · simp [hpi, hpj, hpje]          · by_cases hpie : p = i            · subst p              simp [hij]            · simp [hpi, hpie, hpj, hpje]  have proof_truncate_truncate_same_4 {K : OAI.Thomason.DirectedComplex.{u}}  (i j : ℕ) (e : Bool) (x : OAI.Thomason.DirectedComplex.Table K) :      OAI.Thomason.DirectedComplex.Table.truncate i e (OAI.Thomason.DirectedComplex.Table.truncate j e x) = OAI.Thomason.DirectedComplex.Table.truncate (min i j) e x := by    rw [proof_truncate_truncate_5]    split_ifs with h    · rw [min_eq_left (le_of_lt h)]    · rw [min_eq_right (le_of_not_gt h)]  have proof_comp_row_14 {K : OAI.Thomason.DirectedComplex.{u}}  (k : ℕ) (x y : OAI.Thomason.DirectedComplex.Table K)      (h : OAI.Thomason.DirectedComplex.Table.truncate k true x = OAI.Thomason.DirectedComplex.Table.truncate k false y) (p : ℕ) (b : Bool) :      (OAI.Thomason.DirectedComplex.Table.comp k x y h).row p b = if p < k then x.row p b else if p = k then        (if b then y.row p true else x.row p false) else x.row p b + y.row p b := rfl  have proof_source_comp_le_6 {K : OAI.Thomason.DirectedComplex.{u}}  (i k : ℕ) (hik : i ≤ k) (x y : OAI.Thomason.DirectedComplex.Table K)      (h : OAI.Thomason.DirectedComplex.Table.truncate k true x = OAI.Thomason.DirectedComplex.Table.truncate k false y) :      OAI.Thomason.DirectedComplex.Table.truncate i false (OAI.Thomason.DirectedComplex.Table.comp k x y h) = OAI.Thomason.DirectedComplex.Table.truncate i false x := by    ext p b    by_cases hpi : p < i    · have hpk : p < k := lt_of_lt_of_le hpi hik      simp [OAI.Thomason.DirectedComplex.Table.truncate, OAI.Thomason.DirectedComplex.Table.comp, hpi, hpk]    · by_cases hpe : p = i      · subst p        by_cases hik' : i < k        · simp [OAI.Thomason.DirectedComplex.Table.truncate, OAI.Thomason.DirectedComplex.Table.comp, hik']        · have he : i = k := by omega          subst i          simp [OAI.Thomason.DirectedComplex.Table.truncate, OAI.Thomason.DirectedComplex.Table.comp]      · simp [OAI.Thomason.DirectedComplex.Table.truncate, OAI.Thomason.DirectedComplex.Table.comp, hpi, hpe]  have proof_lower_rows_eq_1 {K : OAI.Thomason.DirectedComplex.{u}}  {k : ℕ} {x y : OAI.Thomason.DirectedComplex.Table K}      (h : OAI.Thomason.DirectedComplex.Table.truncate k true x = OAI.Thomason.DirectedComplex.Table.truncate k false y) {p : ℕ} (hp : p < k) (b : Bool) :      x.row p b = y.row p b := by    have hr := congrArg (fun z : OAI.Thomason.DirectedComplex.Table K => z.row p b) h    simpa only [OAI.Thomason.DirectedComplex.Table.truncate, hp, ite_eq_left] using hr  have proof_target_comp_le_7 {K : OAI.Thomason.DirectedComplex.{u}}  (i k : ℕ) (hik : i ≤ k) (x y : OAI.Thomason.DirectedComplex.Table K)      (h : OAI.Thomason.DirectedComplex.Table.truncate k true x = OAI.Thomason.DirectedComplex.Table.truncate k false y) :      OAI.Thomason.DirectedComplex.Table.truncate i true (OAI.Thomason.DirectedComplex.Table.comp k x y h) = OAI.Thomason.DirectedComplex.Table.truncate i true y := by    ext p b    by_cases hpi : p < i    · have hpk : p < k := lt_of_lt_of_le hpi hik      simp only [OAI.Thomason.DirectedComplex.Table.truncate, ite_eq_left hpi, OAI.Thomason.DirectedComplex.Table.comp, ite_eq_left hpk]      exact proof_lower_rows_eq_1 h hpk b    · by_cases hpe : p = i      · subst p        by_cases hik' : i < k        · simpa [OAI.Thomason.DirectedComplex.Table.truncate, OAI.Thomason.DirectedComplex.Table.comp, hik'] using proof_lower_rows_eq_1 h hik' true        · have he : i = k := by omega          subst i          simp [OAI.Thomason.DirectedComplex.Table.truncate, OAI.Thomason.DirectedComplex.Table.comp]      · simp [OAI.Thomason.DirectedComplex.Table.truncate, OAI.Thomason.DirectedComplex.Table.comp, hpi, hpe]  have proof_truncate_comp_gt_8 {K : OAI.Thomason.DirectedComplex.{u}}  (i k : ℕ) (hki : k < i) (e : Bool) (x y : OAI.Thomason.DirectedComplex.Table K)      (h : OAI.Thomason.DirectedComplex.Table.truncate k true x = OAI.Thomason.DirectedComplex.Table.truncate k false y)      (h' : OAI.Thomason.DirectedComplex.Table.truncate k true (OAI.Thomason.DirectedComplex.Table.truncate i e x) = OAI.Thomason.DirectedComplex.Table.truncate k false (OAI.Thomason.DirectedComplex.Table.truncate i e y)) :      OAI.Thomason.DirectedComplex.Table.truncate i e (OAI.Thomason.DirectedComplex.Table.comp k x y h) = OAI.Thomason.DirectedComplex.Table.comp k (OAI.Thomason.DirectedComplex.Table.truncate i e x) (OAI.Thomason.DirectedComplex.Table.truncate i e y) h' := by    ext p b    by_cases hpk : p < k    · have hpi : p < i := lt_trans hpk hki      simp [OAI.Thomason.DirectedComplex.Table.truncate, OAI.Thomason.DirectedComplex.Table.comp, hpk, hpi]    · by_cases hpe : p = k      · subst p        simp [OAI.Thomason.DirectedComplex.Table.truncate, OAI.Thomason.DirectedComplex.Table.comp, hki]      · by_cases hpi : p < i        · simp [OAI.Thomason.DirectedComplex.Table.truncate, OAI.Thomason.DirectedComplex.Table.comp, hpk, hpe, hpi]        · by_cases hpie : p = i          · subst p            have hik : ¬i < k := by omega            have hie : ¬i = k := by omega            simp [OAI.Thomason.DirectedComplex.Table.truncate, OAI.Thomason.DirectedComplex.Table.comp, hik, hie]          · simp [OAI.Thomason.DirectedComplex.Table.truncate, OAI.Thomason.DirectedComplex.Table.comp, hpk, hpe, hpi, hpie]  have proof_unit_left_9 {K : OAI.Thomason.DirectedComplex.{u}}  (k : ℕ) (x : OAI.Thomason.DirectedComplex.Table K)      (h : OAI.Thomason.DirectedComplex.Table.truncate k true (OAI.Thomason.DirectedComplex.Table.truncate k false x) = OAI.Thomason.DirectedComplex.Table.truncate k false x) :      OAI.Thomason.DirectedComplex.Table.comp k (OAI.Thomason.DirectedComplex.Table.truncate k false x) x h = x := by    ext p b    by_cases hp : p < k    · simp [OAI.Thomason.DirectedComplex.Table.truncate, OAI.Thomason.DirectedComplex.Table.comp, hp]    · by_cases he : p = k      · subst p        cases b <;> simp [OAI.Thomason.DirectedComplex.Table.truncate, OAI.Thomason.DirectedComplex.Table.comp]      · simp [OAI.Thomason.DirectedComplex.Table.truncate, OAI.Thomason.DirectedComplex.Table.comp, hp, he]  have proof_unit_right_10 {K : OAI.Thomason.DirectedComplex.{u}}  (k : ℕ) (x : OAI.Thomason.DirectedComplex.Table K)      (h : OAI.Thomason.DirectedComplex.Table.truncate k true x = OAI.Thomason.DirectedComplex.Table.truncate k false (OAI.Thomason.DirectedComplex.Table.truncate k true x)) :      OAI.Thomason.DirectedComplex.Table.comp k x (OAI.Thomason.DirectedComplex.Table.truncate k true x) h = x := by    ext p b    by_cases hp : p < k    · simp [OAI.Thomason.DirectedComplex.Table.truncate, OAI.Thomason.DirectedComplex.Table.comp, hp]    · by_cases he : p = k      · subst p        cases b <;> simp [OAI.Thomason.DirectedComplex.Table.truncate, OAI.Thomason.DirectedComplex.Table.comp]      · simp [OAI.Thomason.DirectedComplex.Table.truncate, OAI.Thomason.DirectedComplex.Table.comp, hp, he]  have proof_assoc_11 {K : OAI.Thomason.DirectedComplex.{u}}  (k : ℕ) (x y z : OAI.Thomason.DirectedComplex.Table K)      (hxy : OAI.Thomason.DirectedComplex.Table.truncate k true x = OAI.Thomason.DirectedComplex.Table.truncate k false y)      (hyz : OAI.Thomason.DirectedComplex.Table.truncate k true y = OAI.Thomason.DirectedComplex.Table.truncate k false z)      (hxy_z : OAI.Thomason.DirectedComplex.Table.truncate k true (OAI.Thomason.DirectedComplex.Table.comp k x y hxy) = OAI.Thomason.DirectedComplex.Table.truncate k false z)      (hx_yz : OAI.Thomason.DirectedComplex.Table.truncate k true x = OAI.Thomason.DirectedComplex.Table.truncate k false (OAI.Thomason.DirectedComplex.Table.comp k y z hyz)) :      OAI.Thomason.DirectedComplex.Table.comp k (OAI.Thomason.DirectedComplex.Table.comp k x y hxy) z hxy_z = OAI.Thomason.DirectedComplex.Table.comp k x (OAI.Thomason.DirectedComplex.Table.comp k y z hyz) hx_yz := by    ext p b    by_cases hp : p < k    · simp [OAI.Thomason.DirectedComplex.Table.comp, hp]    · by_cases he : p = k      · subst p        cases b <;> simp [OAI.Thomason.DirectedComplex.Table.comp]      · simp [OAI.Thomason.DirectedComplex.Table.comp, hp, he, add_assoc]  have proof_interchange_12 {K : OAI.Thomason.DirectedComplex.{u}}  (k l : ℕ) (hkl : k < l) (a b c d : OAI.Thomason.DirectedComplex.Table K)      (hab : OAI.Thomason.DirectedComplex.Table.truncate l true a = OAI.Thomason.DirectedComplex.Table.truncate l false b)      (hcd : OAI.Thomason.DirectedComplex.Table.truncate l true c = OAI.Thomason.DirectedComplex.Table.truncate l false d)      (hac : OAI.Thomason.DirectedComplex.Table.truncate k true a = OAI.Thomason.DirectedComplex.Table.truncate k false c)      (hbd : OAI.Thomason.DirectedComplex.Table.truncate k true b = OAI.Thomason.DirectedComplex.Table.truncate k false d)      (hab_cd : OAI.Thomason.DirectedComplex.Table.truncate k true (OAI.Thomason.DirectedComplex.Table.comp l a b hab) = OAI.Thomason.DirectedComplex.Table.truncate k false (OAI.Thomason.DirectedComplex.Table.comp l c d hcd))      (hac_bd : OAI.Thomason.DirectedComplex.Table.truncate l true (OAI.Thomason.DirectedComplex.Table.comp k a c hac) = OAI.Thomason.DirectedComplex.Table.truncate l false (OAI.Thomason.DirectedComplex.Table.comp k b d hbd)) :      OAI.Thomason.DirectedComplex.Table.comp k (OAI.Thomason.DirectedComplex.Table.comp l a b hab) (OAI.Thomason.DirectedComplex.Table.comp l c d hcd) hab_cd =        OAI.Thomason.DirectedComplex.Table.comp l (OAI.Thomason.DirectedComplex.Table.comp k a c hac) (OAI.Thomason.DirectedComplex.Table.comp k b d hbd) hac_bd := by    ext p e    by_cases hpk : p < k    · have hpl : p < l := lt_trans hpk hkl      simp [OAI.Thomason.DirectedComplex.Table.comp, hpk, hpl]    · by_cases hpe : p = k      · subst p        cases e <;> simp [OAI.Thomason.DirectedComplex.Table.comp, hkl]      · by_cases hpl : p < l        · simp [OAI.Thomason.DirectedComplex.Table.comp, hpk, hpe, hpl]        · by_cases hple : p = l          · subst p            have hlk : ¬l < k := by omega            have hlke : ¬l = k := by omega            cases e <;> simp [OAI.Thomason.DirectedComplex.Table.comp, hlk, hlke]          · simp only [OAI.Thomason.DirectedComplex.Table.comp, ite_eq_right hpk, ite_eq_right hpe, ite_eq_right hpl, ite_eq_right hple]            abel  have proof_finite_dimension_13 {K : OAI.Thomason.DirectedComplex.{u}}  (x : OAI.Thomason.DirectedComplex.Table K) : ∃ k, OAI.Thomason.DirectedComplex.Table.truncate k false x = x := by    obtain ⟨k, hk⟩ := x.bounded    have ht : x.row k true = x.row k false := by      have hb := x.boundary k false      rw [hk (k+1) (by omega) false, map_zero] at hb      exact sub_eq_zero.mp hb.symm    refine ⟨k, ?_⟩    ext p b    by_cases hp : p < k    · simp [OAI.Thomason.DirectedComplex.Table.truncate, hp]    · by_cases he : p = k      · subst p        cases b <;> simp [OAI.Thomason.DirectedComplex.Table.truncate, ht]      · have hkp : k < p := by omega        simp [OAI.Thomason.DirectedComplex.Table.truncate, hp, he, hk p hkp b]  exact {    Cell := OAI.Thomason.DirectedComplex.Table K    source k := OAI.Thomason.DirectedComplex.Table.truncate k false    target k := OAI.Thomason.DirectedComplex.Table.truncate k true    source_source i j x := proof_truncate_truncate_same_4 i j false x    target_target i j x := proof_truncate_truncate_same_4 i j true x    source_target i j x := proof_truncate_truncate_5 i j false true x    target_source i j x := proof_truncate_truncate_5 i j true false x    comp := OAI.Thomason.DirectedComplex.Table.comp    source_comp_le := proof_source_comp_le_6    target_comp_le := proof_target_comp_le_7    source_comp_gt i k hki x y h hs := proof_truncate_comp_gt_8 i k hki false x y h hs    target_comp_gt i k hki x y h ht := proof_truncate_comp_gt_8 i k hki true x y h ht    unit_left := proof_unit_left_9    unit_right := proof_unit_right_10    assoc := proof_assoc_11    interchange := proof_interchange_12    finite_dimension := proof_finite_dimension_13  }end OAI.Thomason.DirectedComplexendsectionnamespace OAI.Thomason.DirectedComplex.Homvariable {K : DirectedComplex.{u}} {L : DirectedComplex.{v}} {M : DirectedComplex.{w}}noncomputable def table (f : OAI.Thomason.DirectedComplex.Hom K L) (x : OAI.Thomason.DirectedComplex.Table K) : OAI.Thomason.DirectedComplex.Table L where  row p b := f.map p (x.row p b)  positive p b := f.map_positive p _ (x.positive p b)  boundary p b := by rw [← f.map_d, x.boundary, map_sub]  augmentation b := by rw [f.map_augmentation, x.augmentation]  bounded := by    obtain ⟨k, hk⟩ := x.bounded    refine ⟨k, ?_⟩    intro p hp b    rw [hk p hp b, map_zero]noncomputable def nu (f : OAI.Thomason.DirectedComplex.Hom K L) : OAI.Thomason.OmegaCategory.Functor K.nu L.nu := by  classical  have proof_table_row_17 {K : OAI.Thomason.DirectedComplex.{u}} {L : OAI.Thomason.DirectedComplex.{v}}  (f : OAI.Thomason.DirectedComplex.Hom K L) (x : OAI.Thomason.DirectedComplex.Table K) (p : ℕ) (b : Bool) :      (f.table x).row p b = f.map p (x.row p b) := rfl  have proof_truncate_row_3 {K : OAI.Thomason.DirectedComplex.{u}}  (k : ℕ) (e : Bool) (x : OAI.Thomason.DirectedComplex.Table K) (p : ℕ) (b : Bool) :      (OAI.Thomason.DirectedComplex.Table.truncate k e x).row p b =        if p < k then x.row p b else if p = k then x.row p e else 0 := rfl  have proof_table_truncate_15 {K : OAI.Thomason.DirectedComplex.{u}} {L : OAI.Thomason.DirectedComplex.{v}}  (f : OAI.Thomason.DirectedComplex.Hom K L) (k : ℕ) (b : Bool) (x : OAI.Thomason.DirectedComplex.Table K) :      f.table (OAI.Thomason.DirectedComplex.Table.truncate k b x) = OAI.Thomason.DirectedComplex.Table.truncate k b (f.table x) := by    ext p e    simp only [OAI.Thomason.DirectedComplex.Hom.table, OAI.Thomason.DirectedComplex.Table.truncate]    split_ifs <;> simp only [map_zero]  have proof_comp_row_14 {K : OAI.Thomason.DirectedComplex.{u}}  (k : ℕ) (x y : OAI.Thomason.DirectedComplex.Table K)      (h : OAI.Thomason.DirectedComplex.Table.truncate k true x = OAI.Thomason.DirectedComplex.Table.truncate k false y) (p : ℕ) (b : Bool) :      (OAI.Thomason.DirectedComplex.Table.comp k x y h).row p b = if p < k then x.row p b else if p = k then        (if b then y.row p true else x.row p false) else x.row p b + y.row p b := rfl  have proof_table_comp_16 {K : OAI.Thomason.DirectedComplex.{u}} {L : OAI.Thomason.DirectedComplex.{v}}  (f : OAI.Thomason.DirectedComplex.Hom K L) (k : ℕ) (x y : OAI.Thomason.DirectedComplex.Table K)      (h : OAI.Thomason.DirectedComplex.Table.truncate k true x = OAI.Thomason.DirectedComplex.Table.truncate k false y)      (h' : OAI.Thomason.DirectedComplex.Table.truncate k true (f.table x) = OAI.Thomason.DirectedComplex.Table.truncate k false (f.table y)) :      f.table (OAI.Thomason.DirectedComplex.Table.comp k x y h) = OAI.Thomason.DirectedComplex.Table.comp k (f.table x) (f.table y) h' := by    ext p e    simp only [OAI.Thomason.DirectedComplex.Hom.table, OAI.Thomason.DirectedComplex.Table.comp]    split_ifs <;> simp only [map_add]  exact {    map := f.table    map_source k x := (proof_table_truncate_15 f k Bool.false x)    map_target k x := (proof_table_truncate_15 f k Bool.true x)    map_comp := (proof_table_comp_16 f)  }end OAI.Thomason.DirectedComplex.Homendsectionnamespace OAI.Thomason.DirectedComplexnoncomputable def nuFunctor : CategoryTheory.Functor OAI.Thomason.DirectedComplex.{u} OAI.Thomason.OmegaCategory.{u} where  obj := OAI.Thomason.DirectedComplex.nu  map := OAI.Thomason.DirectedComplex.Hom.nu  map_id K := by    change OAI.Thomason.DirectedComplex.Hom.nu (OAI.Thomason.DirectedComplex.Hom.id K) = OAI.Thomason.OmegaCategory.Functor.id K.nu    ext x    rfl  map_comp f g := by    change OAI.Thomason.DirectedComplex.Hom.nu (OAI.Thomason.DirectedComplex.Hom.comp f g) = OAI.Thomason.OmegaCategory.Functor.comp f.nu g.nu    ext x    rflend OAI.Thomason.DirectedComplexendsectionnamespace OAI.Thomason.NormalizedChainsvariable {E : Type u} [PartialOrder E]noncomputable abbrev Word (E : Type u) [PartialOrder E] :=  {l : List E // l.Pairwise (· < ·)}noncomputable abbrev Chains (E : Type u) [PartialOrder E] := OAI.Thomason.NormalizedChains.Word E →₀ ℤnoncomputable def bracket (l : List E) : OAI.Thomason.NormalizedChains.Chains E := by  classical  exact if h : l.Pairwise (· < ·) then Finsupp.single ⟨l, h⟩ 1 else 0noncomputable def prepend (a : E) : OAI.Thomason.NormalizedChains.Chains E →ₗ[ℤ] OAI.Thomason.NormalizedChains.Chains E :=  Finsupp.linearCombination ℤ (fun l : OAI.Thomason.NormalizedChains.Word E => OAI.Thomason.NormalizedChains.bracket (a :: l.val))noncomputable def wordBoundary : List E → OAI.Thomason.NormalizedChains.Chains E  | [] => 0  | a :: l => OAI.Thomason.NormalizedChains.bracket l - OAI.Thomason.NormalizedChains.prepend a (wordBoundary l)noncomputable def boundary : OAI.Thomason.NormalizedChains.Chains E →ₗ[ℤ] OAI.Thomason.NormalizedChains.Chains E :=  Finsupp.linearCombination ℤ (fun l : OAI.Thomason.NormalizedChains.Word E => OAI.Thomason.NormalizedChains.wordBoundary l.val)end OAI.Thomason.NormalizedChainsendsectionnamespace OAI.Thomason.NormalizedChainsvariable {E : Type u} [PartialOrder E]omit [PartialOrder E]variable {M : Type v} [AddCommGroup M]noncomputable def faces (H : List E → M) : List E → M  | [] => 0  | a :: l => H l - faces (fun m => H (a :: m)) lend OAI.Thomason.NormalizedChainsendsectionnamespace OAI.Thomason.NormalizedChainsvariable {E : Type u} [PartialOrder E]noncomputable def grade (k : ℕ) : Submodule ℤ (OAI.Thomason.NormalizedChains.Chains E) :=  Finsupp.supported ℤ ℤ {w : OAI.Thomason.NormalizedChains.Word E | w.val.length = k}noncomputable def emptyWord : OAI.Thomason.NormalizedChains.Word E := ⟨[], List.Pairwise.nil⟩noncomputable def emptyCoefficient : OAI.Thomason.NormalizedChains.Chains E →ₗ[ℤ] ℤ := Finsupp.lapply OAI.Thomason.NormalizedChains.emptyWordnoncomputable def Positive (c : OAI.Thomason.NormalizedChains.Chains E) : Prop := ∀ l, 0 ≤ c lnoncomputable def positiveGrade (p : ℕ) : AddSubmonoid (OAI.Thomason.NormalizedChains.grade (E := E) (p+1)) where  carrier := {c | Positive c.val}  zero_mem' _ := le_rfl  add_mem' ha hb w := add_nonneg (ha w) (hb w)noncomputable def complex (E : Type u) [PartialOrder E] : OAI.Thomason.DirectedComplex.{u} := by  classical  have proof_mem_grade_iff_20 {E : Type u} [instLocal1 : PartialOrder.{u} E]  (k : ℕ) (c : OAI.Thomason.NormalizedChains.Chains E) :      c ∈ OAI.Thomason.NormalizedChains.grade k ↔ ∀ w, c w ≠ 0 → w.val.length = k := by    simp only [OAI.Thomason.NormalizedChains.grade, Finsupp.mem_supported, Set.subset_def, Finsupp.mem_support_iff,      Finset.mem_coe, Set.mem_ofPred_eq]  have proof_linearCombination_mem_grade_21 {E : Type u} [instLocal1 : PartialOrder.{u} E]  {D : Type u} [PartialOrder D]      (H : OAI.Thomason.NormalizedChains.Word E → OAI.Thomason.NormalizedChains.Chains D) (k j : ℕ)      (hH : ∀ w, w.val.length = k → H w ∈ OAI.Thomason.NormalizedChains.grade j)      {c : OAI.Thomason.NormalizedChains.Chains E} (hc : c ∈ OAI.Thomason.NormalizedChains.grade k) :      Finsupp.linearCombination ℤ H c ∈ OAI.Thomason.NormalizedChains.grade j := by    rw [Finsupp.linearCombination_apply, Finsupp.sum]    apply Submodule.sum_mem    intro w hw    exact Submodule.smul_mem _ _ (hH w ((proof_mem_grade_iff_20 k c).mp hc w      (Finsupp.mem_support_iff.mp hw)))  have proof_bracket_of_pairwise_22 {E : Type u} [instLocal1 : PartialOrder.{u} E]  {l : List E} (h : l.Pairwise (· < ·)) :      OAI.Thomason.NormalizedChains.bracket l = Finsupp.single ⟨l, h⟩ 1 := by    classical    simp [OAI.Thomason.NormalizedChains.bracket, h]  have proof_bracket_of_not_pairwise_23 {E : Type u} [instLocal1 : PartialOrder.{u} E]  {l : List E} (h : ¬l.Pairwise (· < ·)) :      OAI.Thomason.NormalizedChains.bracket l = 0 := by    classical    simp [OAI.Thomason.NormalizedChains.bracket, h]  have proof_bracket_mem_grade_24 {E : Type u} [instLocal1 : PartialOrder.{u} E]  (l : List E) : OAI.Thomason.NormalizedChains.bracket l ∈ OAI.Thomason.NormalizedChains.grade l.length := by    classical    by_cases h : l.Pairwise (· < ·)    · rw [proof_bracket_of_pairwise_22 h]      exact Finsupp.single_mem_supported ℤ 1 rfl    · rw [proof_bracket_of_not_pairwise_23 h]      exact Submodule.zero_mem _  have proof_wordBoundary_nil_25 {E : Type u} [instLocal1 : PartialOrder.{u} E]  : OAI.Thomason.NormalizedChains.wordBoundary ([] : List E) = 0 := rfl  have proof_wordBoundary_cons_26 {E : Type u} [instLocal1 : PartialOrder.{u} E]  (a : E) (l : List E) :      OAI.Thomason.NormalizedChains.wordBoundary (a :: l) = OAI.Thomason.NormalizedChains.bracket l - OAI.Thomason.NormalizedChains.prepend a (OAI.Thomason.NormalizedChains.wordBoundary l) := rfl  have proof_prepend_bracket_27 {E : Type u} [instLocal1 : PartialOrder.{u} E]  (a : E) (l : List E) :      OAI.Thomason.NormalizedChains.prepend a (OAI.Thomason.NormalizedChains.bracket l) = OAI.Thomason.NormalizedChains.bracket (a :: l) := by    classical    by_cases h : l.Pairwise (· < ·)    · rw [proof_bracket_of_pairwise_22 h]      change Finsupp.linearCombination ℤ (fun l : OAI.Thomason.NormalizedChains.Word E => OAI.Thomason.NormalizedChains.bracket (a :: l.val))        (Finsupp.single (⟨l, h⟩ : OAI.Thomason.NormalizedChains.Word E) 1) = _      rw [Finsupp.linearCombination_single]      simp    · have h' : ¬(a :: l).Pairwise (· < ·) := fun hw => h hw.tail      simp [proof_bracket_of_not_pairwise_23 h, proof_bracket_of_not_pairwise_23 h']  have proof_prepend_mem_grade_28 {E : Type u} [instLocal1 : PartialOrder.{u} E]  (a : E) {k : ℕ} {c : OAI.Thomason.NormalizedChains.Chains E} (hc : c ∈ OAI.Thomason.NormalizedChains.grade k) :      OAI.Thomason.NormalizedChains.prepend a c ∈ OAI.Thomason.NormalizedChains.grade (k+1) := by    apply proof_linearCombination_mem_grade_21 _ k (k+1) _ hc    intro w hw    simpa only [List.length_cons, hw] using proof_bracket_mem_grade_24 (a :: w.val)  have proof_wordBoundary_mem_grade_29 {E : Type u} [instLocal1 : PartialOrder.{u} E]  (l : List E) : OAI.Thomason.NormalizedChains.wordBoundary l ∈ OAI.Thomason.NormalizedChains.grade (l.length-1) := by    induction l with    | nil => exact Submodule.zero_mem _    | cons a l ih =>      cases l with      | nil => simpa [proof_wordBoundary_nil_25, proof_wordBoundary_cons_26, proof_prepend_bracket_27, OAI.Thomason.NormalizedChains.wordBoundary] using proof_bracket_mem_grade_24 ([] : List E)      | cons b l =>        rw [proof_wordBoundary_cons_26]        apply Submodule.sub_mem        · simpa [proof_wordBoundary_nil_25, proof_wordBoundary_cons_26, proof_prepend_bracket_27] using proof_bracket_mem_grade_24 (b :: l)        · simpa [proof_wordBoundary_nil_25, proof_wordBoundary_cons_26, proof_prepend_bracket_27] using proof_prepend_mem_grade_28 a ih  have proof_boundary_mem_grade_18 {E : Type u} [instLocal1 : PartialOrder.{u} E]  {k : ℕ} {c : OAI.Thomason.NormalizedChains.Chains E} (hc : c ∈ OAI.Thomason.NormalizedChains.grade (k+1)) :      OAI.Thomason.NormalizedChains.boundary c ∈ OAI.Thomason.NormalizedChains.grade k := by    apply proof_linearCombination_mem_grade_21 _ (k+1) k _ hc    intro w hw    simpa only [hw, Nat.add_sub_cancel] using proof_wordBoundary_mem_grade_29 w.val  have proof_prepend_prepend_self_30 {E : Type u} [instLocal1 : PartialOrder.{u} E]  (a : E) (c : OAI.Thomason.NormalizedChains.Chains E) : OAI.Thomason.NormalizedChains.prepend a (OAI.Thomason.NormalizedChains.prepend a c) = 0 := by    classical    induction c using Finsupp.induction with    | zero => simp []    | @single_add l z c _ _ ih =>      simp only [map_add, ih, add_zero]      have hz : Finsupp.single l z = z • OAI.Thomason.NormalizedChains.bracket l.val := by        rw [proof_bracket_of_pairwise_22 l.property]        simp only [Finsupp.smul_single, smul_eq_mul, mul_one]      rw [hz]      simp only [map_smul, proof_prepend_bracket_27]      have h : ¬(a :: a :: l.val).Pairwise (· < ·) := by simp []      simp [proof_bracket_of_not_pairwise_23 h]  have proof_wordBoundary_repeated_31 {E : Type u} [instLocal1 : PartialOrder.{u} E]  (a : E) (l : List E) :      OAI.Thomason.NormalizedChains.wordBoundary (a :: a :: l) = 0 := by    simp [proof_prepend_bracket_27, OAI.Thomason.NormalizedChains.wordBoundary, map_sub, proof_prepend_prepend_self_30]  have proof_wordBoundary_eq_zero_of_not_pairwise_32 {E : Type u} [instLocal1 : PartialOrder.{u} E]  {l : List E}      (h : l.Pairwise (· ≤ ·)) (hn : ¬l.Pairwise (· < ·)) : OAI.Thomason.NormalizedChains.wordBoundary l = 0 := by    induction l with    | nil => exact (hn (by simp)).elim    | cons a l ih =>      by_cases hl : l.Pairwise (· < ·)      · cases l with        | nil => exact (hn (by simp)).elim        | cons b l =>          have hab : a ≤ b := (List.pairwise_cons.mp h).1 b (by simp)          have hab' : ¬a < b := by            intro hab'            exact hn (List.Pairwise.cons_cons_of_trans hab' hl)          have heq : a = b := (lt_or_eq_of_le hab).resolve_left hab'          subst b          exact proof_wordBoundary_repeated_31 a l      · simp [OAI.Thomason.NormalizedChains.wordBoundary, proof_bracket_of_not_pairwise_23 hl, ih h.tail hl]  have proof_boundary_bracket_33 {E : Type u} [instLocal1 : PartialOrder.{u} E]  {l : List E} (h : l.Pairwise (· ≤ ·)) :      OAI.Thomason.NormalizedChains.boundary (OAI.Thomason.NormalizedChains.bracket l) = OAI.Thomason.NormalizedChains.wordBoundary l := by    classical    by_cases hs : l.Pairwise (· < ·)    · rw [proof_bracket_of_pairwise_22 hs]      change Finsupp.linearCombination ℤ (fun l : OAI.Thomason.NormalizedChains.Word E => OAI.Thomason.NormalizedChains.wordBoundary l.val)        (Finsupp.single (⟨l, hs⟩ : OAI.Thomason.NormalizedChains.Word E) 1) = _      rw [Finsupp.linearCombination_single]      simp []    · simp [proof_bracket_of_not_pairwise_23 hs, proof_wordBoundary_eq_zero_of_not_pairwise_32 h hs]  have proof_faces_nil_34 {E : Type u} {M : Type u} [instLocal2 : AddCommGroup.{u} M]  (H : List E → M) : OAI.Thomason.NormalizedChains.faces H [] = 0 := rfl  have proof_faces_cons_35 {E : Type u} {M : Type u} [instLocal2 : AddCommGroup.{u} M]  (H : List E → M) (a : E) (l : List E) :      OAI.Thomason.NormalizedChains.faces H (a :: l) = H l - OAI.Thomason.NormalizedChains.faces (fun m => H (a :: m)) l := rfl  have proof_faces_hom_36 {E : Type u} {M : Type u} [instLocal2 : AddCommGroup.{u} M]  {M' : Type u} [AddCommGroup M'] (q : M →+ M')      (H : List E → M) (l : List E) :      q (OAI.Thomason.NormalizedChains.faces H l) = OAI.Thomason.NormalizedChains.faces (fun m => q (H m)) l := by    induction l generalizing H with    | nil => simp only [OAI.Thomason.NormalizedChains.faces, map_zero]    | cons a l ih => simp only [OAI.Thomason.NormalizedChains.faces, map_sub, ih]  have proof_faces_bracket_37 {E : Type u} [instLocal1 : PartialOrder.{u} E]  (l : List E) : OAI.Thomason.NormalizedChains.faces OAI.Thomason.NormalizedChains.bracket l = OAI.Thomason.NormalizedChains.wordBoundary l := by    induction l with    | nil => rfl    | cons a l ih =>      rw [proof_faces_cons_35, proof_wordBoundary_cons_26]      have h := proof_faces_hom_36 (OAI.Thomason.NormalizedChains.prepend a).toAddMonoidHom OAI.Thomason.NormalizedChains.bracket l      simp only [LinearMap.toAddMonoidHom_coe, proof_prepend_bracket_27] at h      rw [← h, ih]  have proof_faces_congr_38 {E : Type u} {M : Type u} [instLocal2 : AddCommGroup.{u} M]  {H K : List E → M} {l : List E}      (h : ∀ m, m.Sublist l → H m = K m) : OAI.Thomason.NormalizedChains.faces H l = OAI.Thomason.NormalizedChains.faces K l := by    induction l generalizing H K with    | nil => rfl    | cons a l ih =>      rw [proof_faces_cons_35, proof_faces_cons_35, h l (List.sublist_cons_self a l)]      congr 1      exact ih (fun m hm => h (a :: m) (List.Sublist.cons_cons a hm))  have proof_faces_sub_39 {E : Type u} {M : Type u} [instLocal2 : AddCommGroup.{u} M]  (H K : List E → M) (l : List E) :      OAI.Thomason.NormalizedChains.faces (fun m => H m - K m) l = OAI.Thomason.NormalizedChains.faces H l - OAI.Thomason.NormalizedChains.faces K l := by    induction l generalizing H K with    | nil => simp [proof_faces_nil_34]    | cons a l ih => simp only [proof_faces_cons_35, ih]; abel  have proof_faces_faces_40 {E : Type u} {M : Type u} [instLocal2 : AddCommGroup.{u} M]  (H : List E → M) (l : List E) :      OAI.Thomason.NormalizedChains.faces (OAI.Thomason.NormalizedChains.faces H) l = 0 := by    induction l generalizing H with    | nil => rfl    | cons a l ih =>      simp only [proof_faces_cons_35]      rw [proof_faces_sub_39, ih]      simp []  have proof_boundary_wordBoundary_41 {E : Type u} [instLocal1 : PartialOrder.{u} E]  {l : List E} (h : l.Pairwise (· ≤ ·)) :      OAI.Thomason.NormalizedChains.boundary (OAI.Thomason.NormalizedChains.wordBoundary l) = 0 := by    rw [← proof_faces_bracket_37]    change OAI.Thomason.NormalizedChains.boundary.toAddMonoidHom (OAI.Thomason.NormalizedChains.faces OAI.Thomason.NormalizedChains.bracket l) = 0    rw [proof_faces_hom_36]    have hc : OAI.Thomason.NormalizedChains.faces (fun m => OAI.Thomason.NormalizedChains.boundary (OAI.Thomason.NormalizedChains.bracket m)) l = OAI.Thomason.NormalizedChains.faces OAI.Thomason.NormalizedChains.wordBoundary l := by      apply proof_faces_congr_38      intro m hm      exact proof_boundary_bracket_33 (h.sublist hm)    change OAI.Thomason.NormalizedChains.faces (fun m => OAI.Thomason.NormalizedChains.boundary (OAI.Thomason.NormalizedChains.bracket m)) l = 0    rw [hc]    change OAI.Thomason.NormalizedChains.faces (fun m => OAI.Thomason.NormalizedChains.wordBoundary m) l = 0    simp_rw [← proof_faces_bracket_37]    exact proof_faces_faces_40 OAI.Thomason.NormalizedChains.bracket l  have proof_boundary_boundary_19 {E : Type u} [instLocal1 : PartialOrder.{u} E]  (c : OAI.Thomason.NormalizedChains.Chains E) : OAI.Thomason.NormalizedChains.boundary (OAI.Thomason.NormalizedChains.boundary c) = 0 := by    classical    induction c using Finsupp.induction with    | zero => simp []    | @single_add l z c _ _ ih =>      simp only [map_add, ih, add_zero]      have hz : Finsupp.single l z = z • OAI.Thomason.NormalizedChains.bracket l.val := by        rw [proof_bracket_of_pairwise_22 l.property]        simp only [Finsupp.smul_single, smul_eq_mul, mul_one]      rw [hz]      simp only [map_smul]      rw [proof_boundary_bracket_33 (l.property.imp fun h => le_of_lt h),        proof_boundary_wordBoundary_41 (l.property.imp fun h => le_of_lt h), smul_zero]  exact {    Chain p := OAI.Thomason.NormalizedChains.grade (E := E) (p+1)    group _ := inferInstance    d p :=      { toFun := fun c => ⟨OAI.Thomason.NormalizedChains.boundary c.val, proof_boundary_mem_grade_18 c.property⟩        map_zero' := Subtype.ext (map_zero _)        map_add' := fun x y => Subtype.ext (map_add _ x.val y.val) }    d_d p x := Subtype.ext (proof_boundary_boundary_19 x.val)    augmentation :=      { toFun := fun c => OAI.Thomason.NormalizedChains.emptyCoefficient (OAI.Thomason.NormalizedChains.boundary c.val)        map_zero' := by simp []        map_add' := by intros; simp [] }    augmentation_d x := by      change OAI.Thomason.NormalizedChains.emptyCoefficient (OAI.Thomason.NormalizedChains.boundary (OAI.Thomason.NormalizedChains.boundary x.val)) = 0      rw [proof_boundary_boundary_19, map_zero]    positive := OAI.Thomason.NormalizedChains.positiveGrade  }end OAI.Thomason.NormalizedChainsendsectionnamespace OAI.Thomason.NormalizedChainsvariable {E : Type u} [PartialOrder E]variable {D : Type v} [PartialOrder D] {B : Type w} [PartialOrder B]noncomputable def map (f : E →o D) : OAI.Thomason.NormalizedChains.Chains E →ₗ[ℤ] OAI.Thomason.NormalizedChains.Chains D :=  Finsupp.linearCombination ℤ (fun l : OAI.Thomason.NormalizedChains.Word E => OAI.Thomason.NormalizedChains.bracket (l.val.map f))end OAI.Thomason.NormalizedChainsendsectionnamespace OAI.Thomason.NormalizedChainsvariable {E : Type u} [PartialOrder E]noncomputable def complexMap {D : Type v} [PartialOrder D] (f : E →o D) :    OAI.Thomason.DirectedComplex.Hom (OAI.Thomason.NormalizedChains.complex E) (OAI.Thomason.NormalizedChains.complex D) := by  classical  have proof_mem_grade_iff_20 {E : Type u} [instLocal1 : PartialOrder.{u} E]  (k : ℕ) (c : OAI.Thomason.NormalizedChains.Chains E) :      c ∈ OAI.Thomason.NormalizedChains.grade k ↔ ∀ w, c w ≠ 0 → w.val.length = k := by    simp only [OAI.Thomason.NormalizedChains.grade, Finsupp.mem_supported, Set.subset_def, Finsupp.mem_support_iff,      Finset.mem_coe, Set.mem_ofPred_eq]  have proof_linearCombination_mem_grade_46 {E : Type u} [instLocal1 : PartialOrder.{u} E]  {D : Type v} [PartialOrder D]      (H : OAI.Thomason.NormalizedChains.Word E → OAI.Thomason.NormalizedChains.Chains D) (k j : ℕ)      (hH : ∀ w, w.val.length = k → H w ∈ OAI.Thomason.NormalizedChains.grade j)      {c : OAI.Thomason.NormalizedChains.Chains E} (hc : c ∈ OAI.Thomason.NormalizedChains.grade k) :      Finsupp.linearCombination ℤ H c ∈ OAI.Thomason.NormalizedChains.grade j := by    rw [Finsupp.linearCombination_apply, Finsupp.sum]    apply Submodule.sum_mem    intro w hw    exact Submodule.smul_mem _ _ (hH w ((proof_mem_grade_iff_20 k c).mp hc w      (Finsupp.mem_support_iff.mp hw)))  have proof_bracket_of_pairwise_47 {E : Type v} [instLocal1 : PartialOrder.{v} E]  {l : List E} (h : l.Pairwise (· < ·)) :      OAI.Thomason.NormalizedChains.bracket l = Finsupp.single ⟨l, h⟩ 1 := by    classical    simp [OAI.Thomason.NormalizedChains.bracket, h]  have proof_bracket_of_not_pairwise_48 {E : Type v} [instLocal1 : PartialOrder.{v} E]  {l : List E} (h : ¬l.Pairwise (· < ·)) :      OAI.Thomason.NormalizedChains.bracket l = 0 := by    classical    simp [OAI.Thomason.NormalizedChains.bracket, h]  have proof_bracket_mem_grade_49 {E : Type v} [instLocal1 : PartialOrder.{v} E]  (l : List E) : OAI.Thomason.NormalizedChains.bracket l ∈ OAI.Thomason.NormalizedChains.grade l.length := by    classical    by_cases h : l.Pairwise (· < ·)    · rw [proof_bracket_of_pairwise_47 h]      exact Finsupp.single_mem_supported ℤ 1 rfl    · rw [proof_bracket_of_not_pairwise_48 h]      exact Submodule.zero_mem _  have proof_map_mem_grade_42 {E : Type u} [instLocal1 : PartialOrder.{u} E]  {D : Type v} [PartialOrder D] (f : E →o D) {k : ℕ}      {c : OAI.Thomason.NormalizedChains.Chains E} (hc : c ∈ OAI.Thomason.NormalizedChains.grade k) : OAI.Thomason.NormalizedChains.map f c ∈ OAI.Thomason.NormalizedChains.grade k := by    apply proof_linearCombination_mem_grade_46 _ k k _ hc    intro w hw    simpa only [List.length_map, hw] using proof_bracket_mem_grade_49 (w.val.map f)  have proof_bracket_of_pairwise_22 {E : Type u} [instLocal1 : PartialOrder.{u} E]  {l : List E} (h : l.Pairwise (· < ·)) :      OAI.Thomason.NormalizedChains.bracket l = Finsupp.single ⟨l, h⟩ 1 := by    classical    simp [OAI.Thomason.NormalizedChains.bracket, h]  have proof_bracket_of_not_pairwise_23 {E : Type u} [instLocal1 : PartialOrder.{u} E]  {l : List E} (h : ¬l.Pairwise (· < ·)) :      OAI.Thomason.NormalizedChains.bracket l = 0 := by    classical    simp [OAI.Thomason.NormalizedChains.bracket, h]  have proof_prepend_bracket_27 {E : Type u} [instLocal1 : PartialOrder.{u} E]  (a : E) (l : List E) :      OAI.Thomason.NormalizedChains.prepend a (OAI.Thomason.NormalizedChains.bracket l) = OAI.Thomason.NormalizedChains.bracket (a :: l) := by    classical    by_cases h : l.Pairwise (· < ·)    · rw [proof_bracket_of_pairwise_22 h]      change Finsupp.linearCombination ℤ (fun l : OAI.Thomason.NormalizedChains.Word E => OAI.Thomason.NormalizedChains.bracket (a :: l.val))        (Finsupp.single (⟨l, h⟩ : OAI.Thomason.NormalizedChains.Word E) 1) = _      rw [Finsupp.linearCombination_single]      simp    · have h' : ¬(a :: l).Pairwise (· < ·) := fun hw => h hw.tail      simp [proof_bracket_of_not_pairwise_23 h, proof_bracket_of_not_pairwise_23 h']  have proof_prepend_prepend_self_30 {E : Type u} [instLocal1 : PartialOrder.{u} E]  (a : E) (c : OAI.Thomason.NormalizedChains.Chains E) : OAI.Thomason.NormalizedChains.prepend a (OAI.Thomason.NormalizedChains.prepend a c) = 0 := by    classical    induction c using Finsupp.induction with    | zero => simp []    | @single_add l z c _ _ ih =>      simp only [map_add, ih, add_zero]      have hz : Finsupp.single l z = z • OAI.Thomason.NormalizedChains.bracket l.val := by        rw [proof_bracket_of_pairwise_22 l.property]        simp only [Finsupp.smul_single, smul_eq_mul, mul_one]      rw [hz]      simp only [map_smul, proof_prepend_bracket_27]      have h : ¬(a :: a :: l.val).Pairwise (· < ·) := by simp []      simp [proof_bracket_of_not_pairwise_23 h]  have proof_wordBoundary_nil_25 {E : Type u} [instLocal1 : PartialOrder.{u} E]  : OAI.Thomason.NormalizedChains.wordBoundary ([] : List E) = 0 := rfl  have proof_wordBoundary_cons_26 {E : Type u} [instLocal1 : PartialOrder.{u} E]  (a : E) (l : List E) :      OAI.Thomason.NormalizedChains.wordBoundary (a :: l) = OAI.Thomason.NormalizedChains.bracket l - OAI.Thomason.NormalizedChains.prepend a (OAI.Thomason.NormalizedChains.wordBoundary l) := rfl  have proof_wordBoundary_repeated_31 {E : Type u} [instLocal1 : PartialOrder.{u} E]  (a : E) (l : List E) :      OAI.Thomason.NormalizedChains.wordBoundary (a :: a :: l) = 0 := by    simp [proof_prepend_bracket_27, OAI.Thomason.NormalizedChains.wordBoundary, map_sub, proof_prepend_prepend_self_30]  have proof_wordBoundary_eq_zero_of_not_pairwise_32 {E : Type u} [instLocal1 : PartialOrder.{u} E]  {l : List E}      (h : l.Pairwise (· ≤ ·)) (hn : ¬l.Pairwise (· < ·)) : OAI.Thomason.NormalizedChains.wordBoundary l = 0 := by    induction l with    | nil => exact (hn (by simp)).elim    | cons a l ih =>      by_cases hl : l.Pairwise (· < ·)      · cases l with        | nil => exact (hn (by simp)).elim        | cons b l =>          have hab : a ≤ b := (List.pairwise_cons.mp h).1 b (by simp)          have hab' : ¬a < b := by            intro hab'            exact hn (List.Pairwise.cons_cons_of_trans hab' hl)          have heq : a = b := (lt_or_eq_of_le hab).resolve_left hab'          subst b          exact proof_wordBoundary_repeated_31 a l      · simp [OAI.Thomason.NormalizedChains.wordBoundary, proof_bracket_of_not_pairwise_23 hl, ih h.tail hl]  have proof_boundary_bracket_33 {E : Type u} [instLocal1 : PartialOrder.{u} E]  {l : List E} (h : l.Pairwise (· ≤ ·)) :      OAI.Thomason.NormalizedChains.boundary (OAI.Thomason.NormalizedChains.bracket l) = OAI.Thomason.NormalizedChains.wordBoundary l := by    classical    by_cases hs : l.Pairwise (· < ·)    · rw [proof_bracket_of_pairwise_22 hs]      change Finsupp.linearCombination ℤ (fun l : OAI.Thomason.NormalizedChains.Word E => OAI.Thomason.NormalizedChains.wordBoundary l.val)        (Finsupp.single (⟨l, hs⟩ : OAI.Thomason.NormalizedChains.Word E) 1) = _      rw [Finsupp.linearCombination_single]      simp []    · simp [proof_bracket_of_not_pairwise_23 hs, proof_wordBoundary_eq_zero_of_not_pairwise_32 h hs]  have proof_faces_nil_34 {E : Type u} {M : Type u} [instLocal2 : AddCommGroup.{u} M]  (H : List E → M) : OAI.Thomason.NormalizedChains.faces H [] = 0 := rfl  have proof_faces_cons_35 {E : Type u} {M : Type u} [instLocal2 : AddCommGroup.{u} M]  (H : List E → M) (a : E) (l : List E) :      OAI.Thomason.NormalizedChains.faces H (a :: l) = H l - OAI.Thomason.NormalizedChains.faces (fun m => H (a :: m)) l := rfl  have proof_faces_hom_36 {E : Type u} {M : Type u} [instLocal2 : AddCommGroup.{u} M]  {M' : Type u} [AddCommGroup M'] (q : M →+ M')      (H : List E → M) (l : List E) :      q (OAI.Thomason.NormalizedChains.faces H l) = OAI.Thomason.NormalizedChains.faces (fun m => q (H m)) l := by    induction l generalizing H with    | nil => simp only [OAI.Thomason.NormalizedChains.faces, map_zero]    | cons a l ih => simp only [OAI.Thomason.NormalizedChains.faces, map_sub, ih]  have proof_faces_bracket_37 {E : Type u} [instLocal1 : PartialOrder.{u} E]  (l : List E) : OAI.Thomason.NormalizedChains.faces OAI.Thomason.NormalizedChains.bracket l = OAI.Thomason.NormalizedChains.wordBoundary l := by    induction l with    | nil => rfl    | cons a l ih =>      rw [proof_faces_cons_35, proof_wordBoundary_cons_26]      have h := proof_faces_hom_36 (OAI.Thomason.NormalizedChains.prepend a).toAddMonoidHom OAI.Thomason.NormalizedChains.bracket l      simp only [LinearMap.toAddMonoidHom_coe, proof_prepend_bracket_27] at h      rw [← h, ih]  have proof_faces_nil_50 {E : Type v} {M : Type v} [instLocal2 : AddCommGroup.{v} M]  (H : List E → M) : OAI.Thomason.NormalizedChains.faces H [] = 0 := rfl  have proof_faces_cons_51 {E : Type v} {M : Type v} [instLocal2 : AddCommGroup.{v} M]  (H : List E → M) (a : E) (l : List E) :      OAI.Thomason.NormalizedChains.faces H (a :: l) = H l - OAI.Thomason.NormalizedChains.faces (fun m => H (a :: m)) l := rfl  have proof_wordBoundary_nil_52 {E : Type v} [instLocal1 : PartialOrder.{v} E]  : OAI.Thomason.NormalizedChains.wordBoundary ([] : List E) = 0 := rfl  have proof_wordBoundary_cons_53 {E : Type v} [instLocal1 : PartialOrder.{v} E]  (a : E) (l : List E) :      OAI.Thomason.NormalizedChains.wordBoundary (a :: l) = OAI.Thomason.NormalizedChains.bracket l - OAI.Thomason.NormalizedChains.prepend a (OAI.Thomason.NormalizedChains.wordBoundary l) := rfl  have proof_faces_hom_54 {E : Type v} {M : Type v} [instLocal2 : AddCommGroup.{v} M]  {M' : Type v} [AddCommGroup M'] (q : M →+ M')      (H : List E → M) (l : List E) :      q (OAI.Thomason.NormalizedChains.faces H l) = OAI.Thomason.NormalizedChains.faces (fun m => q (H m)) l := by    induction l generalizing H with    | nil => simp [proof_faces_nil_50]    | cons a l ih => simp only [proof_faces_cons_51, map_sub, ih]  have proof_prepend_bracket_55 {E : Type v} [instLocal1 : PartialOrder.{v} E]  (a : E) (l : List E) :      OAI.Thomason.NormalizedChains.prepend a (OAI.Thomason.NormalizedChains.bracket l) = OAI.Thomason.NormalizedChains.bracket (a :: l) := by    classical    by_cases h : l.Pairwise (· < ·)    · rw [proof_bracket_of_pairwise_47 h]      change Finsupp.linearCombination ℤ (fun l : OAI.Thomason.NormalizedChains.Word E => OAI.Thomason.NormalizedChains.bracket (a :: l.val))        (Finsupp.single (⟨l, h⟩ : OAI.Thomason.NormalizedChains.Word E) 1) = _      rw [Finsupp.linearCombination_single]      simp    · have h' : ¬(a :: l).Pairwise (· < ·) := fun hw => h hw.tail      simp [proof_bracket_of_not_pairwise_48 h, proof_bracket_of_not_pairwise_48 h']  have proof_faces_bracket_56 {E : Type v} [instLocal1 : PartialOrder.{v} E]  (l : List E) : OAI.Thomason.NormalizedChains.faces OAI.Thomason.NormalizedChains.bracket l = OAI.Thomason.NormalizedChains.wordBoundary l := by    induction l with    | nil => rfl    | cons a l ih =>      rw [proof_faces_cons_51, proof_wordBoundary_cons_53]      have h := proof_faces_hom_54 (OAI.Thomason.NormalizedChains.prepend a).toAddMonoidHom OAI.Thomason.NormalizedChains.bracket l      simp only [LinearMap.toAddMonoidHom_coe, proof_prepend_bracket_55] at h      rw [← h, ih]  have proof_faces_hom_57 {E : Type u} {M : Type u} [instLocal2 : AddCommGroup.{u} M]  {M' : Type v} [AddCommGroup M'] (q : M →+ M')      (H : List E → M) (l : List E) :      q (OAI.Thomason.NormalizedChains.faces H l) = OAI.Thomason.NormalizedChains.faces (fun m => q (H m)) l := by    induction l generalizing H with    | nil => simp only [OAI.Thomason.NormalizedChains.faces, map_zero]    | cons a l ih => simp only [OAI.Thomason.NormalizedChains.faces, map_sub, ih]  have proof_faces_map_58 {E : Type v} {M : Type v} [instLocal2 : AddCommGroup.{v} M]  {D : Type u} (f : D → E) (H : List E → M) (l : List D) :      OAI.Thomason.NormalizedChains.faces H (l.map f) = OAI.Thomason.NormalizedChains.faces (fun m => H (m.map f)) l := by    induction l generalizing H with    | nil => rfl    | cons a l ih => simp only [List.map_cons, OAI.Thomason.NormalizedChains.faces, ih]  have proof_faces_nil_59 {E : Type u} {M : Type v} [instLocal2 : AddCommGroup.{v} M]  (H : List E → M) : OAI.Thomason.NormalizedChains.faces H [] = 0 := rfl  have proof_faces_cons_60 {E : Type u} {M : Type v} [instLocal2 : AddCommGroup.{v} M]  (H : List E → M) (a : E) (l : List E) :      OAI.Thomason.NormalizedChains.faces H (a :: l) = H l - OAI.Thomason.NormalizedChains.faces (fun m => H (a :: m)) l := rfl  have proof_faces_congr_61 {E : Type u} {M : Type v} [instLocal2 : AddCommGroup.{v} M]  {H K : List E → M} {l : List E}      (h : ∀ m, m.Sublist l → H m = K m) : OAI.Thomason.NormalizedChains.faces H l = OAI.Thomason.NormalizedChains.faces K l := by    induction l generalizing H K with    | nil => rfl    | cons a l ih =>      rw [proof_faces_cons_60, proof_faces_cons_60, h l (List.sublist_cons_self a l)]      congr 1      exact ih (fun m hm => h (a :: m) (List.Sublist.cons_cons a hm))  have proof_pairwise_of_map_62 {E : Type u} [instLocal1 : PartialOrder.{u} E] {D : Type v} [instLocal3 : PartialOrder.{v} D]  {l : List E} (h : l.Pairwise (· ≤ ·)) (f : E → D)      (hf : (l.map f).Pairwise (· < ·)) : l.Pairwise (· < ·) := by    apply (h.and (List.pairwise_map.mp hf)).imp    intro a b hab    exact lt_of_le_of_ne hab.1 (fun he => (ne_of_lt hab.2) (congrArg f he))  have proof_map_bracket_63 {E : Type u} [instLocal1 : PartialOrder.{u} E] {D : Type v} [instLocal3 : PartialOrder.{v} D]  (f : E →o D) {l : List E} (h : l.Pairwise (· ≤ ·)) :      OAI.Thomason.NormalizedChains.map f (OAI.Thomason.NormalizedChains.bracket l) = OAI.Thomason.NormalizedChains.bracket (l.map f) := by    classical    by_cases hs : l.Pairwise (· < ·)    · rw [proof_bracket_of_pairwise_22 hs]      change Finsupp.linearCombination ℤ (fun l : OAI.Thomason.NormalizedChains.Word E => OAI.Thomason.NormalizedChains.bracket (l.val.map f))        (Finsupp.single (⟨l, hs⟩ : OAI.Thomason.NormalizedChains.Word E) 1) = _      rw [Finsupp.linearCombination_single]      simp    · have hf : ¬(l.map f).Pairwise (· < ·) := fun hm => hs (proof_pairwise_of_map_62 h f hm)      simp [proof_bracket_of_not_pairwise_23 hs, proof_bracket_of_not_pairwise_48 hf]  have proof_map_wordBoundary_64 {E : Type u} [instLocal1 : PartialOrder.{u} E] {D : Type v} [instLocal3 : PartialOrder.{v} D]  (f : E →o D) {l : List E} (h : l.Pairwise (· ≤ ·)) :      OAI.Thomason.NormalizedChains.map f (OAI.Thomason.NormalizedChains.wordBoundary l) = OAI.Thomason.NormalizedChains.wordBoundary (l.map f) := by    rw [← proof_faces_bracket_37, ← proof_faces_bracket_56]    change (OAI.Thomason.NormalizedChains.map f).toAddMonoidHom (OAI.Thomason.NormalizedChains.faces OAI.Thomason.NormalizedChains.bracket l) = _    rw [proof_faces_hom_57, proof_faces_map_58]    apply proof_faces_congr_61    intro m hm    exact proof_map_bracket_63 f (h.sublist hm)  have proof_prepend_prepend_self_65 {E : Type v} [instLocal1 : PartialOrder.{v} E]  (a : E) (c : OAI.Thomason.NormalizedChains.Chains E) : OAI.Thomason.NormalizedChains.prepend a (OAI.Thomason.NormalizedChains.prepend a c) = 0 := by    classical    induction c using Finsupp.induction with    | zero => simp []    | @single_add l z c _ _ ih =>      simp only [map_add, ih, add_zero]      have hz : Finsupp.single l z = z • OAI.Thomason.NormalizedChains.bracket l.val := by        rw [proof_bracket_of_pairwise_47 l.property]        simp only [Finsupp.smul_single, smul_eq_mul, mul_one]      rw [hz]      simp only [map_smul, proof_prepend_bracket_55]      have h : ¬(a :: a :: l.val).Pairwise (· < ·) := by simp []      simp [proof_bracket_of_not_pairwise_48 h]  have proof_wordBoundary_repeated_66 {E : Type v} [instLocal1 : PartialOrder.{v} E]  (a : E) (l : List E) :      OAI.Thomason.NormalizedChains.wordBoundary (a :: a :: l) = 0 := by    simp [proof_prepend_bracket_55, OAI.Thomason.NormalizedChains.wordBoundary, map_sub, proof_prepend_prepend_self_65]  have proof_wordBoundary_eq_zero_of_not_pairwise_67 {E : Type v} [instLocal1 : PartialOrder.{v} E]  {l : List E}      (h : l.Pairwise (· ≤ ·)) (hn : ¬l.Pairwise (· < ·)) : OAI.Thomason.NormalizedChains.wordBoundary l = 0 := by    induction l with    | nil => exact (hn (by simp)).elim    | cons a l ih =>      by_cases hl : l.Pairwise (· < ·)      · cases l with        | nil => exact (hn (by simp)).elim        | cons b l =>          have hab : a ≤ b := (List.pairwise_cons.mp h).1 b (by simp)          have hab' : ¬a < b := by            intro hab'            exact hn (List.Pairwise.cons_cons_of_trans hab' hl)          have heq : a = b := (lt_or_eq_of_le hab).resolve_left hab'          subst b          exact proof_wordBoundary_repeated_66 a l      · simp [OAI.Thomason.NormalizedChains.wordBoundary, proof_bracket_of_not_pairwise_48 hl, ih h.tail hl]  have proof_boundary_bracket_68 {E : Type v} [instLocal1 : PartialOrder.{v} E]  {l : List E} (h : l.Pairwise (· ≤ ·)) :      OAI.Thomason.NormalizedChains.boundary (OAI.Thomason.NormalizedChains.bracket l) = OAI.Thomason.NormalizedChains.wordBoundary l := by    classical    by_cases hs : l.Pairwise (· < ·)    · rw [proof_bracket_of_pairwise_47 hs]      change Finsupp.linearCombination ℤ (fun l : OAI.Thomason.NormalizedChains.Word E => OAI.Thomason.NormalizedChains.wordBoundary l.val)        (Finsupp.single (⟨l, hs⟩ : OAI.Thomason.NormalizedChains.Word E) 1) = _      rw [Finsupp.linearCombination_single]      simp []    · simp [proof_bracket_of_not_pairwise_48 hs, proof_wordBoundary_eq_zero_of_not_pairwise_67 h hs]  have proof_map_boundary_43 {E : Type u} [instLocal1 : PartialOrder.{u} E] {D : Type v} [instLocal3 : PartialOrder.{v} D]  (f : E →o D) (c : OAI.Thomason.NormalizedChains.Chains E) :      OAI.Thomason.NormalizedChains.map f (OAI.Thomason.NormalizedChains.boundary c) = OAI.Thomason.NormalizedChains.boundary (OAI.Thomason.NormalizedChains.map f c) := by    classical    induction c using Finsupp.induction with    | zero => simp []    | @single_add l z c _ _ ih =>      simp only [map_add, ih]      congr 1      have hz : Finsupp.single l z = z • OAI.Thomason.NormalizedChains.bracket l.val := by        rw [proof_bracket_of_pairwise_22 l.property]        simp only [Finsupp.smul_single, smul_eq_mul, mul_one]      have hl := l.property.imp fun h => le_of_lt h      rw [hz]      simp only [map_smul]      rw [proof_boundary_bracket_33 hl, proof_map_wordBoundary_64 f hl, proof_map_bracket_63 f hl,        proof_boundary_bracket_68 (List.pairwise_map.mpr (hl.imp fun hh => f.monotone hh))]  have proof_emptyCoefficient_bracket_69 {E : Type v} [instLocal1 : PartialOrder.{v} E]  (l : List E) :      OAI.Thomason.NormalizedChains.emptyCoefficient (OAI.Thomason.NormalizedChains.bracket l) = if l = [] then 1 else 0 := by    classical    by_cases hl : l = []    · subst l      simp [OAI.Thomason.NormalizedChains.emptyCoefficient, proof_bracket_of_pairwise_47 List.Pairwise.nil, OAI.Thomason.NormalizedChains.emptyWord]    · by_cases hs : l.Pairwise (· < ·)      · have hw : (⟨l, hs⟩ : OAI.Thomason.NormalizedChains.Word E) ≠ OAI.Thomason.NormalizedChains.emptyWord := by          intro he          exact hl (congrArg Subtype.val he)        simp [OAI.Thomason.NormalizedChains.emptyCoefficient, proof_bracket_of_pairwise_47 hs, hw, hl]      · simp [proof_bracket_of_not_pairwise_48 hs, hl]  have proof_emptyCoefficient_bracket_70 {E : Type u} [instLocal1 : PartialOrder.{u} E]  (l : List E) :      OAI.Thomason.NormalizedChains.emptyCoefficient (OAI.Thomason.NormalizedChains.bracket l) = if l = [] then 1 else 0 := by    classical    by_cases hl : l = []    · subst l      simp [OAI.Thomason.NormalizedChains.emptyCoefficient, proof_bracket_of_pairwise_22 List.Pairwise.nil, OAI.Thomason.NormalizedChains.emptyWord]    · by_cases hs : l.Pairwise (· < ·)      · have hw : (⟨l, hs⟩ : OAI.Thomason.NormalizedChains.Word E) ≠ OAI.Thomason.NormalizedChains.emptyWord := by          intro he          exact hl (congrArg Subtype.val he)        simp [OAI.Thomason.NormalizedChains.emptyCoefficient, proof_bracket_of_pairwise_22 hs, hw, hl]      · simp [proof_bracket_of_not_pairwise_23 hs, hl]  have proof_emptyCoefficient_map_44 {E : Type u} [instLocal1 : PartialOrder.{u} E]  {D : Type v} [PartialOrder D] (f : E →o D) (c : OAI.Thomason.NormalizedChains.Chains E) :      OAI.Thomason.NormalizedChains.emptyCoefficient (OAI.Thomason.NormalizedChains.map f c) = OAI.Thomason.NormalizedChains.emptyCoefficient c := by    classical    induction c using Finsupp.induction with    | zero => simp []    | @single_add l z c _ _ ih =>      simp only [map_add, ih]      congr 1      have hz : Finsupp.single l z = z • OAI.Thomason.NormalizedChains.bracket l.val := by        rw [proof_bracket_of_pairwise_22 l.property]        simp only [Finsupp.smul_single, smul_eq_mul, mul_one]      rw [hz]      simp only [map_smul, proof_map_bracket_63 _ (l.property.imp fun h => le_of_lt h),        proof_emptyCoefficient_bracket_69, proof_emptyCoefficient_bracket_70, List.map_eq_nil_iff]  have proof_linearCombination_positive_71 {E : Type u} [instLocal1 : PartialOrder.{u} E]  {D : Type v} [PartialOrder D]      (H : OAI.Thomason.NormalizedChains.Word E → OAI.Thomason.NormalizedChains.Chains D) (hH : ∀ w, OAI.Thomason.NormalizedChains.Positive (H w))      {c : OAI.Thomason.NormalizedChains.Chains E} (hc : OAI.Thomason.NormalizedChains.Positive c) :      OAI.Thomason.NormalizedChains.Positive (Finsupp.linearCombination ℤ H c) := by    intro w    rw [Finsupp.linearCombination_apply, Finsupp.sum]    simp only [Finset.sum_apply, Finsupp.coe_finsetSum]    apply Finset.sum_nonneg    intro i _    exact mul_nonneg (hc i) (hH i w)  have proof_bracket_positive_72 {E : Type v} [instLocal1 : PartialOrder.{v} E]  (l : List E) : OAI.Thomason.NormalizedChains.Positive (OAI.Thomason.NormalizedChains.bracket l) := by    classical    intro w    by_cases h : l.Pairwise (· < ·)    · simp [proof_bracket_of_pairwise_47 h, Finsupp.single_apply]      split <;> omega    · simp [proof_bracket_of_not_pairwise_48 h]  have proof_map_positive_45 {E : Type u} [instLocal1 : PartialOrder.{u} E]  {D : Type v} [PartialOrder D] (f : E →o D)      {c : OAI.Thomason.NormalizedChains.Chains E} (hc : OAI.Thomason.NormalizedChains.Positive c) : OAI.Thomason.NormalizedChains.Positive (OAI.Thomason.NormalizedChains.map f c) :=    proof_linearCombination_positive_71 _ (fun w => proof_bracket_positive_72 (w.val.map f)) hc  exact {    map p :=      { toFun := fun c => ⟨OAI.Thomason.NormalizedChains.map f c.val, proof_map_mem_grade_42 f c.property⟩        map_zero' := Subtype.ext (map_zero _)        map_add' := fun x y => Subtype.ext (map_add _ x.val y.val) }    map_d p x := Subtype.ext (proof_map_boundary_43 f x.val)    map_augmentation x := by      change OAI.Thomason.NormalizedChains.emptyCoefficient (OAI.Thomason.NormalizedChains.boundary (OAI.Thomason.NormalizedChains.map f x.val)) = OAI.Thomason.NormalizedChains.emptyCoefficient (OAI.Thomason.NormalizedChains.boundary x.val)      rw [← proof_map_boundary_43, proof_emptyCoefficient_map_44]    map_positive p x hx := proof_map_positive_45 f hx  }end OAI.Thomason.NormalizedChainsendsectionnamespace OAI.Thomason.NormalizedChainsvariable {E : Type u} [PartialOrder E]open CategoryTheorynoncomputable def simplexComplexes : SimplexCategory ⥤ OAI.Thomason.DirectedComplex.{0} := by  classical  have proof_bracket_of_pairwise_75 {E : Type 0} [instLocal1 : PartialOrder.{0} E]  {l : List E} (h : l.Pairwise (· < ·)) :      OAI.Thomason.NormalizedChains.bracket l = Finsupp.single ⟨l, h⟩ 1 := by    classical    simp [OAI.Thomason.NormalizedChains.bracket, h]  have proof_pairwise_of_map_76 {E : Type 0} [instLocal1 : PartialOrder.{0} E] {D : Type 0} [instLocal3 : PartialOrder.{0} D]  {l : List E} (h : l.Pairwise (· ≤ ·)) (f : E → D)      (hf : (l.map f).Pairwise (· < ·)) : l.Pairwise (· < ·) := by    apply (h.and (List.pairwise_map.mp hf)).imp    intro a b hab    exact lt_of_le_of_ne hab.1 (fun he => (ne_of_lt hab.2) (congrArg f he))  have proof_bracket_of_not_pairwise_77 {E : Type 0} [instLocal1 : PartialOrder.{0} E]  {l : List E} (h : ¬l.Pairwise (· < ·)) :      OAI.Thomason.NormalizedChains.bracket l = 0 := by    classical    simp [OAI.Thomason.NormalizedChains.bracket, h]  have proof_map_bracket_78 {E : Type 0} [instLocal1 : PartialOrder.{0} E] {D : Type 0} [instLocal3 : PartialOrder.{0} D]  (f : E →o D) {l : List E} (h : l.Pairwise (· ≤ ·)) :      OAI.Thomason.NormalizedChains.map f (OAI.Thomason.NormalizedChains.bracket l) = OAI.Thomason.NormalizedChains.bracket (l.map f) := by    classical    by_cases hs : l.Pairwise (· < ·)    · rw [proof_bracket_of_pairwise_75 hs]      change Finsupp.linearCombination ℤ (fun l : OAI.Thomason.NormalizedChains.Word E => OAI.Thomason.NormalizedChains.bracket (l.val.map f))        (Finsupp.single (⟨l, hs⟩ : OAI.Thomason.NormalizedChains.Word E) 1) = _      rw [Finsupp.linearCombination_single]      simp    · have hf : ¬(l.map f).Pairwise (· < ·) := fun hm => hs (proof_pairwise_of_map_76 h f hm)      simp [proof_bracket_of_not_pairwise_77 hs, proof_bracket_of_not_pairwise_77 hf]  have proof_map_id_79 {E : Type 0} [instLocal1 : PartialOrder.{0} E]  (c : OAI.Thomason.NormalizedChains.Chains E) : OAI.Thomason.NormalizedChains.map (OrderHom.id) c = c := by    classical    induction c using Finsupp.induction with    | zero => simp    | @single_add l z c _ _ ih =>      simp only [map_add, ih]      congr 1      have hz : Finsupp.single l z = z • OAI.Thomason.NormalizedChains.bracket l.val := by        rw [proof_bracket_of_pairwise_75 l.property]        simp only [Finsupp.smul_single, smul_eq_mul, mul_one]      rw [hz, map_smul, proof_map_bracket_78 _ (l.property.imp fun h => le_of_lt h)]      simp  have proof_complexMap_id_73 {E : Type 0} [instLocal1 : PartialOrder.{0} E]  : OAI.Thomason.NormalizedChains.complexMap (OrderHom.id : E →o E) =      OAI.Thomason.DirectedComplex.Hom.id (OAI.Thomason.NormalizedChains.complex E) := by    ext p x    apply Subtype.ext    exact proof_map_id_79 x.val  have proof_map_comp_80 {E : Type 0} [instLocal1 : PartialOrder.{0} E] {D : Type 0} [instLocal3 : PartialOrder.{0} D] {B : Type 0} [instLocal5 : PartialOrder.{0} B]  (f : E →o D) (g : D →o B) (c : OAI.Thomason.NormalizedChains.Chains E) :      OAI.Thomason.NormalizedChains.map (g.comp f) c = OAI.Thomason.NormalizedChains.map g (OAI.Thomason.NormalizedChains.map f c) := by    classical    induction c using Finsupp.induction with    | zero => simp    | @single_add l z c _ _ ih =>      simp only [map_add, ih]      congr 1      have hz : Finsupp.single l z = z • OAI.Thomason.NormalizedChains.bracket l.val := by        rw [proof_bracket_of_pairwise_75 l.property]        simp only [Finsupp.smul_single, smul_eq_mul, mul_one]      have hl := l.property.imp fun h => le_of_lt h      rw [hz]      simp only [map_smul]      rw [proof_map_bracket_78 _ hl, proof_map_bracket_78 _ hl,        proof_map_bracket_78 _ (List.pairwise_map.mpr (hl.imp fun hh => f.monotone hh))]      simp [List.map_map]  have proof_complexMap_comp_74 {E : Type 0} [instLocal1 : PartialOrder.{0} E]  {D : Type 0} [PartialOrder D] {B : Type 0} [PartialOrder B]      (f : E →o D) (g : D →o B) : OAI.Thomason.NormalizedChains.complexMap (g.comp f) =        OAI.Thomason.DirectedComplex.Hom.comp (OAI.Thomason.NormalizedChains.complexMap f) (OAI.Thomason.NormalizedChains.complexMap g) := by    ext p x    apply Subtype.ext    exact proof_map_comp_80 f g x.val  exact {    obj m := OAI.Thomason.NormalizedChains.complex (Fin (m.len+1))    map f := OAI.Thomason.NormalizedChains.complexMap f.toOrderHom    map_id _ := proof_complexMap_id_73    map_comp f g := proof_complexMap_comp_74 f.toOrderHom g.toOrderHom  }end OAI.Thomason.NormalizedChainsendsectionnamespace OAI.Thomasonopen CategoryTheory Oppositenoncomputable def orientals : SimplexCategory ⥤ OAI.Thomason.OmegaCategory.{0} :=  OAI.Thomason.NormalizedChains.simplexComplexes ⋙ OAI.Thomason.DirectedComplex.nuFunctorend OAI.Thomasonendsectionnamespace OAI.Thomason.OmegaCategorynoncomputable def ulift (C : OAI.Thomason.OmegaCategory.{u}) : OAI.Thomason.OmegaCategory.{max u v} where  Cell := ULift.{v} C.Cell  source k x := ⟨C.source k x.down⟩  target k x := ⟨C.target k x.down⟩  source_source i j x := congrArg ULift.up (C.source_source i j x.down)  target_target i j x := congrArg ULift.up (C.target_target i j x.down)  source_target i j x := by    simpa only [apply_ite] using congrArg (ULift.up (α := C.Cell)) (C.source_target i j x.down)  target_source i j x := by    simpa only [apply_ite] using congrArg (ULift.up (α := C.Cell)) (C.target_source i j x.down)  comp k x y h := ⟨C.comp k x.down y.down (congrArg ULift.down h)⟩  source_comp_le i k hik x y h :=    congrArg ULift.up (C.source_comp_le i k hik x.down y.down (congrArg ULift.down h))  target_comp_le i k hik x y h :=    congrArg ULift.up (C.target_comp_le i k hik x.down y.down (congrArg ULift.down h))  source_comp_gt i k hki x y h hs :=    congrArg ULift.up (C.source_comp_gt i k hki x.down y.down      (congrArg ULift.down h) (congrArg ULift.down hs))  target_comp_gt i k hki x y h ht :=    congrArg ULift.up (C.target_comp_gt i k hki x.down y.down      (congrArg ULift.down h) (congrArg ULift.down ht))  unit_left k x h := congrArg ULift.up (C.unit_left k x.down (congrArg ULift.down h))  unit_right k x h := congrArg ULift.up (C.unit_right k x.down (congrArg ULift.down h))  assoc k x y z hxy hyz hxy_z hx_yz :=    congrArg ULift.up (C.assoc k x.down y.down z.down      (congrArg ULift.down hxy) (congrArg ULift.down hyz)      (congrArg ULift.down hxy_z) (congrArg ULift.down hx_yz))  interchange k l hkl a b c d hab hcd hac hbd h₁ h₂ :=    congrArg ULift.up (C.interchange k l hkl a.down b.down c.down d.down      (congrArg ULift.down hab) (congrArg ULift.down hcd)      (congrArg ULift.down hac) (congrArg ULift.down hbd)      (congrArg ULift.down h₁) (congrArg ULift.down h₂))  finite_dimension x := by    obtain ⟨k, hk⟩ := C.finite_dimension x.down    exact ⟨k, congrArg ULift.up hk⟩noncomputable def uliftUp (C : OAI.Thomason.OmegaCategory.{u}) : OAI.Thomason.OmegaCategory.Functor C (OAI.Thomason.OmegaCategory.ulift.{u,v} C) where  map := ULift.up  map_source _ _ := rfl  map_target _ _ := rfl  map_comp _ _ _ _ _ := rflnoncomputable def uliftDown (C : OAI.Thomason.OmegaCategory.{u}) : OAI.Thomason.OmegaCategory.Functor (OAI.Thomason.OmegaCategory.ulift.{u,v} C) C where  map := ULift.down  map_source _ _ := rfl  map_target _ _ := rfl  map_comp _ _ _ _ _ := rflend OAI.Thomason.OmegaCategoryendsectionnamespace OAI.Thomason.OmegaCategoryopen CategoryTheorynoncomputable def uliftFunctor : OAI.Thomason.OmegaCategory.{u} ⥤ OAI.Thomason.OmegaCategory.{max u v} where  obj := OAI.Thomason.OmegaCategory.ulift  map {C D} F := OAI.Thomason.OmegaCategory.Functor.comp (OAI.Thomason.OmegaCategory.Functor.comp (OAI.Thomason.OmegaCategory.uliftDown C) F) (OAI.Thomason.OmegaCategory.uliftUp D)end OAI.Thomason.OmegaCategoryendsectionnamespace OAI.Thomasonopen CategoryTheory Oppositenoncomputable def raisedOrientals : SimplexCategory ⥤ OAI.Thomason.OmegaCategory.{u} :=  OAI.Thomason.orientals ⋙ OAI.Thomason.OmegaCategory.uliftFunctor.{0,u}end OAI.Thomasonendsectionnamespace OAI.Thomason.OmegaCategorystructure Presentation where  Generator : Type u  dimension : Generator → ℕ  relations : (C : OAI.Thomason.OmegaCategory.{u}) → (Generator → C.Cell) → Propend OAI.Thomason.OmegaCategoryendsectionnamespace OAI.Thomason.OmegaCategory.Presentationvariable (P : Presentation.{u})structure Interpretation (C : OAI.Thomason.OmegaCategory.{u}) where  map : P.Generator → C.Cell  bounded : ∀ g, C.source (P.dimension g) (map g) = map g  satisfies : P.relations C mapend OAI.Thomason.OmegaCategory.Presentationendsectionnamespace OAI.Thomason.OmegaCategoryinductive CellTerm (G : Type u) where  | gen : G → CellTerm G  | source : ℕ → CellTerm G → CellTerm G  | target : ℕ → CellTerm G → CellTerm G  | comp : ℕ → CellTerm G → CellTerm G → CellTerm Gend OAI.Thomason.OmegaCategoryendsectionnamespace OAI.Thomason.OmegaCategory.CellTermnoncomputable def composeOrLeft (C : OAI.Thomason.OmegaCategory.{v}) (k : ℕ) (x y : C.Cell) : C.Cell := by  classical  exact if h : C.target k x = C.source k y then C.comp k x y h else xnoncomputable def eval {G : Type u} (C : OAI.Thomason.OmegaCategory.{v}) (f : G → C.Cell) : OAI.Thomason.OmegaCategory.CellTerm G → C.Cell  | gen g => f g  | source k x => C.source k (eval C f x)  | target k x => C.target k (eval C f x)  | comp k x y => OAI.Thomason.OmegaCategory.CellTerm.composeOrLeft C k (eval C f x) (eval C f y)end OAI.Thomason.OmegaCategory.CellTermendsectionnamespace OAI.Thomason.OmegaCategory.Presentationvariable (P : Presentation.{u})noncomputable def Equiv (x y : OAI.Thomason.OmegaCategory.CellTerm P.Generator) : Prop :=  ∀ (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C), x.eval C I.map = y.eval C I.mapinductive Valid : OAI.Thomason.OmegaCategory.CellTerm P.Generator → Prop  | gen (g) : Valid (.gen g)  | source (k x) : Valid x → Valid (.source k x)  | target (k x) : Valid x → Valid (.target k x)  | comp (k x y) : Valid x → Valid y → P.Equiv (.target k x) (.source k y) → Valid (.comp k x y)noncomputable abbrev ValidTerm := {x : OAI.Thomason.OmegaCategory.CellTerm P.Generator // P.Valid x}noncomputable instance termSetoid : Setoid P.ValidTerm := by  classical  have proof_refl_81 {P : OAI.Thomason.OmegaCategory.Presentation.{u}}  (x : OAI.Thomason.OmegaCategory.CellTerm P.Generator) : P.Equiv x x := fun _ _ => rfl  have proof_symm_82 {P : OAI.Thomason.OmegaCategory.Presentation.{u}} {x : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)} {y : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)}  (h : P.Equiv x y) : P.Equiv y x := fun C I => (h C I).symm  have proof_trans_83 {P : OAI.Thomason.OmegaCategory.Presentation.{u}} {x : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)} {y : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)} {z : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)}  (h : P.Equiv x y) (h' : P.Equiv y z) : P.Equiv x z :=    fun C I => (h C I).trans (h' C I)  exact {    r x y := P.Equiv x.val y.val    iseqv := ⟨fun _ => proof_refl_81 _, fun h => (proof_symm_82 h), fun h h' => (proof_trans_83 h h')⟩  }noncomputable abbrev Cells := Quotient P.termSetoidnoncomputable def evaluate (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) : P.Cells → C.Cell :=  Quotient.lift (fun x : P.ValidTerm => x.val.eval C I.map) (fun _ _ h => h C I)end OAI.Thomason.OmegaCategory.Presentationendsectionnamespace OAI.Thomason.OmegaCategory.CellTermnoncomputable def dimension {G : Type u} (d : G → ℕ) : OAI.Thomason.OmegaCategory.CellTerm G → ℕ  | gen g => d g  | source k _ => k  | target k _ => k  | comp k x y => max (k+1) (max (dimension d x) (dimension d y))end OAI.Thomason.OmegaCategory.CellTermendsectionnamespace OAI.Thomason.OmegaCategory.Presentationvariable (P : Presentation.{u})noncomputable def sourceTerm (k : ℕ) (x : P.ValidTerm) : P.ValidTerm := ⟨.source k x.val, OAI.Thomason.OmegaCategory.Presentation.Valid.source (P := P) k x.val x.property⟩noncomputable def source (k : ℕ) : P.Cells → P.Cells := by  classical  have proof_source_84 {P : OAI.Thomason.OmegaCategory.Presentation.{u}} {x : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)} {y : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)}  (k : ℕ) (h : P.Equiv x y) : P.Equiv (.source k x) (.source k y) :=    fun C I => congrArg (C.source k) (h C I)  exact    Quotient.map (P.sourceTerm k) (fun _ _ h => (proof_source_84 k h))noncomputable def targetTerm (k : ℕ) (x : P.ValidTerm) : P.ValidTerm := ⟨.target k x.val, OAI.Thomason.OmegaCategory.Presentation.Valid.target (P := P) k x.val x.property⟩noncomputable def target (k : ℕ) : P.Cells → P.Cells := by  classical  have proof_target_85 {P : OAI.Thomason.OmegaCategory.Presentation.{u}} {x : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)} {y : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)}  (k : ℕ) (h : P.Equiv x y) : P.Equiv (.target k x) (.target k y) :=    fun C I => congrArg (C.target k) (h C I)  exact    Quotient.map (P.targetTerm k) (fun _ _ h => (proof_target_85 k h))noncomputable def compTerm (k : ℕ) (x y : P.ValidTerm) : P.ValidTerm := by  classical  exact if h : P.Equiv (.target k x.val) (.source k y.val) then    ⟨.comp k x.val y.val, OAI.Thomason.OmegaCategory.Presentation.Valid.comp (P := P) k x.val y.val x.property y.property h⟩ else xnoncomputable def comp (k : ℕ) (x y : P.Cells) (_ : P.target k x = P.source k y) : P.Cells := by  classical  have proof_trans_83 {P : OAI.Thomason.OmegaCategory.Presentation.{u}} {x : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)} {y : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)} {z : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)}  (h : P.Equiv x y) (h' : P.Equiv y z) : P.Equiv x z :=    fun C I => (h C I).trans (h' C I)  have proof_symm_82 {P : OAI.Thomason.OmegaCategory.Presentation.{u}} {x : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)} {y : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)}  (h : P.Equiv x y) : P.Equiv y x := fun C I => (h C I).symm  have proof_target_85 {P : OAI.Thomason.OmegaCategory.Presentation.{u}} {x : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)} {y : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)}  (k : ℕ) (h : P.Equiv x y) : P.Equiv (.target k x) (.target k y) :=    fun C I => congrArg (C.target k) (h C I)  have proof_source_84 {P : OAI.Thomason.OmegaCategory.Presentation.{u}} {x : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)} {y : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)}  (k : ℕ) (h : P.Equiv x y) : P.Equiv (.source k x) (.source k y) :=    fun C I => congrArg (C.source k) (h C I)  have proof_composable_congr_87 {P : OAI.Thomason.OmegaCategory.Presentation.{u}} {x : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)} {y : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)} {x' : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)} {y' : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)}  (k : ℕ) (hx : P.Equiv x x') (hy : P.Equiv y y') :      P.Equiv (.target k x) (.source k y) ↔ P.Equiv (.target k x') (.source k y') :=    ⟨fun h => (proof_trans_83    (proof_symm_82 (proof_target_85 k hx))    (proof_trans_83 h (proof_source_84 k hy))),     fun h => (proof_trans_83 (proof_target_85 k hx)    (proof_trans_83 h      (proof_symm_82 (proof_source_84 k hy))))⟩  have proof_comp_88 {P : OAI.Thomason.OmegaCategory.Presentation.{u}} {x : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)} {y : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)} {x' : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)} {y' : OAI.Thomason.OmegaCategory.CellTerm.{u} (OAI.Thomason.OmegaCategory.Presentation.Generator.{u} P)}  (k : ℕ) (hx : P.Equiv x x') (hy : P.Equiv y y') :      P.Equiv (.comp k x y) (.comp k x' y') := by    intro C I    exact congrArg₂ (OAI.Thomason.OmegaCategory.CellTerm.composeOrLeft C k) (hx C I) (hy C I)  have proof_compTerm_equiv_86 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (k : ℕ) {x y x' y' : P.ValidTerm}      (hx : P.Equiv x.val x'.val) (hy : P.Equiv y.val y'.val) :      P.Equiv (P.compTerm k x y).val (P.compTerm k x' y').val := by    classical    have he := proof_composable_congr_87 k hx hy    by_cases h : P.Equiv (.target k x.val) (.source k y.val)    · simp only [OAI.Thomason.OmegaCategory.Presentation.compTerm, dite_eq_left h, dite_eq_left (he.mp h)]      exact proof_comp_88 k hx hy    · simp only [OAI.Thomason.OmegaCategory.Presentation.compTerm, dite_eq_right h, dite_eq_right (mt he.mpr h)]      exact hx  exact    Quotient.map₂ (P.compTerm k) (fun _ _ hx _ _ hy => (proof_compTerm_equiv_86 P k hx hy)) x ynoncomputable abbrev category : OAI.Thomason.OmegaCategory.{u} := by  classical  have proof_cells_ext_89 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  {x y : P.Cells}      (h : ∀ (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C), P.evaluate C I x = P.evaluate C I y) : x = y := by    induction x using Quotient.inductionOn with | h x =>      induction y using Quotient.inductionOn with | h y =>        exact Quotient.sound h  have proof_evaluate_source_90 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) (k : ℕ) (x : P.Cells) :      P.evaluate C I (P.source k x) = C.source k (P.evaluate C I x) := by    induction x using Quotient.inductionOn    rfl  have proof_evaluate_target_91 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) (k : ℕ) (x : P.Cells) :      P.evaluate C I (P.target k x) = C.target k (P.evaluate C I x) := by    induction x using Quotient.inductionOn    rfl  have proof_evaluate_composable_94 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) (k : ℕ)      (x y : P.Cells) (h : P.target k x = P.source k y) :      C.target k (P.evaluate C I x) = C.source k (P.evaluate C I y) := by    rw [← proof_evaluate_target_91, ← proof_evaluate_source_90, h]  have proof_evaluate_comp_92 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) (k : ℕ)      (x y : P.Cells) (h : P.target k x = P.source k y) :      P.evaluate C I (P.comp k x y h) =        C.comp k (P.evaluate C I x) (P.evaluate C I y) (proof_evaluate_composable_94 P C I k x y h) := by    induction x using Quotient.inductionOn with | h x =>      induction y using Quotient.inductionOn with | h y =>        have hm : P.Equiv (.target k x.val) (.source k y.val) := Quotient.exact h        change (P.compTerm k x y).val.eval C I.map = _        have hm' : C.target k (x.val.eval C I.map) = C.source k (y.val.eval C I.map) := hm C I        simp only [OAI.Thomason.OmegaCategory.Presentation.compTerm, dite_eq_left hm, OAI.Thomason.OmegaCategory.CellTerm.eval, OAI.Thomason.OmegaCategory.CellTerm.composeOrLeft, dite_eq_left hm']        rfl  have proof_source_source_self_95 (C : OAI.Thomason.OmegaCategory.{u})  (k : ℕ) (x : C.Cell) :      C.source k (C.source k x) = C.source k x := by    simp [C.source_source]  have proof_source_target_self_96 (C : OAI.Thomason.OmegaCategory.{u})  (k : ℕ) (x : C.Cell) :      C.source k (C.target k x) = C.target k x := by    simp [C.source_target]  have proof_source_composable_97 (C : OAI.Thomason.OmegaCategory.{u})  {k i : ℕ} (hki : k < i) {x y : C.Cell}      (h : C.target k x = C.source k y) :      C.target k (C.source i x) = C.source k (C.source i y) := by    rw [C.target_source, ite_eq_left hki, C.source_source, min_eq_left (le_of_lt hki)]    exact h  have proof_source_fixed_upwards_98 (C : OAI.Thomason.OmegaCategory.{u})  {i j : ℕ} (hij : i ≤ j) {x : C.Cell}      (h : C.source i x = x) : C.source j x = x := by    rw [← h, C.source_source, min_eq_right hij]  have proof_eval_dimension_93 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  {x : OAI.Thomason.OmegaCategory.CellTerm P.Generator} (hx : P.Valid x)      (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) :      C.source (x.dimension P.dimension) (x.eval C I.map) = x.eval C I.map := by    induction hx with    | gen g => exact I.bounded g    | source k x hx ih => exact (proof_source_source_self_95 C k    (OAI.Thomason.OmegaCategory.CellTerm.eval C (OAI.Thomason.OmegaCategory.Presentation.Interpretation.map I) x))    | target k x hx ih => exact (proof_source_target_self_96 C k    (OAI.Thomason.OmegaCategory.CellTerm.eval C (OAI.Thomason.OmegaCategory.Presentation.Interpretation.map I) x))    | comp k x y hx hy h ihx ihy =>      have hm := h C I      change C.target k (x.eval C I.map) = C.source k (y.eval C I.map) at hm      simp only [OAI.Thomason.OmegaCategory.CellTerm.dimension, OAI.Thomason.OmegaCategory.CellTerm.eval, OAI.Thomason.OmegaCategory.CellTerm.composeOrLeft, dite_eq_left hm]      have hkn : k < max (k+1) (max (x.dimension P.dimension) (y.dimension P.dimension)) := by omega      rw [C.source_comp_gt _ k hkn _ _ hm (proof_source_composable_97 C hkn hm)]      congr 1      · exact (proof_source_fixed_upwards_98 C (by omega) ihx)      · exact (proof_source_fixed_upwards_98 C (by omega) ihy)  exact {    Cell := P.Cells    source := P.source    target := P.target    comp := P.comp    source_source i j x := by      apply (proof_cells_ext_89 P)      intro C I      simp only [proof_evaluate_source_90, C.source_source]    target_target i j x := by      apply (proof_cells_ext_89 P)      intro C I      simp only [proof_evaluate_target_91, C.target_target]    source_target i j x := by      apply (proof_cells_ext_89 P)      intro C I      by_cases hij : i < j <;> simp [proof_evaluate_source_90, proof_evaluate_target_91, hij, C.source_target]    target_source i j x := by      apply (proof_cells_ext_89 P)      intro C I      by_cases hij : i < j <;> simp [proof_evaluate_source_90, proof_evaluate_target_91, hij, C.target_source]    source_comp_le i k hik x y h := by      apply (proof_cells_ext_89 P)      intro C I      simp only [proof_evaluate_source_90, proof_evaluate_comp_92]      exact C.source_comp_le i k hik _ _ _    target_comp_le i k hik x y h := by      apply (proof_cells_ext_89 P)      intro C I      simp only [proof_evaluate_target_91, proof_evaluate_comp_92]      exact C.target_comp_le i k hik _ _ _    source_comp_gt i k hki x y h hs := by      apply (proof_cells_ext_89 P)      intro C I      simp only [proof_evaluate_source_90, proof_evaluate_comp_92]      exact C.source_comp_gt i k hki _ _ _ _    target_comp_gt i k hki x y h hs := by      apply (proof_cells_ext_89 P)      intro C I      simp only [proof_evaluate_target_91, proof_evaluate_comp_92]      exact C.target_comp_gt i k hki _ _ _ _    unit_left k x h := by      apply (proof_cells_ext_89 P)      intro C I      simp only [proof_evaluate_source_90, proof_evaluate_comp_92]      exact C.unit_left k _ _    unit_right k x h := by      apply (proof_cells_ext_89 P)      intro C I      simp only [proof_evaluate_target_91, proof_evaluate_comp_92]      exact C.unit_right k _ _    assoc k x y z hxy hyz hxy_z hx_yz := by      apply (proof_cells_ext_89 P)      intro C I      simp only [proof_evaluate_comp_92]      exact C.assoc k _ _ _ _ _ _ _    interchange k l hkl a b c d hab hcd hac hbd hab_cd hac_bd := by      apply (proof_cells_ext_89 P)      intro C I      simp only [proof_evaluate_comp_92]      exact C.interchange k l hkl _ _ _ _ _ _ _ _ _ _    finite_dimension x := by      induction x using Quotient.inductionOn with | h x =>        refine ⟨x.val.dimension P.dimension, ?_⟩        apply (proof_cells_ext_89 P)        intro C I        exact (proof_eval_dimension_93 P (Subtype.property x) C I)  }end OAI.Thomason.OmegaCategory.Presentationendsectionnamespace OAI.Thomason.OmegaCategoryopen CategoryTheory Limitsvariable {J : Type u} [Category.{u} J]noncomputable abbrev colimitPresentation (F : J ⥤ OAI.Thomason.OmegaCategory.{u}) : OAI.Thomason.OmegaCategory.Presentation.{u} where  Generator := (j : J) × (F.obj j).Cell  dimension g := Classical.choose ((F.obj g.1).finite_dimension g.2)  relations C f := ∃ ι : ∀ j, OAI.Thomason.OmegaCategory.Functor (F.obj j) C,    (∀ j x, f ⟨j, x⟩ = (ι j).map x) ∧    (∀ ⦃j j'⦄ (a : j ⟶ j'), OAI.Thomason.OmegaCategory.Functor.comp (F.map a) (ι j') = ι j)end OAI.Thomason.OmegaCategoryendsectionnamespace OAI.Thomason.OmegaCategory.Presentationvariable (P : Presentation.{u})noncomputable def generator (g : P.Generator) : P.Cells := Quotient.mk _ ⟨.gen g, .gen g⟩end OAI.Thomason.OmegaCategory.Presentationendsectionnamespace OAI.Thomason.OmegaCategoryopen CategoryTheory Limitsvariable {J : Type u} [Category.{u} J]noncomputable def colimitInclusion (F : J ⥤ OAI.Thomason.OmegaCategory.{u}) (j : J) :    OAI.Thomason.OmegaCategory.Functor (F.obj j) (OAI.Thomason.OmegaCategory.colimitPresentation F).category := by  classical  have proof_cells_ext_89 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  {x y : P.Cells}      (h : ∀ (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C), P.evaluate C I x = P.evaluate C I y) : x = y := by    induction x using Quotient.inductionOn with | h x =>      induction y using Quotient.inductionOn with | h y =>        exact Quotient.sound h  have proof_evaluate_source_90 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) (k : ℕ) (x : P.Cells) :      P.evaluate C I (P.source k x) = C.source k (P.evaluate C I x) := by    induction x using Quotient.inductionOn    rfl  have proof_evaluate_target_91 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) (k : ℕ) (x : P.Cells) :      P.evaluate C I (P.target k x) = C.target k (P.evaluate C I x) := by    induction x using Quotient.inductionOn    rfl  have proof_evaluate_composable_94 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) (k : ℕ)      (x y : P.Cells) (h : P.target k x = P.source k y) :      C.target k (P.evaluate C I x) = C.source k (P.evaluate C I y) := by    rw [← proof_evaluate_target_91, ← proof_evaluate_source_90, h]  have proof_evaluate_comp_92 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) (k : ℕ)      (x y : P.Cells) (h : P.target k x = P.source k y) :      P.evaluate C I (P.comp k x y h) =        C.comp k (P.evaluate C I x) (P.evaluate C I y) (proof_evaluate_composable_94 P C I k x y h) := by    induction x using Quotient.inductionOn with | h x =>      induction y using Quotient.inductionOn with | h y =>        have hm : P.Equiv (.target k x.val) (.source k y.val) := Quotient.exact h        change (P.compTerm k x y).val.eval C I.map = _        have hm' : C.target k (x.val.eval C I.map) = C.source k (y.val.eval C I.map) := hm C I        simp only [OAI.Thomason.OmegaCategory.Presentation.compTerm, dite_eq_left hm, OAI.Thomason.OmegaCategory.CellTerm.eval, OAI.Thomason.OmegaCategory.CellTerm.composeOrLeft, dite_eq_left hm']        rfl  have proof_evaluate_generator_99  (P : OAI.Thomason.OmegaCategory.Presentation.{u}) (C : OAI.Thomason.OmegaCategory.{u})      (I : P.Interpretation C) (g : P.Generator) : P.evaluate C I (P.generator g) = I.map g := rfl  exact {    map x := (OAI.Thomason.OmegaCategory.colimitPresentation F).generator ⟨j, x⟩    map_source k x := by      apply (proof_cells_ext_89 (OAI.Thomason.OmegaCategory.colimitPresentation F))      intro C I      rcases I.satisfies with ⟨ι, hi, _⟩      simp only [proof_evaluate_source_90, proof_evaluate_generator_99, hi]      exact (ι j).map_source k x    map_target k x := by      apply (proof_cells_ext_89 (OAI.Thomason.OmegaCategory.colimitPresentation F))      intro C I      rcases I.satisfies with ⟨ι, hi, _⟩      simp only [proof_evaluate_target_91, proof_evaluate_generator_99, hi]      exact (ι j).map_target k x    map_comp k x y h h' := by      apply (proof_cells_ext_89 (OAI.Thomason.OmegaCategory.colimitPresentation F))      intro C I      rcases I.satisfies with ⟨ι, hi, _⟩      simp only [proof_evaluate_comp_92, proof_evaluate_generator_99, hi]      exact (ι j).map_comp k x y h _  }noncomputable def presentedCocone (F : J ⥤ OAI.Thomason.OmegaCategory.{u}) : Cocone F := by  classical  have proof_cells_ext_89 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  {x y : P.Cells}      (h : ∀ (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C), P.evaluate C I x = P.evaluate C I y) : x = y := by    induction x using Quotient.inductionOn with | h x =>      induction y using Quotient.inductionOn with | h y =>        exact Quotient.sound h  exact {    pt := (OAI.Thomason.OmegaCategory.colimitPresentation F).category    ι := {      app := OAI.Thomason.OmegaCategory.colimitInclusion F      naturality := by        intro j j' a        apply OAI.Thomason.OmegaCategory.Functor.ext        funext x        apply (proof_cells_ext_89 (OAI.Thomason.OmegaCategory.colimitPresentation F))        intro C I        rcases I.satisfies with ⟨ι, hi, hw⟩        change I.map ⟨j', (F.map a).map x⟩ = I.map ⟨j, x⟩        rw [hi, hi]        exact congrArg (fun h : OAI.Thomason.OmegaCategory.Functor (F.obj j) C => h.map x) (hw a) }  }end OAI.Thomason.OmegaCategoryendsectionnamespace OAI.Thomason.OmegaCategory.Presentationvariable (P : Presentation.{u})noncomputable def lift (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) : OAI.Thomason.OmegaCategory.Functor P.category C := by  classical  have proof_evaluate_source_90 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) (k : ℕ) (x : P.Cells) :      P.evaluate C I (P.source k x) = C.source k (P.evaluate C I x) := by    induction x using Quotient.inductionOn    rfl  have proof_evaluate_target_91 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) (k : ℕ) (x : P.Cells) :      P.evaluate C I (P.target k x) = C.target k (P.evaluate C I x) := by    induction x using Quotient.inductionOn    rfl  have proof_evaluate_composable_94 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) (k : ℕ)      (x y : P.Cells) (h : P.target k x = P.source k y) :      C.target k (P.evaluate C I x) = C.source k (P.evaluate C I y) := by    rw [← proof_evaluate_target_91, ← proof_evaluate_source_90, h]  have proof_evaluate_comp_92 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) (k : ℕ)      (x y : P.Cells) (h : P.target k x = P.source k y) :      P.evaluate C I (P.comp k x y h) =        C.comp k (P.evaluate C I x) (P.evaluate C I y) (proof_evaluate_composable_94 P C I k x y h) := by    induction x using Quotient.inductionOn with | h x =>      induction y using Quotient.inductionOn with | h y =>        have hm : P.Equiv (.target k x.val) (.source k y.val) := Quotient.exact h        change (P.compTerm k x y).val.eval C I.map = _        have hm' : C.target k (x.val.eval C I.map) = C.source k (y.val.eval C I.map) := hm C I        simp only [OAI.Thomason.OmegaCategory.Presentation.compTerm, dite_eq_left hm, OAI.Thomason.OmegaCategory.CellTerm.eval, OAI.Thomason.OmegaCategory.CellTerm.composeOrLeft, dite_eq_left hm']        rfl  exact {    map := P.evaluate C I    map_source := (proof_evaluate_source_90 P C I)    map_target := (proof_evaluate_target_91 P C I)    map_comp k x y h _ := (proof_evaluate_comp_92 P C I k x y h)  }end OAI.Thomason.OmegaCategory.Presentationendsectionnamespace OAI.Thomason.OmegaCategoryopen CategoryTheory Limitsvariable {J : Type u} [Category.{u} J]noncomputable def colimitInterpretation (F : J ⥤ OAI.Thomason.OmegaCategory.{u}) (s : Cocone F) :    (OAI.Thomason.OmegaCategory.colimitPresentation F).Interpretation s.pt where  map g := (s.ι.app g.1).map g.2  bounded g := by    exact ((s.ι.app g.1).map_source _ g.2).symm.trans      (congrArg (s.ι.app g.1).map (Classical.choose_spec ((F.obj g.1).finite_dimension g.2)))  satisfies := ⟨fun j => s.ι.app j, fun _ _ => rfl, fun {_ _} a => s.w a⟩noncomputable def presentedCoconeIsColimit (F : J ⥤ OAI.Thomason.OmegaCategory.{u}) :    IsColimit (OAI.Thomason.OmegaCategory.presentedCocone F) := by  classical  have proof_mk_comp_101 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (k : ℕ) (x y : P.ValidTerm)      (h : P.Equiv (.target k x.val) (.source k y.val))      (h' : P.target k (Quotient.mk _ x) = P.source k (Quotient.mk _ y)) :      P.comp k (Quotient.mk _ x) (Quotient.mk _ y) h' =        Quotient.mk _ ⟨.comp k x.val y.val, OAI.Thomason.OmegaCategory.Presentation.Valid.comp (P := P) k x.val y.val x.property y.property h⟩ := by    change Quotient.mk _ (P.compTerm k x y) = _    simp only [OAI.Thomason.OmegaCategory.Presentation.compTerm, dite_eq_left h]  have proof_map_composable_102 {C : OAI.Thomason.OmegaCategory.{u}} {D : OAI.Thomason.OmegaCategory.{u}}  (F : OAI.Thomason.OmegaCategory.Functor C D) {k : ℕ} {x y : C.Cell}      (h : C.target k x = C.source k y) :      D.target k (F.map x) = D.source k (F.map y) := by    rw [← F.map_target, ← F.map_source, h]  have proof_functor_ext_100 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  {C : OAI.Thomason.OmegaCategory.{u}} {F G : OAI.Thomason.OmegaCategory.Functor P.category C}      (h : ∀ g, F.map (P.generator g) = G.map (P.generator g)) : F = G := by    apply OAI.Thomason.OmegaCategory.Functor.ext    funext x    induction x using Quotient.inductionOn with | h x =>      rcases x with ⟨x, hx⟩      induction hx with      | gen g => exact h g      | source k x hx ih =>        change F.map (P.category.source k (Quotient.mk _ ⟨x, hx⟩)) =          G.map (P.category.source k (Quotient.mk _ ⟨x, hx⟩))        rw [F.map_source, G.map_source, ih]      | target k x hx ih =>        change F.map (P.category.target k (Quotient.mk _ ⟨x, hx⟩)) =          G.map (P.category.target k (Quotient.mk _ ⟨x, hx⟩))        rw [F.map_target, G.map_target, ih]      | comp k x y hx hy hm ihx ihy =>        have hc : P.category.target k (Quotient.mk _ ⟨x, hx⟩) =            P.category.source k (Quotient.mk _ ⟨y, hy⟩) := Quotient.sound hm        rw [← (proof_mk_comp_101 P k ⟨x, hx⟩ ⟨y, hy⟩ hm hc)]        change F.map (P.category.comp k _ _ hc) = G.map (P.category.comp k _ _ hc)        rw [F.map_comp k _ _ hc (proof_map_composable_102 F hc), G.map_comp k _ _ hc (proof_map_composable_102 G hc)]        congr 1  exact {    desc s := (OAI.Thomason.OmegaCategory.colimitPresentation F).lift s.pt (OAI.Thomason.OmegaCategory.colimitInterpretation F s)    fac s j := by      apply OAI.Thomason.OmegaCategory.Functor.ext      funext x      rfl    uniq s m hm := by      apply (proof_functor_ext_100 (OAI.Thomason.OmegaCategory.colimitPresentation F))      intro ⟨j, x⟩      exact congrArg (fun f : OAI.Thomason.OmegaCategory.Functor (F.obj j) s.pt => f.map x) (hm j)  }noncomputable instance hasColimits : HasColimitsOfSize.{u,u} OAI.Thomason.OmegaCategory.{u} where  has_colimits_of_shape := fun _ _ => { has_colimit := fun F => ⟨⟨OAI.Thomason.OmegaCategory.presentedCocone F, OAI.Thomason.OmegaCategory.presentedCoconeIsColimit F⟩⟩ }end OAI.Thomason.OmegaCategoryendsectionnamespace OAI.Thomasonopen CategoryTheory Oppositenoncomputable instance omegaHasSimplicialColimits :    Limits.HasColimitsOfSize.{0,u} OAI.Thomason.OmegaCategory.{u} :=  Limits.hasColimitsOfSizeShrink.{0,u} OAI.Thomason.OmegaCategory.{u}noncomputable def categorification : SSet.{u} ⥤ OAI.Thomason.OmegaCategory.{u} :=  (uliftYoneda.{u} : SimplexCategory ⥤ (SimplexCategoryᵒᵖ ⥤ Type u)).leftKanExtension OAI.Thomason.raisedOrientals.{u}end OAI.Thomasonendsectionnamespace OAI.Thomasonopen CategoryTheorynoncomputable def thomasonLeft : SSet.{u} ⥤ OAI.Thomason.OmegaCategory.{u} :=  (SSet.sd ⋙ SSet.sd) ⋙ OAI.Thomason.categorificationend OAI.Thomasonendsectionnamespace OAI.Thomasonopen CategoryTheory Oppositenoncomputable def streetNerve (C : OAI.Thomason.OmegaCategory.{u}) : SSet.{u} where  obj m := OAI.Thomason.OmegaCategory.Functor (OAI.Thomason.orientals.obj m.unop) C  map f := ↾fun x => OAI.Thomason.OmegaCategory.Functor.comp (OAI.Thomason.orientals.map f.unop) x  map_id m := by    apply ConcreteCategory.hom_ext    intro x    change OAI.Thomason.OmegaCategory.Functor.comp (OAI.Thomason.orientals.map (𝟙 m.unop)) x = x    rw [OAI.Thomason.orientals.map_id]    rfl  map_comp f g := by    apply ConcreteCategory.hom_ext    intro x    change OAI.Thomason.OmegaCategory.Functor.comp (OAI.Thomason.orientals.map (g.unop ≫ f.unop)) x =      OAI.Thomason.OmegaCategory.Functor.comp (OAI.Thomason.orientals.map g.unop)        (OAI.Thomason.OmegaCategory.Functor.comp (OAI.Thomason.orientals.map f.unop) x)    rw [OAI.Thomason.orientals.map_comp]    rflnoncomputable def streetNerveMap {C D : OAI.Thomason.OmegaCategory.{u}} (F : OAI.Thomason.OmegaCategory.Functor C D) :    OAI.Thomason.streetNerve C ⟶ OAI.Thomason.streetNerve D where  app _ := ↾fun x => OAI.Thomason.OmegaCategory.Functor.comp x F  naturality _ _ _ := rflnoncomputable def streetNerveFunctor : OAI.Thomason.OmegaCategory.{u} ⥤ SSet.{u} where  obj := OAI.Thomason.streetNerve  map := OAI.Thomason.streetNerveMapend OAI.Thomasonendsectionnamespace OAI.Thomasonopen CategoryTheorynoncomputable def thomasonRight : OAI.Thomason.OmegaCategory.{u} ⥤ SSet.{u} :=  OAI.Thomason.streetNerveFunctor ⋙ (SSet.ex ⋙ SSet.ex)end OAI.Thomasonendsectionnamespace OAI.Thomasonopen CategoryTheory Oppositenoncomputable def streetYonedaEquiv (C : OAI.Thomason.OmegaCategory.{u}) (m : SimplexCategoryᵒᵖ) :    ((Presheaf.restrictedULiftYoneda.{0} OAI.Thomason.raisedOrientals).obj C).obj m ≃      (OAI.Thomason.streetNerve C).obj m where  toFun F := OAI.Thomason.OmegaCategory.Functor.comp (OAI.Thomason.OmegaCategory.uliftUp _) F.down  invFun F := ULift.up (OAI.Thomason.OmegaCategory.Functor.comp (OAI.Thomason.OmegaCategory.uliftDown _) F)  left_inv _ := rfl  right_inv _ := rflnoncomputable def streetYonedaIso : Presheaf.restrictedULiftYoneda.{0} OAI.Thomason.raisedOrientals.{u} ≅    OAI.Thomason.streetNerveFunctor.{u} :=  NatIso.ofComponents (fun C =>    NatIso.ofComponents (fun m => (OAI.Thomason.streetYonedaEquiv C m).toIso) (by intros; rfl))      (by intros; rfl)noncomputable def categorificationAdjunction : OAI.Thomason.categorification.{u} ⊣ OAI.Thomason.streetNerveFunctor.{u} :=  (Presheaf.uliftYonedaAdjunction.{0}    ((uliftYoneda.{u} : SimplexCategory ⥤ (SimplexCategoryᵒᵖ ⥤ Type u)).leftKanExtension OAI.Thomason.raisedOrientals.{u})    ((uliftYoneda.{u} : SimplexCategory ⥤ (SimplexCategoryᵒᵖ ⥤ Type u)).leftKanExtensionUnit OAI.Thomason.raisedOrientals.{u})).ofNatIsoRight OAI.Thomason.streetYonedaIsoend OAI.Thomasonendsectionnamespace OAI.Thomasonopen CategoryTheorynoncomputable def thomasonAdjunction : OAI.Thomason.thomasonLeft.{u} ⊣ OAI.Thomason.thomasonRight.{u} :=  (SSet.sdExAdjunction.comp SSet.sdExAdjunction).comp OAI.Thomason.categorificationAdjunctionend OAI.Thomasonendsectionnamespace OAI.Thomason.OmegaCategorynoncomputable abbrev truncationPresentation (n : ℕ) (C : OAI.Thomason.OmegaCategory.{u}) : OAI.Thomason.OmegaCategory.Presentation.{u} where  Generator := C.Cell  dimension _ := n  relations D f := D.IsTruncated n ∧ ∃ F : OAI.Thomason.OmegaCategory.Functor C D, f = F.mapnoncomputable def truncationUnit (n : ℕ) (C : OAI.Thomason.OmegaCategory.{u}) :    OAI.Thomason.OmegaCategory.Functor C (OAI.Thomason.OmegaCategory.truncationPresentation n C).category := by  classical  have proof_cells_ext_89 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  {x y : P.Cells}      (h : ∀ (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C), P.evaluate C I x = P.evaluate C I y) : x = y := by    induction x using Quotient.inductionOn with | h x =>      induction y using Quotient.inductionOn with | h y =>        exact Quotient.sound h  have proof_evaluate_source_90 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) (k : ℕ) (x : P.Cells) :      P.evaluate C I (P.source k x) = C.source k (P.evaluate C I x) := by    induction x using Quotient.inductionOn    rfl  have proof_evaluate_target_91 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) (k : ℕ) (x : P.Cells) :      P.evaluate C I (P.target k x) = C.target k (P.evaluate C I x) := by    induction x using Quotient.inductionOn    rfl  have proof_evaluate_composable_94 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) (k : ℕ)      (x y : P.Cells) (h : P.target k x = P.source k y) :      C.target k (P.evaluate C I x) = C.source k (P.evaluate C I y) := by    rw [← proof_evaluate_target_91, ← proof_evaluate_source_90, h]  have proof_evaluate_comp_92 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) (k : ℕ)      (x y : P.Cells) (h : P.target k x = P.source k y) :      P.evaluate C I (P.comp k x y h) =        C.comp k (P.evaluate C I x) (P.evaluate C I y) (proof_evaluate_composable_94 P C I k x y h) := by    induction x using Quotient.inductionOn with | h x =>      induction y using Quotient.inductionOn with | h y =>        have hm : P.Equiv (.target k x.val) (.source k y.val) := Quotient.exact h        change (P.compTerm k x y).val.eval C I.map = _        have hm' : C.target k (x.val.eval C I.map) = C.source k (y.val.eval C I.map) := hm C I        simp only [OAI.Thomason.OmegaCategory.Presentation.compTerm, dite_eq_left hm, OAI.Thomason.OmegaCategory.CellTerm.eval, OAI.Thomason.OmegaCategory.CellTerm.composeOrLeft, dite_eq_left hm']        rfl  have proof_evaluate_generator_99  (P : OAI.Thomason.OmegaCategory.Presentation.{u}) (C : OAI.Thomason.OmegaCategory.{u})      (I : P.Interpretation C) (g : P.Generator) : P.evaluate C I (P.generator g) = I.map g := rfl  exact {    map := (OAI.Thomason.OmegaCategory.truncationPresentation n C).generator    map_source k x := by      apply (proof_cells_ext_89 (OAI.Thomason.OmegaCategory.truncationPresentation n C))      intro D I      rcases I.satisfies with ⟨_, F, hF⟩      simp only [proof_evaluate_source_90, proof_evaluate_generator_99, hF]      exact F.map_source k x    map_target k x := by      apply (proof_cells_ext_89 (OAI.Thomason.OmegaCategory.truncationPresentation n C))      intro D I      rcases I.satisfies with ⟨_, F, hF⟩      simp only [proof_evaluate_target_91, proof_evaluate_generator_99, hF]      exact F.map_target k x    map_comp k x y h h' := by      apply (proof_cells_ext_89 (OAI.Thomason.OmegaCategory.truncationPresentation n C))      intro D I      rcases I.satisfies with ⟨_, F, hF⟩      simp only [proof_evaluate_comp_92, proof_evaluate_generator_99, hF]      exact F.map_comp k x y h _  }noncomputable def truncation (n : ℕ) (C : OAI.Thomason.OmegaCategory.{u}) : OAI.Thomason.OmegaCategory.NCategory.{u} n := by  classical  have proof_cells_ext_89 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  {x y : P.Cells}      (h : ∀ (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C), P.evaluate C I x = P.evaluate C I y) : x = y := by    induction x using Quotient.inductionOn with | h x =>      induction y using Quotient.inductionOn with | h y =>        exact Quotient.sound h  have proof_evaluate_source_90 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (C : OAI.Thomason.OmegaCategory.{u}) (I : P.Interpretation C) (k : ℕ) (x : P.Cells) :      P.evaluate C I (P.source k x) = C.source k (P.evaluate C I x) := by    induction x using Quotient.inductionOn    rfl  have proof_truncation_isTruncated_103  (n : ℕ) (C : OAI.Thomason.OmegaCategory.{u}) :      (OAI.Thomason.OmegaCategory.truncationPresentation n C).category.IsTruncated n := by    intro x    apply (proof_cells_ext_89 (OAI.Thomason.OmegaCategory.truncationPresentation n C))    intro D I    rw [proof_evaluate_source_90]    exact I.satisfies.1 _  exact    ⟨(OAI.Thomason.OmegaCategory.truncationPresentation n C).category, proof_truncation_isTruncated_103 n C⟩noncomputable def truncationLift {n : ℕ} {C : OAI.Thomason.OmegaCategory.{u}} (D : OAI.Thomason.OmegaCategory.NCategory.{u} n)    (F : OAI.Thomason.OmegaCategory.Functor C D.val) : OAI.Thomason.OmegaCategory.Functor (OAI.Thomason.OmegaCategory.truncation n C).val D.val :=  (OAI.Thomason.OmegaCategory.truncationPresentation n C).lift D.val {    map := F.map    bounded := fun x => D.property (F.map x)    satisfies := ⟨D.property, F, rfl⟩ }end OAI.Thomason.OmegaCategoryendsectionnamespace OAI.Thomason.OmegaCategoryopen CategoryTheorynoncomputable def truncationFunctor (n : ℕ) : OAI.Thomason.OmegaCategory.{u} ⥤ OAI.Thomason.OmegaCategory.NCategory.{u} n := by  classical  have proof_mk_comp_101 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (k : ℕ) (x y : P.ValidTerm)      (h : P.Equiv (.target k x.val) (.source k y.val))      (h' : P.target k (Quotient.mk _ x) = P.source k (Quotient.mk _ y)) :      P.comp k (Quotient.mk _ x) (Quotient.mk _ y) h' =        Quotient.mk _ ⟨.comp k x.val y.val, OAI.Thomason.OmegaCategory.Presentation.Valid.comp (P := P) k x.val y.val x.property y.property h⟩ := by    change Quotient.mk _ (P.compTerm k x y) = _    simp only [OAI.Thomason.OmegaCategory.Presentation.compTerm, dite_eq_left h]  have proof_map_composable_102 {C : OAI.Thomason.OmegaCategory.{u}} {D : OAI.Thomason.OmegaCategory.{u}}  (F : OAI.Thomason.OmegaCategory.Functor C D) {k : ℕ} {x y : C.Cell}      (h : C.target k x = C.source k y) :      D.target k (F.map x) = D.source k (F.map y) := by    rw [← F.map_target, ← F.map_source, h]  have proof_functor_ext_100 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  {C : OAI.Thomason.OmegaCategory.{u}} {F G : OAI.Thomason.OmegaCategory.Functor P.category C}      (h : ∀ g, F.map (P.generator g) = G.map (P.generator g)) : F = G := by    apply OAI.Thomason.OmegaCategory.Functor.ext    funext x    induction x using Quotient.inductionOn with | h x =>      rcases x with ⟨x, hx⟩      induction hx with      | gen g => exact h g      | source k x hx ih =>        change F.map (P.category.source k (Quotient.mk _ ⟨x, hx⟩)) =          G.map (P.category.source k (Quotient.mk _ ⟨x, hx⟩))        rw [F.map_source, G.map_source, ih]      | target k x hx ih =>        change F.map (P.category.target k (Quotient.mk _ ⟨x, hx⟩)) =          G.map (P.category.target k (Quotient.mk _ ⟨x, hx⟩))        rw [F.map_target, G.map_target, ih]      | comp k x y hx hy hm ihx ihy =>        have hc : P.category.target k (Quotient.mk _ ⟨x, hx⟩) =            P.category.source k (Quotient.mk _ ⟨y, hy⟩) := Quotient.sound hm        rw [← (proof_mk_comp_101 P k ⟨x, hx⟩ ⟨y, hy⟩ hm hc)]        change F.map (P.category.comp k _ _ hc) = G.map (P.category.comp k _ _ hc)        rw [F.map_comp k _ _ hc (proof_map_composable_102 F hc), G.map_comp k _ _ hc (proof_map_composable_102 G hc)]        congr 1  have proof_truncation_functor_ext_104  {n : ℕ} {C D : OAI.Thomason.OmegaCategory.{u}}      {F G : OAI.Thomason.OmegaCategory.Functor (OAI.Thomason.OmegaCategory.truncation n C).val D}      (h : OAI.Thomason.OmegaCategory.Functor.comp (OAI.Thomason.OmegaCategory.truncationUnit n C) F = OAI.Thomason.OmegaCategory.Functor.comp (OAI.Thomason.OmegaCategory.truncationUnit n C) G) : F = G := by    apply (proof_functor_ext_100 (OAI.Thomason.OmegaCategory.truncationPresentation n C))    intro x    exact congrArg (fun H : OAI.Thomason.OmegaCategory.Functor C D => H.map x) h  exact {    obj := OAI.Thomason.OmegaCategory.truncation n    map {C D} F := OAI.Thomason.OmegaCategory.truncationLift (OAI.Thomason.OmegaCategory.truncation n D) (OAI.Thomason.OmegaCategory.Functor.comp F (OAI.Thomason.OmegaCategory.truncationUnit n D))    map_id C := by      apply proof_truncation_functor_ext_104      rfl    map_comp F G := by      apply proof_truncation_functor_ext_104      rfl  }end OAI.Thomason.OmegaCategoryendsectionnamespace OAI.Thomasonopen CategoryTheory Oppositenoncomputable def categorificationFinite (n : ℕ) : SSet.{u} ⥤ OAI.Thomason.OmegaCategory.NCategory.{u} n :=  OAI.Thomason.categorification ⋙ OAI.Thomason.OmegaCategory.truncationFunctor nend OAI.Thomasonendsectionnamespace OAI.Thomasonopen CategoryTheorynoncomputable def thomasonLeftFinite (n : ℕ) : SSet.{u} ⥤ OAI.Thomason.OmegaCategory.NCategory.{u} n :=  (SSet.sd ⋙ SSet.sd) ⋙ OAI.Thomason.categorificationFinite nend OAI.Thomasonendsectionnamespace OAI.Thomasonopen CategoryTheory Oppositenoncomputable def streetNerveFinite (n : ℕ) : OAI.Thomason.OmegaCategory.NCategory.{u} n ⥤ SSet.{u} where  obj C := OAI.Thomason.streetNerve C.val  map := OAI.Thomason.streetNerveMapend OAI.Thomasonendsectionnamespace OAI.Thomasonopen CategoryTheorynoncomputable def thomasonRightFinite (n : ℕ) : OAI.Thomason.OmegaCategory.NCategory.{u} n ⥤ SSet.{u} :=  OAI.Thomason.streetNerveFinite n ⋙ (SSet.ex ⋙ SSet.ex)end OAI.Thomasonendsectionnamespace OAI.Thomason.OmegaCategoryopen CategoryTheorynoncomputable def nCategoryInclusion (n : ℕ) : OAI.Thomason.OmegaCategory.NCategory.{u} n ⥤ OAI.Thomason.OmegaCategory.{u} where  obj C := C.val  map F := Fnoncomputable def truncationHomEquiv (n : ℕ) (C : OAI.Thomason.OmegaCategory.{u}) (D : OAI.Thomason.OmegaCategory.NCategory.{u} n) :    ((OAI.Thomason.OmegaCategory.truncationFunctor n).obj C ⟶ D) ≃ (C ⟶ (OAI.Thomason.OmegaCategory.nCategoryInclusion n).obj D) := by  classical  have proof_mk_comp_101 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (k : ℕ) (x y : P.ValidTerm)      (h : P.Equiv (.target k x.val) (.source k y.val))      (h' : P.target k (Quotient.mk _ x) = P.source k (Quotient.mk _ y)) :      P.comp k (Quotient.mk _ x) (Quotient.mk _ y) h' =        Quotient.mk _ ⟨.comp k x.val y.val, OAI.Thomason.OmegaCategory.Presentation.Valid.comp (P := P) k x.val y.val x.property y.property h⟩ := by    change Quotient.mk _ (P.compTerm k x y) = _    simp only [OAI.Thomason.OmegaCategory.Presentation.compTerm, dite_eq_left h]  have proof_map_composable_102 {C : OAI.Thomason.OmegaCategory.{u}} {D : OAI.Thomason.OmegaCategory.{u}}  (F : OAI.Thomason.OmegaCategory.Functor C D) {k : ℕ} {x y : C.Cell}      (h : C.target k x = C.source k y) :      D.target k (F.map x) = D.source k (F.map y) := by    rw [← F.map_target, ← F.map_source, h]  have proof_functor_ext_100 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  {C : OAI.Thomason.OmegaCategory.{u}} {F G : OAI.Thomason.OmegaCategory.Functor P.category C}      (h : ∀ g, F.map (P.generator g) = G.map (P.generator g)) : F = G := by    apply OAI.Thomason.OmegaCategory.Functor.ext    funext x    induction x using Quotient.inductionOn with | h x =>      rcases x with ⟨x, hx⟩      induction hx with      | gen g => exact h g      | source k x hx ih =>        change F.map (P.category.source k (Quotient.mk _ ⟨x, hx⟩)) =          G.map (P.category.source k (Quotient.mk _ ⟨x, hx⟩))        rw [F.map_source, G.map_source, ih]      | target k x hx ih =>        change F.map (P.category.target k (Quotient.mk _ ⟨x, hx⟩)) =          G.map (P.category.target k (Quotient.mk _ ⟨x, hx⟩))        rw [F.map_target, G.map_target, ih]      | comp k x y hx hy hm ihx ihy =>        have hc : P.category.target k (Quotient.mk _ ⟨x, hx⟩) =            P.category.source k (Quotient.mk _ ⟨y, hy⟩) := Quotient.sound hm        rw [← (proof_mk_comp_101 P k ⟨x, hx⟩ ⟨y, hy⟩ hm hc)]        change F.map (P.category.comp k _ _ hc) = G.map (P.category.comp k _ _ hc)        rw [F.map_comp k _ _ hc (proof_map_composable_102 F hc), G.map_comp k _ _ hc (proof_map_composable_102 G hc)]        congr 1  have proof_truncation_functor_ext_104  {n : ℕ} {C D : OAI.Thomason.OmegaCategory.{u}}      {F G : OAI.Thomason.OmegaCategory.Functor (OAI.Thomason.OmegaCategory.truncation n C).val D}      (h : OAI.Thomason.OmegaCategory.Functor.comp (OAI.Thomason.OmegaCategory.truncationUnit n C) F = OAI.Thomason.OmegaCategory.Functor.comp (OAI.Thomason.OmegaCategory.truncationUnit n C) G) : F = G := by    apply (proof_functor_ext_100 (OAI.Thomason.OmegaCategory.truncationPresentation n C))    intro x    exact congrArg (fun H : OAI.Thomason.OmegaCategory.Functor C D => H.map x) h  exact {    toFun F := OAI.Thomason.OmegaCategory.Functor.comp (OAI.Thomason.OmegaCategory.truncationUnit n C) F    invFun := OAI.Thomason.OmegaCategory.truncationLift D    left_inv F := by      apply proof_truncation_functor_ext_104      rfl    right_inv _ := rfl  }noncomputable def truncationAdjunction (n : ℕ) : OAI.Thomason.OmegaCategory.truncationFunctor.{u} n ⊣ OAI.Thomason.OmegaCategory.nCategoryInclusion n := by  classical  have proof_mk_comp_101 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  (k : ℕ) (x y : P.ValidTerm)      (h : P.Equiv (.target k x.val) (.source k y.val))      (h' : P.target k (Quotient.mk _ x) = P.source k (Quotient.mk _ y)) :      P.comp k (Quotient.mk _ x) (Quotient.mk _ y) h' =        Quotient.mk _ ⟨.comp k x.val y.val, OAI.Thomason.OmegaCategory.Presentation.Valid.comp (P := P) k x.val y.val x.property y.property h⟩ := by    change Quotient.mk _ (P.compTerm k x y) = _    simp only [OAI.Thomason.OmegaCategory.Presentation.compTerm, dite_eq_left h]  have proof_map_composable_102 {C : OAI.Thomason.OmegaCategory.{u}} {D : OAI.Thomason.OmegaCategory.{u}}  (F : OAI.Thomason.OmegaCategory.Functor C D) {k : ℕ} {x y : C.Cell}      (h : C.target k x = C.source k y) :      D.target k (F.map x) = D.source k (F.map y) := by    rw [← F.map_target, ← F.map_source, h]  have proof_functor_ext_100 (P : OAI.Thomason.OmegaCategory.Presentation.{u})  {C : OAI.Thomason.OmegaCategory.{u}} {F G : OAI.Thomason.OmegaCategory.Functor P.category C}      (h : ∀ g, F.map (P.generator g) = G.map (P.generator g)) : F = G := by    apply OAI.Thomason.OmegaCategory.Functor.ext    funext x    induction x using Quotient.inductionOn with | h x =>      rcases x with ⟨x, hx⟩      induction hx with      | gen g => exact h g      | source k x hx ih =>        change F.map (P.category.source k (Quotient.mk _ ⟨x, hx⟩)) =          G.map (P.category.source k (Quotient.mk _ ⟨x, hx⟩))        rw [F.map_source, G.map_source, ih]      | target k x hx ih =>        change F.map (P.category.target k (Quotient.mk _ ⟨x, hx⟩)) =          G.map (P.category.target k (Quotient.mk _ ⟨x, hx⟩))        rw [F.map_target, G.map_target, ih]      | comp k x y hx hy hm ihx ihy =>        have hc : P.category.target k (Quotient.mk _ ⟨x, hx⟩) =            P.category.source k (Quotient.mk _ ⟨y, hy⟩) := Quotient.sound hm        rw [← (proof_mk_comp_101 P k ⟨x, hx⟩ ⟨y, hy⟩ hm hc)]        change F.map (P.category.comp k _ _ hc) = G.map (P.category.comp k _ _ hc)        rw [F.map_comp k _ _ hc (proof_map_composable_102 F hc), G.map_comp k _ _ hc (proof_map_composable_102 G hc)]        congr 1  have proof_truncation_functor_ext_104  {n : ℕ} {C D : OAI.Thomason.OmegaCategory.{u}}      {F G : OAI.Thomason.OmegaCategory.Functor (OAI.Thomason.OmegaCategory.truncation n C).val D}      (h : OAI.Thomason.OmegaCategory.Functor.comp (OAI.Thomason.OmegaCategory.truncationUnit n C) F = OAI.Thomason.OmegaCategory.Functor.comp (OAI.Thomason.OmegaCategory.truncationUnit n C) G) : F = G := by    apply (proof_functor_ext_100 (OAI.Thomason.OmegaCategory.truncationPresentation n C))    intro x    exact congrArg (fun H : OAI.Thomason.OmegaCategory.Functor C D => H.map x) h  exact    Adjunction.mkOfHomEquiv {        homEquiv := OAI.Thomason.OmegaCategory.truncationHomEquiv n        homEquiv_naturality_left_symm := by          intro C' C D F G          apply proof_truncation_functor_ext_104          rfl        homEquiv_naturality_right := by          intro C D D' F G          rfl }end OAI.Thomason.OmegaCategoryendsectionnamespace OAI.Thomasonopen CategoryTheory Oppositenoncomputable def categorificationFiniteAdjunction (n : ℕ) :    OAI.Thomason.categorificationFinite.{u} n ⊣ OAI.Thomason.streetNerveFinite.{u} n :=  OAI.Thomason.categorificationAdjunction.comp (OAI.Thomason.OmegaCategory.truncationAdjunction n)end OAI.Thomasonendsectionnamespace OAI.Thomasonopen CategoryTheorynoncomputable def thomasonFiniteAdjunction (n : ℕ) :    OAI.Thomason.thomasonLeftFinite.{u} n ⊣ OAI.Thomason.thomasonRightFinite.{u} n :=  (SSet.sdExAdjunction.comp SSet.sdExAdjunction).comp (OAI.Thomason.categorificationFiniteAdjunction n)end OAI.Thomasonendsectionnamespace OAI.Thomason.WeakHomotopyopen scoped Topology Topology.Homotopyvariable {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y]noncomputable def loopMap (N : Type w) (f : C(X, Y)) (x : X) : GenLoop N X x → GenLoop N Y (f x) :=  fun p => ⟨f.comp p.val, fun y hy => congrArg f (p.property y hy)⟩noncomputable def groupMap (N : Type w) (f : C(X, Y)) (x : X) :    HomotopyGroup N X x → HomotopyGroup N Y (f x) := by  classical  have proof_loopMap_homotopic_105 {X : Type u} {Y : Type v} [instLocal2 : TopologicalSpace.{u} X] [instLocal3 : TopologicalSpace.{v} Y]  (N : Type w) (f : C(X, Y)) (x : X)      {p q : GenLoop N X x} (h : GenLoop.Homotopic p q) :      GenLoop.Homotopic (OAI.Thomason.WeakHomotopy.loopMap N f x p) (OAI.Thomason.WeakHomotopy.loopMap N f x q) :=    h.comp_continuousMap f  exact    Quotient.map (OAI.Thomason.WeakHomotopy.loopMap N f x) (fun _ _ h => proof_loopMap_homotopic_105 N f x h)noncomputable def componentsMap (f : C(X, Y)) : ZerothHomotopy X → ZerothHomotopy Y :=  ZerothHomotopy.lift (fun x => ZerothHomotopy.mk (f x))    (fun _ _ p => ZerothHomotopy.sound (p.map f.continuous))noncomputable def Equivalence (f : C(X, Y)) : Prop :=  Function.Bijective (OAI.Thomason.WeakHomotopy.componentsMap f) ∧    ∀ (n : ℕ) (x : X), Function.Bijective (OAI.Thomason.WeakHomotopy.groupMap (Fin (n+1)) f x)end OAI.Thomason.WeakHomotopyendsectionnamespace OAI.Thomasonopen CategoryTheorynoncomputable def simplicialWeakEquivalences : MorphismProperty SSet.{u} :=  fun _ _ f => OAI.Thomason.WeakHomotopy.Equivalence (SSet.toTop.map f).homnoncomputable def simplicialFibrations : MorphismProperty SSet.{u} := (SSet.modelCategoryQuillen.J).rlpend OAI.Thomasonendsectionnamespace OAI.Thomasonopen CategoryTheory Limits HomotopicalAlgebrastructure KanQuillenModel where  model : ModelCategory SSet.{u}  weak_eq : model.categoryWithWeakEquivalences.weakEquivalences = OAI.Thomason.simplicialWeakEquivalences  fib_eq : model.categoryWithFibrations.fibrations = OAI.Thomason.simplicialFibrations  cof_eq : model.categoryWithCofibrations.cofibrations = MorphismProperty.monomorphisms SSetnoncomputable def LeftProperFor {C : Type v} [Category.{u} C]    (W Cof : MorphismProperty C) : Prop :=  ∀ {A B X Y : C} (i : A ⟶ B) (f : A ⟶ X) (g : B ⟶ Y) (j : X ⟶ Y),    IsPushout i f g j → Cof i → W f → W gnoncomputable def RightProperFor {C : Type v} [Category.{u} C]    (W Fib : MorphismProperty C) : Prop :=  ∀ {A B X Y : C} (f : A ⟶ B) (g : A ⟶ X) (p : B ⟶ Y) (q : X ⟶ Y),    IsPullback f g p q → Fib q → W p → W gnoncomputable def FibrantFor {C : Type v} [Category.{u} C] (Fib : MorphismProperty C) (Y : C) : Prop :=  ∃ (T : C) (_ : IsTerminal T) (p : Y ⟶ T), Fib pnoncomputable def boundaryImages {C : Type v} [Category.{u} C] (L : SSet.{u} ⥤ C) : MorphismProperty C :=  .ofHoms (fun n : ℕ => L.map (SSet.boundary n).ι)noncomputable def hornImages {C : Type v} [Category.{u} C] (L : SSet.{u} ⥤ C) : MorphismProperty C :=  ⨆ n : ℕ, .ofHoms (fun i : Fin (n+2) => L.map (SSet.horn (n+1) i).ι)structure ExactModelEndpoint {C : Type v} [Category.{u} C]    (L : SSet.{u} ⥤ C) (R : C ⥤ SSet.{u}) (adj : L ⊣ R) where  model : ModelCategory C  weak_eq : model.categoryWithWeakEquivalences.weakEquivalences =    OAI.Thomason.simplicialWeakEquivalences.inverseImage R  fib_eq : model.categoryWithFibrations.fibrations = OAI.Thomason.simplicialFibrations.inverseImage R  cof_eq : model.categoryWithCofibrations.cofibrations =    ((OAI.Thomason.simplicialFibrations.inverseImage R) ⊓ (OAI.Thomason.simplicialWeakEquivalences.inverseImage R)).llp  generating_cofibrations : (OAI.Thomason.boundaryImages L).rlp =    model.categoryWithFibrations.fibrations ⊓ model.categoryWithWeakEquivalences.weakEquivalences  generating_trivial_cofibrations : (OAI.Thomason.hornImages L).rlp = model.categoryWithFibrations.fibrations  weak_factorization_one : MorphismProperty.IsWeakFactorizationSystem    (model.categoryWithCofibrations.cofibrations ⊓ model.categoryWithWeakEquivalences.weakEquivalences)    model.categoryWithFibrations.fibrations  weak_factorization_two : MorphismProperty.IsWeakFactorizationSystem    model.categoryWithCofibrations.cofibrations    (model.categoryWithFibrations.fibrations ⊓ model.categoryWithWeakEquivalences.weakEquivalences)  complete : HasLimitsOfSize.{u,u} C  cocomplete : HasColimitsOfSize.{u,u} C  locallyPresentable : IsLocallyPresentable.{u} C  leftProper : OAI.Thomason.LeftProperFor model.categoryWithWeakEquivalences.weakEquivalences    model.categoryWithCofibrations.cofibrations  rightProper : OAI.Thomason.RightProperFor model.categoryWithWeakEquivalences.weakEquivalences    model.categoryWithFibrations.fibrations  leftQuillen : ∀ {K K' : SSet.{u}} (f : K ⟶ K'), Mono f →    model.categoryWithCofibrations.cofibrations (L.map f) ∧      (OAI.Thomason.simplicialWeakEquivalences f → model.categoryWithWeakEquivalences.weakEquivalences (L.map f))  quillenEquivalence : ∀ (K : SSet.{u}) (Y : C),    OAI.Thomason.FibrantFor model.categoryWithFibrations.fibrations Y →    ∀ f : L.obj K ⟶ Y,      model.categoryWithWeakEquivalences.weakEquivalences f ↔        OAI.Thomason.simplicialWeakEquivalences (adj.homEquiv K Y f)noncomputable def FullMain : Prop :=  Nonempty OAI.Thomason.KanQuillenModel.{u} ∧  Nonempty (OAI.Thomason.ExactModelEndpoint OAI.Thomason.thomasonLeft.{u} OAI.Thomason.thomasonRight OAI.Thomason.thomasonAdjunction) ∧  ∀ n : ℕ, 1 ≤ n →    Nonempty (OAI.Thomason.ExactModelEndpoint (OAI.Thomason.thomasonLeftFinite.{u} n) (OAI.Thomason.thomasonRightFinite n)      (OAI.Thomason.thomasonFiniteAdjunction n))end OAI.Thomasonendsectionnamespace OAI.Thomasonopen CategoryTheorynoncomputable def thomasonWeakEquivalences : MorphismProperty OAI.Thomason.OmegaCategory.{u} :=  OAI.Thomason.simplicialWeakEquivalences.inverseImage OAI.Thomason.thomasonRightnoncomputable def thomasonWeakEquivalencesFinite (n : ℕ) :    MorphismProperty (OAI.Thomason.OmegaCategory.NCategory.{u} n) :=  OAI.Thomason.simplicialWeakEquivalences.inverseImage (OAI.Thomason.thomasonRightFinite n)end OAI.Thomasonendsectionnamespace OAItheorem Thomason.main : OAI.Thomason.FullMain.{u} := by  sorrytheorem Thomason.nerveDetection_allDimensions :    OAI.Thomason.thomasonWeakEquivalences.{u} =      OAI.Thomason.simplicialWeakEquivalences.inverseImage OAI.Thomason.streetNerveFunctor ∧    ∀ n : ℕ, OAI.Thomason.thomasonWeakEquivalencesFinite.{u} n =      OAI.Thomason.simplicialWeakEquivalences.inverseImage (OAI.Thomason.streetNerveFinite n) := by  sorryend OAIendend