ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>P : CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ)<GOAL>∀ {X Y : SimplexCategoryᵒᵖ} (θ : X ⟶ Y), (AlgebraicTopology.DoldKan.Γ₂.obj P).X.map θ = AlgebraicTopology.DoldKan.Γ₀.Obj.map P.X θ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>∀ {X Y : CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ)} (f : X ⟶ Y) (Δ : SimplexCategoryᵒᵖ), (AlgebraicTopology.DoldKan.Γ₂.map f).f.app Δ = (AlgebraicTopology.DoldKan.Γ₀.splitting X.X).desc Δ fun A => f.f.f (Opposite.unop A.fst).len ≫ ((AlgebraicTopology.DoldKan.Γ₀.splitting Y.X).cofan Δ).inj A
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<GOAL>AlgebraicTopology.DoldKan.HigherFacesVanish (n + 1) (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op [n + 1])).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op [n + 1])))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<GOAL>((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op [n])).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op [n])) ≫ AlgebraicTopology.DoldKan.PInfty.f n = ((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op [n])).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op [n]))
<VAR>α : Type u_1<VAR>a : Lists α<VAR>l : Lists' α true<GOAL>(Lists'.cons a l).toList = a :: l.toList
<VAR>α : Type u_1<VAR>l : List (Lists α)<GOAL>(Lists'.ofList l).toList = l
<VAR>α : Type u_1<VAR>l : Lists' α true<GOAL>Lists'.ofList l.toList = l
<VAR>α : Type u_1<VAR>b : Bool<VAR>a : Lists α<VAR>l : Lists' α b<GOAL>a ∈ l ↔ ∃ a' ∈ l.toList, a ~ a'
<VAR>α : Type u_1<VAR>a y : Lists α<VAR>l : Lists' α true<GOAL>a ∈ Lists'.cons y l ↔ a ~ y ∨ a ∈ l
<VAR>α : Type u_1<VAR>a : Lists α<VAR>l₁ l₂ : Lists' α true<GOAL>Lists'.cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List (Lists α)<VAR>h : l₁ ⊆ l₂<GOAL>Lists'.ofList l₁ ⊆ Lists'.ofList l₂
<VAR>α : Type u_1<VAR>l : Lists' α true<GOAL>l ⊆ Lists'.nil → l = Lists'.nil
<VAR>α : Type u_1<VAR>a : Lists α<VAR>l₁ l₂ : Lists' α true<GOAL>l₁ ⊆ l₂ → a ∈ l₁.toList → a ∈ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : Lists' α true<GOAL>l₁ ⊆ l₂ ↔ ∀ a ∈ l₁.toList, a ∈ l₂
<VAR>α : Type u_1<VAR>l : List (Lists α)<GOAL>(Lists.ofList l).IsList
<VAR>α : Type u_1<VAR>l : List (Lists α)<GOAL>(Lists.ofList l).toList = l
<VAR>α : Type u_1<VAR>l : Lists α<GOAL>l.IsList → Lists.ofList l.toList = l
<VAR>α : Type u_1<VAR>a l : Lists α<GOAL>a ∈ l → l.IsList
<VAR>α : Type u_1<VAR>l₁ l₂ : Lists' α true<GOAL>Lists.of' l₁ ~ Lists.of' l₂ ↔ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
<VAR>α : Type u_1<VAR>a : α<VAR>l : Lists α<GOAL>Lists.atom a ~ l ↔ Lists.atom a = l
<VAR>α : Type u_1<VAR>l₁ l₂ : Lists α<VAR>h : l₁ ~ l₂<GOAL>l₂ ~ l₁
<VAR>α : Type u_1<VAR>l₁ l₂ l₃ : Lists α<GOAL>l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
<VAR>α : Type u_1<VAR>l : Lists' α true<VAR>a a' : Lists α<GOAL>a ~ a' → (a ∈ l ↔ a' ∈ l)
<VAR>α : Type u_1<VAR>a : Lists α<VAR>l₁ l₂ : Lists' α true<VAR>s : l₁ ⊆ l₂<GOAL>a ∈ l₁ → a ∈ l₂
<VAR>α : Type u_1<VAR>l₁ l₂ l₃ : Lists' α true<VAR>h₁ : l₁ ⊆ l₂<VAR>h₂ : l₂ ⊆ l₃<GOAL>l₁ ⊆ l₃
<GOAL>Cardinal.lift.{v, u_1} Cardinal.continuum = Cardinal.continuum
<VAR>c : Cardinal.{u}<GOAL>Cardinal.continuum ≤ Cardinal.lift.{v, u} c ↔ Cardinal.continuum ≤ c
<VAR>c : Cardinal.{u}<GOAL>Cardinal.lift.{v, u} c ≤ Cardinal.continuum ↔ c ≤ Cardinal.continuum
<VAR>c : Cardinal.{u}<GOAL>Cardinal.continuum < Cardinal.lift.{v, u} c ↔ Cardinal.continuum < c
<VAR>c : Cardinal.{u}<GOAL>Cardinal.lift.{v, u} c < Cardinal.continuum ↔ c < Cardinal.continuum
<VAR>n : ℕ<GOAL>↑n < Cardinal.continuum
<VAR>n : ℕ<GOAL>↑n + Cardinal.continuum = Cardinal.continuum
<VAR>n : ℕ<GOAL>Cardinal.continuum + ↑n = Cardinal.continuum
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n + Cardinal.continuum = Cardinal.continuum
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Cardinal.continuum + OfNat.ofNat n = Cardinal.continuum
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>↑n * Cardinal.continuum = Cardinal.continuum
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Cardinal.continuum * ↑n = Cardinal.continuum
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n * Cardinal.continuum = Cardinal.continuum
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Cardinal.continuum * OfNat.ofNat n = Cardinal.continuum
<GOAL>Cardinal.aleph0 ^ Cardinal.aleph0 = Cardinal.continuum
<VAR>n : ℕ<VAR>hn : 2 ≤ n<GOAL>↑n ^ Cardinal.aleph0 = Cardinal.continuum
<GOAL>UnivLE.{u, v} ↔ Cardinal.univ.{u, v + 1} ≤ Cardinal.univ.{v, u + 1}
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject.Augmented C<VAR>self : SimplicialObject.Augmented.ExtraDegeneracy X<GOAL>self.s 0 ≫ X.left.δ 1 = X.hom.app (Opposite.op [0]) ≫ self.s'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject.Augmented C<VAR>self : SimplicialObject.Augmented.ExtraDegeneracy X<GOAL>self.s' ≫ X.hom.app (Opposite.op [0]) = 𝟙 (CategoryTheory.SimplicialObject.Augmented.point.obj X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject.Augmented C<VAR>self : SimplicialObject.Augmented.ExtraDegeneracy X<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>self.s n ≫ X.left.σ i.succ = X.left.σ i ≫ self.s (n + 1)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject.Augmented C<VAR>self : SimplicialObject.Augmented.ExtraDegeneracy X<VAR>n : ℕ<VAR>i : Fin (n + 2)<GOAL>self.s (n + 1) ≫ X.left.δ i.succ = X.left.δ i ≫ self.s n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject.Augmented C<VAR>self : SimplicialObject.Augmented.ExtraDegeneracy X<VAR>n : ℕ<GOAL>self.s n ≫ X.left.δ 0 = 𝟙 (CategoryTheory.SimplicialObject.Augmented.drop.obj X _[n])
<VAR>n : ℕ<VAR>X : Type u_1<VAR>Zero X<VAR>f : Fin n → X<GOAL>SSet.Augmented.StandardSimplex.shiftFun f 0 = 0
<VAR>n : ℕ<VAR>X : Type u_1<VAR>Zero X<VAR>f : Fin n → X<VAR>i : Fin n<GOAL>SSet.Augmented.StandardSimplex.shiftFun f i.succ = f i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>S : CategoryTheory.SplitEpi f.hom<VAR>n : ℕ<GOAL>CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s f S n ≫ CategoryTheory.Limits.WidePullback.π (fun x => f.hom) 0 = (CategoryTheory.Limits.WidePullback.base fun x => f.hom) ≫ S.section_
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>S : CategoryTheory.SplitEpi f.hom<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s f S n ≫ CategoryTheory.Limits.WidePullback.π (fun x => f.hom) i.succ = CategoryTheory.Limits.WidePullback.π (fun x => f.hom) i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>S : CategoryTheory.SplitEpi f.hom<VAR>n : ℕ<GOAL>(CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s f S n ≫ CategoryTheory.Limits.WidePullback.base fun x => f.hom) = CategoryTheory.Limits.WidePullback.base fun x => f.hom
<VAR>α : Type u<VAR>s : Set α<VAR>DivisionRing α<GOAL>Subfield.rangeOfWType s = ⊤
<VAR>α : Type u<VAR>s : Set α<VAR>DivisionRing α<GOAL>Function.Surjective (WType.elim (↥(Subfield.closure s)) (Subfield.operate s))
<VAR>α : Type u<VAR>s : Set α<VAR>DivisionRing α<GOAL>Cardinal.mk ↥(Subfield.closure s) ≤ max (Cardinal.mk ↑s) Cardinal.aleph0
<VAR>α : Type u<VAR>s : Set α<VAR>DivisionRing α<VAR>Infinite ↑s<GOAL>Cardinal.mk ↥(Subfield.closure s) = Cardinal.mk ↑s
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<GOAL>AlgebraicTopology.DoldKan.N₂ ⋙ (CategoryTheory.Idempotents.karoubiChainComplexEquivalence C ℕ).functor = CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙ AlgebraicTopology.DoldKan.N₁ ⋙ (CategoryTheory.Idempotents.karoubiChainComplexEquivalence (CategoryTheory.Idempotents.Karoubi C) ℕ).functor ⋙ (CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>q n : ℕ<VAR>hqn : n ≤ q<GOAL>(AlgebraicTopology.DoldKan.P (q + 1)).f n = (AlgebraicTopology.DoldKan.P q).f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>q n : ℕ<VAR>hqn : n ≤ q<GOAL>(AlgebraicTopology.DoldKan.Q (q + 1)).f n = (AlgebraicTopology.DoldKan.Q q).f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<GOAL>AlgebraicTopology.DoldKan.PInfty.f 0 = 𝟙 (K[X].X 0)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<GOAL>AlgebraicTopology.DoldKan.PInfty.f n = (AlgebraicTopology.DoldKan.P n).f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<GOAL>AlgebraicTopology.DoldKan.QInfty.f 0 = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<GOAL>AlgebraicTopology.DoldKan.QInfty.f n = (AlgebraicTopology.DoldKan.Q n).f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>n : ℕ<VAR>X Y : CategoryTheory.SimplicialObject C<VAR>f : X ⟶ Y<GOAL>f.app (Opposite.op [n]) ≫ AlgebraicTopology.DoldKan.PInfty.f n = AlgebraicTopology.DoldKan.PInfty.f n ≫ f.app (Opposite.op [n])
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>n : ℕ<VAR>X Y : CategoryTheory.SimplicialObject C<VAR>f : X ⟶ Y<GOAL>f.app (Opposite.op [n]) ≫ AlgebraicTopology.DoldKan.QInfty.f n = AlgebraicTopology.DoldKan.QInfty.f n ≫ f.app (Opposite.op [n])
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<GOAL>AlgebraicTopology.DoldKan.PInfty.f n ≫ AlgebraicTopology.DoldKan.PInfty.f n = AlgebraicTopology.DoldKan.PInfty.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<GOAL>AlgebraicTopology.DoldKan.PInfty ≫ AlgebraicTopology.DoldKan.PInfty = AlgebraicTopology.DoldKan.PInfty
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<GOAL>AlgebraicTopology.DoldKan.QInfty.f n ≫ AlgebraicTopology.DoldKan.QInfty.f n = AlgebraicTopology.DoldKan.QInfty.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<GOAL>AlgebraicTopology.DoldKan.QInfty ≫ AlgebraicTopology.DoldKan.QInfty = AlgebraicTopology.DoldKan.QInfty
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<GOAL>AlgebraicTopology.DoldKan.PInfty.f n ≫ AlgebraicTopology.DoldKan.QInfty.f n = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<GOAL>AlgebraicTopology.DoldKan.PInfty ≫ AlgebraicTopology.DoldKan.QInfty = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<GOAL>AlgebraicTopology.DoldKan.QInfty.f n ≫ AlgebraicTopology.DoldKan.PInfty.f n = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<GOAL>AlgebraicTopology.DoldKan.QInfty ≫ AlgebraicTopology.DoldKan.PInfty = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<GOAL>AlgebraicTopology.DoldKan.PInfty + AlgebraicTopology.DoldKan.QInfty = 𝟙 K[X]
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<GOAL>AlgebraicTopology.DoldKan.PInfty.f n + AlgebraicTopology.DoldKan.QInfty.f n = 𝟙 (K[X].X n)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<GOAL>∀ (x : CategoryTheory.SimplicialObject C), (AlgebraicTopology.DoldKan.natTransPInfty C).app x = AlgebraicTopology.DoldKan.PInfty
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>n : ℕ<VAR>X : CategoryTheory.SimplicialObject C<GOAL>(AlgebraicTopology.DoldKan.natTransPInfty_f C n).app X = AlgebraicTopology.DoldKan.PInfty.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive D<VAR>G : C ⥤ D<VAR>G.Additive<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<GOAL>AlgebraicTopology.DoldKan.PInfty.f n = G.map (AlgebraicTopology.DoldKan.PInfty.f n)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>Y : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)<VAR>n : ℕ<GOAL>(AlgebraicTopology.DoldKan.PInfty.f n).f = Y.p.app (Opposite.op [n]) ≫ AlgebraicTopology.DoldKan.PInfty.f n
<VAR>a b : SimplexCategory<GOAL>a.len = b.len → a = b
<VAR>n : ℕ<GOAL>(SimplexCategory.mk n).len = n
<VAR>n : SimplexCategory<GOAL>SimplexCategory.mk n.len = n
<VAR>a b : SimplexCategory<VAR>f g : a.Hom b<GOAL>f.toOrderHom = g.toOrderHom → f = g
<VAR>a b : SimplexCategory<VAR>f : a.Hom b<GOAL>SimplexCategory.Hom.mk f.toOrderHom = f
<VAR>a b : SimplexCategory<VAR>f : Fin (a.len + 1) →o Fin (b.len + 1)<GOAL>(SimplexCategory.Hom.mk f).toOrderHom = f
<VAR>a b : SimplexCategory<VAR>f : Fin (a.len + 1) →o Fin (b.len + 1)<VAR>i : Fin (a.len + 1)<GOAL>(SimplexCategory.Hom.mk f).toOrderHom i = f i
<VAR>a : SimplexCategory<GOAL>SimplexCategory.Hom.toOrderHom (𝟙 a) = OrderHom.id
<VAR>a b c : SimplexCategory<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>SimplexCategory.Hom.toOrderHom (f ≫ g) = (SimplexCategory.Hom.toOrderHom g).comp (SimplexCategory.Hom.toOrderHom f)
<VAR>a b : SimplexCategory<VAR>f g : a ⟶ b<GOAL>SimplexCategory.Hom.toOrderHom f = SimplexCategory.Hom.toOrderHom g → f = g
<GOAL>(SimplexCategory.mk 0).const (SimplexCategory.mk 0) 0 = 𝟙 (SimplexCategory.mk 0)
<VAR>x y : SimplexCategory<VAR>i : Fin (y.len + 1)<VAR>a : Fin (x.len + 1)<GOAL>(SimplexCategory.Hom.toOrderHom (x.const y i)) a = i
<VAR>x : SimplexCategory<VAR>y z : SimplexCategory<VAR>f : y ⟶ z<VAR>i : Fin (y.len + 1)<GOAL>x.const y i ≫ f = x.const z ((SimplexCategory.Hom.toOrderHom f) i)
<VAR>f : SimplexCategory.mk 0 ⟶ SimplexCategory.mk 0<GOAL>f = 𝟙 (SimplexCategory.mk 0)
<VAR>n : ℕ<VAR>i j : Fin (n + 2)<VAR>H : i ≤ j<GOAL>SimplexCategory.δ i ≫ SimplexCategory.δ j.succ = SimplexCategory.δ j ≫ SimplexCategory.δ i.castSucc
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 3)<VAR>H : i.castSucc < j<GOAL>SimplexCategory.δ i ≫ SimplexCategory.δ j = SimplexCategory.δ (j.pred ⋯) ≫ SimplexCategory.δ i.castSucc
<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : i ≤ j.castSucc<GOAL>SimplexCategory.δ (i.castLT ⋯) ≫ SimplexCategory.δ j.succ = SimplexCategory.δ j ≫ SimplexCategory.δ i
<VAR>n : ℕ<VAR>i : Fin (n + 2)<GOAL>SimplexCategory.δ i ≫ SimplexCategory.δ i.castSucc = SimplexCategory.δ i ≫ SimplexCategory.δ i.succ
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 3)<VAR>H : j = i.castSucc<GOAL>SimplexCategory.δ i ≫ SimplexCategory.δ j = SimplexCategory.δ i ≫ SimplexCategory.δ i.succ
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 1)<VAR>H : i ≤ j.castSucc<GOAL>SimplexCategory.δ i.castSucc ≫ SimplexCategory.σ j.succ = SimplexCategory.σ j ≫ SimplexCategory.δ i
<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>SimplexCategory.δ i.castSucc ≫ SimplexCategory.σ i = 𝟙 (SimplexCategory.mk n)
<VAR>n : ℕ<VAR>j : Fin (n + 2)<VAR>i : Fin (n + 1)<VAR>H : j = i.castSucc<GOAL>SimplexCategory.δ j ≫ SimplexCategory.σ i = 𝟙 (SimplexCategory.mk n)
<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>SimplexCategory.δ i.succ ≫ SimplexCategory.σ i = 𝟙 (SimplexCategory.mk n)
<VAR>n : ℕ<VAR>j : Fin (n + 2)<VAR>i : Fin (n + 1)<VAR>H : j = i.succ<GOAL>SimplexCategory.δ j ≫ SimplexCategory.σ i = 𝟙 (SimplexCategory.mk n)
<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 1)<VAR>H : j.castSucc < i<GOAL>SimplexCategory.δ i.succ ≫ SimplexCategory.σ j.castSucc = SimplexCategory.σ j ≫ SimplexCategory.δ i
<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : j.succ < i<GOAL>SimplexCategory.δ i ≫ SimplexCategory.σ j = SimplexCategory.σ (j.castLT ⋯) ≫ SimplexCategory.δ (i.pred ⋯)
<VAR>n : ℕ<VAR>i j : Fin (n + 1)<VAR>H : i ≤ j<GOAL>SimplexCategory.σ i.castSucc ≫ SimplexCategory.σ j = SimplexCategory.σ j.succ ≫ SimplexCategory.σ i
<VAR>m n : ℕ<VAR>f : SimplexCategory.mk m ⟶ SimplexCategory.mk (n + 1)<VAR>j : Fin (n + 2)<VAR>hj : ∀ (k : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f) k ≠ j<GOAL>SimplexCategory.factor_δ f j ≫ SimplexCategory.δ j = f
<VAR>a : SimplexCategory<GOAL>SimplexCategory.skeletalFunctor.obj a = NonemptyFinLinOrd.of (Fin (a.len + 1))
<GOAL>∀ {X Y : SimplexCategory} (f : X ⟶ Y), SimplexCategory.skeletalFunctor.map f = SimplexCategory.Hom.toOrderHom f
<VAR>Δ₁ Δ₂ : SimplexCategory<VAR>f : Δ₁ ⟶ Δ₂<GOAL>SimplexCategory.skeletalFunctor.map f = SimplexCategory.Hom.toOrderHom f
<GOAL>CategoryTheory.IsSkeletonOf NonemptyFinLinOrd SimplexCategory SimplexCategory.skeletalFunctor
<VAR>n m : SimplexCategory<VAR>f : n ⟶ m<GOAL>CategoryTheory.Mono f ↔ Function.Injective ⇑(SimplexCategory.Hom.toOrderHom f)
<VAR>n m : SimplexCategory<VAR>f : n ⟶ m<GOAL>CategoryTheory.Epi f ↔ Function.Surjective ⇑(SimplexCategory.Hom.toOrderHom f)
<VAR>x y : SimplexCategory<VAR>f : x ⟶ y<GOAL>CategoryTheory.Mono f → x.len ≤ y.len
<VAR>n m : ℕ<VAR>f : SimplexCategory.mk n ⟶ SimplexCategory.mk m<GOAL>CategoryTheory.Mono f → n ≤ m
<VAR>x y : SimplexCategory<VAR>f : x ⟶ y<GOAL>CategoryTheory.Epi f → y.len ≤ x.len
<VAR>n m : ℕ<VAR>f : SimplexCategory.mk n ⟶ SimplexCategory.mk m<GOAL>CategoryTheory.Epi f → m ≤ n
<VAR>x y : SimplexCategory<VAR>f : x ⟶ y<VAR>hf : Function.Bijective (SimplexCategory.Hom.toOrderHom f).toFun<GOAL>CategoryTheory.IsIso f
<VAR>x : SimplexCategory<VAR>e : x ≅ x<GOAL>e = CategoryTheory.Iso.refl x
<VAR>x : SimplexCategory<VAR>f : x ⟶ x<VAR>CategoryTheory.IsIso f<GOAL>f = 𝟙 x
<VAR>n : ℕ<VAR>Δ' : SimplexCategory<VAR>θ : SimplexCategory.mk (n + 1) ⟶ Δ'<VAR>i : Fin (n + 1)<VAR>hi : (SimplexCategory.Hom.toOrderHom θ) i.castSucc = (SimplexCategory.Hom.toOrderHom θ) i.succ<GOAL>∃ θ', θ = SimplexCategory.σ i ≫ θ'
<VAR>n : ℕ<VAR>Δ' : SimplexCategory<VAR>θ : SimplexCategory.mk (n + 1) ⟶ Δ'<VAR>hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)<GOAL>∃ i θ', θ = SimplexCategory.σ i ≫ θ'
<VAR>n : ℕ<VAR>Δ : SimplexCategory<VAR>θ : Δ ⟶ SimplexCategory.mk (n + 1)<VAR>i : Fin (n + 2)<VAR>hi : ∀ (x : Fin (Δ.len + 1)), (SimplexCategory.Hom.toOrderHom θ) x ≠ i<GOAL>∃ θ', θ = θ' ≫ SimplexCategory.δ i
<VAR>n : ℕ<VAR>Δ : SimplexCategory<VAR>θ : Δ ⟶ SimplexCategory.mk (n + 1)<VAR>hθ : ¬Function.Surjective ⇑(SimplexCategory.Hom.toOrderHom θ)<GOAL>∃ i θ', θ = θ' ≫ SimplexCategory.δ i
<VAR>x : SimplexCategory<VAR>i : x ⟶ x<VAR>CategoryTheory.Mono i<GOAL>i = 𝟙 x
<VAR>x : SimplexCategory<VAR>i : x ⟶ x<VAR>CategoryTheory.Epi i<GOAL>i = 𝟙 x
<VAR>n : ℕ<VAR>θ : SimplexCategory.mk (n + 1) ⟶ SimplexCategory.mk n<VAR>CategoryTheory.Epi θ<GOAL>∃ i, θ = SimplexCategory.σ i
<VAR>n : ℕ<VAR>θ : SimplexCategory.mk n ⟶ SimplexCategory.mk (n + 1)<VAR>CategoryTheory.Mono θ<GOAL>∃ i, θ = SimplexCategory.δ i
<VAR>Δ' Δ : SimplexCategory<VAR>i : Δ' ⟶ Δ<VAR>hi : CategoryTheory.Mono i<VAR>hi' : Δ ≠ Δ'<GOAL>Δ'.len < Δ.len
<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>φ : Δ ⟶ Δ''<VAR>e : Δ ⟶ Δ'<VAR>CategoryTheory.Epi e<VAR>i : Δ' ⟶ Δ''<VAR>CategoryTheory.Mono i<VAR>fac : e ≫ i = φ<GOAL>CategoryTheory.Limits.image φ = Δ'
<VAR>Δ Δ'' : SimplexCategory<VAR>φ : Δ ⟶ Δ''<VAR>e : Δ ⟶ CategoryTheory.Limits.image φ<VAR>CategoryTheory.Epi e<VAR>i : CategoryTheory.Limits.image φ ⟶ Δ''<VAR>CategoryTheory.Mono i<VAR>fac : e ≫ i = φ<GOAL>CategoryTheory.Limits.image.ι φ = i
<VAR>Δ Δ'' : SimplexCategory<VAR>φ : Δ ⟶ Δ''<VAR>e : Δ ⟶ CategoryTheory.Limits.image φ<VAR>CategoryTheory.Epi e<VAR>i : CategoryTheory.Limits.image φ ⟶ Δ''<VAR>CategoryTheory.Mono i<VAR>fac : e ≫ i = φ<GOAL>CategoryTheory.Limits.factorThruImage φ = e
<VAR>X : SimplexCategory<GOAL>SimplexCategory.toCat.obj X = CategoryTheory.Cat.of ↑((CategoryTheory.forget₂ PartOrd Preord).obj ((CategoryTheory.forget₂ Lat PartOrd).obj ((CategoryTheory.forget₂ LinOrd Lat).obj ((CategoryTheory.forget₂ NonemptyFinLinOrd LinOrd).obj (NonemptyFinLinOrd.of (Fin (X.len + 1)))))))
<GOAL>∀ {X Y : SimplexCategory} (f : X ⟶ Y), SimplexCategory.toCat.map f = ⋯.functor
<VAR>α ι : Type u<VAR>a : Cardinal.{u}<VAR>Countable ι<VAR>f : ι → Set α<VAR>l : Filter ι<VAR>l.NeBot<VAR>t : Set α<VAR>ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i<VAR>h'f : ∀ (i : ι), #↑(f i) ≤ a<GOAL>#↑t ≤ a
<VAR>α : Type u<VAR>ι : Type v<VAR>a : Cardinal.{u}<VAR>Countable ι<VAR>f : ι → Set α<VAR>l : Filter ι<VAR>l.NeBot<VAR>t : Set α<VAR>ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i<VAR>h'f : ∀ (i : ι), #↑(f i) ≤ a<GOAL>#↑t ≤ a
<VAR>α : Type u<VAR>ι : Type v<VAR>a : Cardinal.{u}<VAR>Countable ι<VAR>f : ι → Set α<VAR>l : Filter ι<VAR>l.NeBot<VAR>ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i<VAR>h'f : ∀ (i : ι), #↑(f i) ≤ a<GOAL>#α ≤ a
<VAR>α : Type u<VAR>ι : Type v<VAR>a : Cardinal.{u}<VAR>Countable ι<VAR>f : ι → Set α<VAR>l : Filter ι<VAR>l.NeBot<VAR>ht : ∀ (x : α), ∀ᶠ (i : ι) in l, x ∈ f i<VAR>h'f : ∀ (i : ι), #↑(f i) = a<GOAL>#α = a
<VAR>c : Cardinal.{u_1}<GOAL>↑(Cardinal.toENat c) = Cardinal.toPartENat c
<VAR>n : ℕ<GOAL>Cardinal.toPartENat ↑n = ↑n
<VAR>c : Cardinal.{u_1}<VAR>h : c < Cardinal.aleph0<GOAL>Cardinal.toPartENat c = ↑(Cardinal.toNat c)
<VAR>c : Cardinal.{u_1}<GOAL>Cardinal.toPartENat c = ⊤ ↔ Cardinal.aleph0 ≤ c
<VAR>c : Cardinal.{u_1}<VAR>h : Cardinal.aleph0 ≤ c<GOAL>Cardinal.toPartENat c = ⊤
<VAR>α : Type u<VAR>h : Infinite α<GOAL>Cardinal.toPartENat (Cardinal.mk α) = ⊤
<GOAL>Cardinal.toPartENat Cardinal.aleph0 = ⊤
<GOAL>StrictMonoOn (⇑Cardinal.toPartENat) (Set.Iic Cardinal.aleph0)
<VAR>c c' : Cardinal.{u_1}<VAR>h : c ≤ Cardinal.aleph0<GOAL>Cardinal.toPartENat c ≤ Cardinal.toPartENat c' ↔ c ≤ c'
<VAR>c c' : Cardinal.{u_1}<VAR>hc' : c' < Cardinal.aleph0<GOAL>Cardinal.toPartENat c ≤ Cardinal.toPartENat c' ↔ c ≤ c'
<VAR>c c' : Cardinal.{u_1}<VAR>hc : c ≤ Cardinal.aleph0<VAR>hc' : c' ≤ Cardinal.aleph0<GOAL>Cardinal.toPartENat c = Cardinal.toPartENat c' ↔ c = c'
<VAR>c c' : Cardinal.{u_1}<VAR>h : c ≤ c'<GOAL>Cardinal.toPartENat c ≤ Cardinal.toPartENat c'
<VAR>c : Cardinal.{v}<GOAL>Cardinal.toPartENat (Cardinal.lift.{u, v} c) = Cardinal.toPartENat c
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<GOAL>Cardinal.toPartENat (Cardinal.mk α) = Cardinal.toPartENat (Cardinal.mk β)
<VAR>α : Type u<VAR>Fintype α<GOAL>Cardinal.toPartENat (Cardinal.mk α) = ↑(Fintype.card α)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.SimplicialCategory C<VAR>K : C<GOAL>(CategoryTheory.SimplicialCategory.homEquiv K K) (𝟙 K) = CategoryTheory.eId SSet K
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.SimplicialCategory C<VAR>K L M : C<VAR>f : K ⟶ L<VAR>g : L ⟶ M<GOAL>(CategoryTheory.SimplicialCategory.homEquiv K M) (f ≫ g) = (λ_ (𝟙_ SSet)).inv ≫ ((CategoryTheory.SimplicialCategory.homEquiv K L) f ⊗ (CategoryTheory.SimplicialCategory.homEquiv L M) g) ≫ CategoryTheory.eComp SSet K L M
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.SimplicialCategory C<VAR>K L : C<GOAL>CategoryTheory.SimplicialCategory.sHomWhiskerRight (𝟙 K) L = 𝟙 (CategoryTheory.SimplicialCategory.sHom K L)