ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<GOAL>∀ {X Y : C ⥤ D} (η : X ⟶ Y) (A : CategoryTheory.SimplicialObject.Augmented C), (((CategoryTheory.SimplicialObject.Augmented.whiskering C D).map η).app A).right = η.app (CategoryTheory.SimplicialObject.Augmented.point.obj A)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>X₀ : C<VAR>f : X.obj (Opposite.op (SimplexCategory.mk 0)) ⟶ X₀<VAR>w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f<VAR>i : SimplexCategoryᵒᵖ<GOAL>(X.augment X₀ f w).hom.app i = X.map ((SimplexCategory.mk 0).const (Opposite.unop i) 0).op ≫ f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>X₀ : C<VAR>f : X.obj (Opposite.op (SimplexCategory.mk 0)) ⟶ X₀<VAR>w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f<GOAL>(X.augment X₀ f w).left = X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>X₀ : C<VAR>f : X.obj (Opposite.op (SimplexCategory.mk 0)) ⟶ X₀<VAR>w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f<GOAL>(X.augment X₀ f w).right = X₀
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>X₀ : C<VAR>f : X.obj (Opposite.op (SimplexCategory.mk 0)) ⟶ X₀<VAR>w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f<GOAL>(X.augment X₀ f w).hom.app (Opposite.op (SimplexCategory.mk 0)) = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : SimplexCategory ⥤ C<VAR>X : SimplexCategory<GOAL>(𝟙 F).app X = 𝟙 (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y Z : SimplexCategory ⥤ C} (α : X ⟶ Y) (β : Y ⟶ Z) (X_1 : SimplexCategory), (α ≫ β).app X_1 = α.app X_1 ≫ β.app X_1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : CategoryTheory.CosimplicialObject C<VAR>f g : X ⟶ Y<VAR>h : ∀ (n : SimplexCategory), f.app n = g.app n<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>n : ℕ<VAR>h : n = n<GOAL>X.eqToIso h = CategoryTheory.Iso.refl (X.obj (SimplexCategory.mk n))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>n : ℕ<VAR>i j : Fin (n + 2)<VAR>H : i ≤ j<GOAL>X.δ i ≫ X.δ j.succ = X.δ j ≫ X.δ i.castSucc
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 3)<VAR>H : i.castSucc < j<GOAL>X.δ i ≫ X.δ j = X.δ (j.pred ⋯) ≫ X.δ i.castSucc
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : i ≤ j.castSucc<GOAL>X.δ (i.castLT ⋯) ≫ X.δ j.succ = X.δ j ≫ X.δ i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<GOAL>X.δ i ≫ X.δ i.castSucc = X.δ i ≫ X.δ i.succ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 3)<VAR>H : j = i.castSucc<GOAL>X.δ i ≫ X.δ j = X.δ i ≫ X.δ i.succ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 1)<VAR>H : i ≤ j.castSucc<GOAL>X.δ i.castSucc ≫ X.σ j.succ = X.σ j ≫ X.δ i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>X.δ i.castSucc ≫ X.σ i = 𝟙 (X.obj (SimplexCategory.mk n))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>n : ℕ<VAR>j : Fin (n + 2)<VAR>i : Fin (n + 1)<VAR>H : j = i.castSucc<GOAL>X.δ j ≫ X.σ i = 𝟙 (X.obj (SimplexCategory.mk n))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>X.δ i.succ ≫ X.σ i = 𝟙 (X.obj (SimplexCategory.mk n))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>n : ℕ<VAR>j : Fin (n + 2)<VAR>i : Fin (n + 1)<VAR>H : j = i.succ<GOAL>X.δ j ≫ X.σ i = 𝟙 (X.obj (SimplexCategory.mk n))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 1)<VAR>H : j.castSucc < i<GOAL>X.δ i.succ ≫ X.σ j.castSucc = X.σ j ≫ X.δ i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 3)<VAR>j : Fin (n + 2)<VAR>H : j.succ < i<GOAL>X.δ i ≫ X.σ j = X.σ (j.castLT ⋯) ≫ X.δ (i.pred ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>n : ℕ<VAR>i j : Fin (n + 1)<VAR>H : i ≤ j<GOAL>X.σ i.castSucc ≫ X.σ j = X.σ j.succ ≫ X.σ i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X' X : CategoryTheory.CosimplicialObject C<VAR>f : X ⟶ X'<VAR>n : ℕ<VAR>i : Fin (n + 2)<GOAL>X.δ i ≫ f.app (SimplexCategory.mk (n + 1)) = f.app (SimplexCategory.mk n) ≫ X'.δ i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X' X : CategoryTheory.CosimplicialObject C<VAR>f : X ⟶ X'<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>X.σ i ≫ f.app (SimplexCategory.mk n) = f.app (SimplexCategory.mk (n + 1)) ≫ X'.σ i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<GOAL>∀ {X Y : C ⥤ D} (τ : X ⟶ Y) (F : SimplexCategory ⥤ C) (c : SimplexCategory), (((CategoryTheory.CosimplicialObject.whiskering C D).map τ).app F).app c = τ.app (F.obj c)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>H : C ⥤ D<VAR>F : SimplexCategory ⥤ C<GOAL>∀ {X Y : SimplexCategory} (f : X ⟶ Y), (((CategoryTheory.CosimplicialObject.whiskering C D).obj H).obj F).map f = H.map (F.map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>H : C ⥤ D<VAR>F : SimplexCategory ⥤ C<VAR>X : SimplexCategory<GOAL>(((CategoryTheory.CosimplicialObject.whiskering C D).obj H).obj F).obj X = H.obj (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>H : C ⥤ D<GOAL>∀ {X Y : SimplexCategory ⥤ C} (α : X ⟶ Y) (X_1 : SimplexCategory), (((CategoryTheory.CosimplicialObject.whiskering C D).obj H).map α).app X_1 = H.map (α.app X_1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>n : ℕ<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>H : C ⥤ D<GOAL>∀ {X Y : SimplexCategory.Truncated n ⥤ C} (α : X ⟶ Y) (X_1 : SimplexCategory.Truncated n), (((CategoryTheory.CosimplicialObject.Truncated.whiskering C D).obj H).map α).app X_1 = H.map (α.app X_1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>n : ℕ<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>H : C ⥤ D<VAR>F : SimplexCategory.Truncated n ⥤ C<GOAL>∀ {X Y : SimplexCategory.Truncated n} (f : X ⟶ Y), (((CategoryTheory.CosimplicialObject.Truncated.whiskering C D).obj H).obj F).map f = H.map (F.map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>n : ℕ<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<GOAL>∀ {X Y : C ⥤ D} (τ : X ⟶ Y) (F : SimplexCategory.Truncated n ⥤ C) (c : SimplexCategory.Truncated n), (((CategoryTheory.CosimplicialObject.Truncated.whiskering C D).map τ).app F).app c = τ.app (F.obj c)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>n : ℕ<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>H : C ⥤ D<VAR>F : SimplexCategory.Truncated n ⥤ C<VAR>X : SimplexCategory.Truncated n<GOAL>(((CategoryTheory.CosimplicialObject.Truncated.whiskering C D).obj H).obj F).obj X = H.obj (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C) (𝟭 (CategoryTheory.CosimplicialObject C))<GOAL>(𝟙 X).left = 𝟙 X.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y Z : CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C) (𝟭 (CategoryTheory.CosimplicialObject C))} (f : X ⟶ Y) (g : Y ⟶ Z), (f ≫ g).left = f.left ≫ g.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y Z : CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C) (𝟭 (CategoryTheory.CosimplicialObject C))} (f : X ⟶ Y) (g : Y ⟶ Z) (X_1 : SimplexCategory), (f ≫ g).right.app X_1 = f.right.app X_1 ≫ g.right.app X_1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C) (𝟭 (CategoryTheory.CosimplicialObject C))<GOAL>∀ (X_1 : SimplexCategory), (𝟙 X).right.app X_1 = 𝟙 (X.right.obj X_1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : CategoryTheory.CosimplicialObject.Augmented C<VAR>f g : X ⟶ Y<VAR>h₁ : f.left = g.left<VAR>h₂ : f.right = g.right<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C) (𝟭 (CategoryTheory.CosimplicialObject C))} (f : X ⟶ Y), CategoryTheory.CosimplicialObject.Augmented.drop.map f = f.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C) (𝟭 (CategoryTheory.CosimplicialObject C))<GOAL>CategoryTheory.CosimplicialObject.Augmented.drop.obj X = X.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C) (𝟭 (CategoryTheory.CosimplicialObject C))<GOAL>CategoryTheory.CosimplicialObject.Augmented.point.obj X = X.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C) (𝟭 (CategoryTheory.CosimplicialObject C))} (f : X ⟶ Y), CategoryTheory.CosimplicialObject.Augmented.point.map f = f.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject.Augmented C<GOAL>(CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X).right = X.right.obj (SimplexCategory.mk 0)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.CosimplicialObject.Augmented C} (η : X ⟶ Y), (CategoryTheory.CosimplicialObject.Augmented.toArrow.map η).right = η.right.app (SimplexCategory.mk 0)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject.Augmented C<GOAL>(CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X).left = X.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.CosimplicialObject.Augmented C} (η : X ⟶ Y), (CategoryTheory.CosimplicialObject.Augmented.toArrow.map η).left = η.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject.Augmented C<GOAL>(CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X).hom = X.hom.app (SimplexCategory.mk 0)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<GOAL>∀ {X Y : C ⥤ D} (η : X ⟶ Y) (A : CategoryTheory.CosimplicialObject.Augmented C), (((CategoryTheory.CosimplicialObject.Augmented.whiskering C D).map η).app A).right = CategoryTheory.whiskerLeft (CategoryTheory.CosimplicialObject.Augmented.drop.obj A) η
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>F : C ⥤ D<GOAL>(CategoryTheory.CosimplicialObject.Augmented.whiskering C D).obj F = CategoryTheory.CosimplicialObject.Augmented.whiskeringObj C D F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<GOAL>∀ {X Y : C ⥤ D} (η : X ⟶ Y) (A : CategoryTheory.CosimplicialObject.Augmented C), (((CategoryTheory.CosimplicialObject.Augmented.whiskering C D).map η).app A).left = η.app (CategoryTheory.CosimplicialObject.Augmented.point.obj A)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>X₀ : C<VAR>f : X₀ ⟶ X.obj (SimplexCategory.mk 0)<VAR>w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂<GOAL>(X.augment X₀ f w).right = X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>X₀ : C<VAR>f : X₀ ⟶ X.obj (SimplexCategory.mk 0)<VAR>w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂<GOAL>(X.augment X₀ f w).left = X₀
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>X₀ : C<VAR>f : X₀ ⟶ X.obj (SimplexCategory.mk 0)<VAR>w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂<VAR>i : SimplexCategory<GOAL>(X.augment X₀ f w).hom.app i = f ≫ X.map ((SimplexCategory.mk 0).const i 0)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject C<VAR>X₀ : C<VAR>f : X₀ ⟶ X.obj (SimplexCategory.mk 0)<VAR>w : ∀ (i : SimplexCategory) (g₁ g₂ : SimplexCategory.mk 0 ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂<GOAL>(X.augment X₀ f w).hom.app (SimplexCategory.mk 0) = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : (SimplexCategoryᵒᵖ ⥤ C)ᵒᵖ<GOAL>(CategoryTheory.simplicialCosimplicialEquiv C).unitIso.inv.app X = (Opposite.unop X).rightOpLeftOpIso.inv.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : (SimplexCategoryᵒᵖ ⥤ C)ᵒᵖ<VAR>X : SimplexCategory<GOAL>((CategoryTheory.simplicialCosimplicialEquiv C).functor.obj F).obj X = Opposite.op ((Opposite.unop F).obj (Opposite.op X))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : SimplexCategory ⥤ Cᵒᵖ<GOAL>∀ (X_1 : SimplexCategory), ((CategoryTheory.simplicialCosimplicialEquiv C).counitIso.hom.app X).app X_1 = 𝟙 (X.obj X_1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : SimplexCategory ⥤ Cᵒᵖ<GOAL>(CategoryTheory.simplicialCosimplicialEquiv C).inverse.obj F = Opposite.op F.leftOp
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : SimplexCategory ⥤ Cᵒᵖ} (η : X ⟶ Y), (CategoryTheory.simplicialCosimplicialEquiv C).inverse.map η = (CategoryTheory.NatTrans.leftOp η).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : (SimplexCategoryᵒᵖ ⥤ C)ᵒᵖ<GOAL>(CategoryTheory.simplicialCosimplicialEquiv C).unitIso.hom.app X = (Opposite.unop X).rightOpLeftOpIso.hom.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : (SimplexCategoryᵒᵖ ⥤ C)ᵒᵖ<GOAL>∀ {X Y : SimplexCategory} (f : X ⟶ Y), ((CategoryTheory.simplicialCosimplicialEquiv C).functor.obj F).map f = ((Opposite.unop F).map f.op).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : SimplexCategory ⥤ Cᵒᵖ<GOAL>∀ (X_1 : SimplexCategory), ((CategoryTheory.simplicialCosimplicialEquiv C).counitIso.inv.app X).app X_1 = 𝟙 (X.obj X_1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : (SimplexCategoryᵒᵖ ⥤ C)ᵒᵖ} (η : X ⟶ Y) (X_1 : SimplexCategory), ((CategoryTheory.simplicialCosimplicialEquiv C).functor.map η).app X_1 = (η.unop.app (Opposite.op X_1)).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : (SimplexCategory ⥤ C)ᵒᵖ<GOAL>(CategoryTheory.cosimplicialSimplicialEquiv C).unitIso.inv.app X = (Opposite.unop X).opUnopIso.inv.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : SimplexCategoryᵒᵖ ⥤ Cᵒᵖ<GOAL>∀ (X_1 : SimplexCategoryᵒᵖ), ((CategoryTheory.cosimplicialSimplicialEquiv C).counitIso.hom.app X).app X_1 = 𝟙 (X.obj X_1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : (SimplexCategory ⥤ C)ᵒᵖ<VAR>X : SimplexCategoryᵒᵖ<GOAL>((CategoryTheory.cosimplicialSimplicialEquiv C).functor.obj F).obj X = Opposite.op ((Opposite.unop F).obj (Opposite.unop X))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : (SimplexCategory ⥤ C)ᵒᵖ} (α : X ⟶ Y) (X_1 : SimplexCategoryᵒᵖ), ((CategoryTheory.cosimplicialSimplicialEquiv C).functor.map α).app X_1 = (α.unop.app (Opposite.unop X_1)).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : SimplexCategoryᵒᵖ ⥤ Cᵒᵖ} (α : X ⟶ Y), (CategoryTheory.cosimplicialSimplicialEquiv C).inverse.map α = Quiver.Hom.op { app := fun X_1 => (α.app (Opposite.op X_1)).unop, naturality := ⋯ }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : (SimplexCategory ⥤ C)ᵒᵖ<GOAL>∀ {X Y : SimplexCategoryᵒᵖ} (f : X ⟶ Y), ((CategoryTheory.cosimplicialSimplicialEquiv C).functor.obj F).map f = ((Opposite.unop F).map f.unop).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : SimplexCategoryᵒᵖ ⥤ Cᵒᵖ<GOAL>(CategoryTheory.cosimplicialSimplicialEquiv C).inverse.obj F = Opposite.op F.unop
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : (SimplexCategory ⥤ C)ᵒᵖ<GOAL>(CategoryTheory.cosimplicialSimplicialEquiv C).unitIso.hom.app X = (Opposite.unop X).opUnopIso.hom.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : SimplexCategoryᵒᵖ ⥤ Cᵒᵖ<GOAL>∀ (X_1 : SimplexCategoryᵒᵖ), ((CategoryTheory.cosimplicialSimplicialEquiv C).counitIso.inv.app X).app X_1 = 𝟙 (X.obj X_1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject.Augmented C<GOAL>∀ {X_1 Y : SimplexCategory} (f : X_1 ⟶ Y), X.rightOp.right.map f = (X.left.map f.op).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject.Augmented C<GOAL>X.rightOp.left = Opposite.op X.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject.Augmented C<GOAL>∀ (X_1 : SimplexCategory), X.rightOp.hom.app X_1 = (X.hom.app (Opposite.op X_1)).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject.Augmented C<GOAL>∀ (X_1 : SimplexCategory), X.rightOp.right.obj X_1 = Opposite.op (X.left.obj (Opposite.op X_1))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ<GOAL>∀ {X_1 Y : SimplexCategoryᵒᵖ} (f : X_1 ⟶ Y), X.leftOp.left.map f = (X.right.map f.unop).unop
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ<GOAL>∀ (X_1 : SimplexCategoryᵒᵖ), X.leftOp.hom.app X_1 = (X.hom.app (Opposite.unop X_1)).unop
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ<GOAL>X.leftOp.right = Opposite.unop X.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ<GOAL>∀ (X_1 : SimplexCategoryᵒᵖ), X.leftOp.left.obj X_1 = Opposite.unop (X.right.obj (Opposite.unop X_1))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject.Augmented C<GOAL>X.rightOpLeftOpIso.inv.right = 𝟙 X.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject.Augmented C<GOAL>∀ (X_1 : SimplexCategoryᵒᵖ), X.rightOpLeftOpIso.hom.left.app X_1 = 𝟙 (X.left.obj X_1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject.Augmented C<GOAL>∀ (X_1 : SimplexCategoryᵒᵖ), X.rightOpLeftOpIso.inv.left.app X_1 = 𝟙 (X.left.obj X_1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.SimplicialObject.Augmented C<GOAL>X.rightOpLeftOpIso.hom.right = 𝟙 X.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ<GOAL>X.leftOpRightOpIso.hom.left = 𝟙 X.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ<GOAL>X.leftOpRightOpIso.inv.left = 𝟙 X.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ<GOAL>∀ (X_1 : SimplexCategory), X.leftOpRightOpIso.hom.right.app X_1 = 𝟙 (X.right.obj X_1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ<GOAL>∀ (X_1 : SimplexCategory), X.leftOpRightOpIso.inv.right.app X_1 = 𝟙 (X.right.obj X_1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : (CategoryTheory.SimplicialObject.Augmented C)ᵒᵖ<GOAL>(CategoryTheory.simplicialToCosimplicialAugmented C).obj X = (Opposite.unop X).rightOp
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : (CategoryTheory.SimplicialObject.Augmented C)ᵒᵖ} (f : X ⟶ Y), ((CategoryTheory.simplicialToCosimplicialAugmented C).map f).right = CategoryTheory.NatTrans.rightOp f.unop.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : (CategoryTheory.SimplicialObject.Augmented C)ᵒᵖ} (f : X ⟶ Y), ((CategoryTheory.simplicialToCosimplicialAugmented C).map f).left = f.unop.right.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ<GOAL>(CategoryTheory.cosimplicialToSimplicialAugmented C).obj X = Opposite.op X.leftOp
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.CosimplicialObject.Augmented Cᵒᵖ} (f : X ⟶ Y), (CategoryTheory.cosimplicialToSimplicialAugmented C).map f = Quiver.Hom.op { left := CategoryTheory.NatTrans.leftOp f.right, right := f.left.unop, w := ⋯ }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>(CategoryTheory.simplicialCosimplicialAugmentedEquiv C).functor = CategoryTheory.simplicialToCosimplicialAugmented C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>(CategoryTheory.simplicialCosimplicialAugmentedEquiv C).inverse = CategoryTheory.cosimplicialToSimplicialAugmented C
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>One α<VAR>A : Matrix V V α<VAR>self : A.IsAdjMatrix<GOAL>A.IsSymm
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>One α<VAR>A : Matrix V V α<VAR>self : A.IsAdjMatrix<VAR>i j : V<GOAL>A i j = 0 ∨ A i j = 1
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>One α<VAR>A : Matrix V V α<VAR>self : A.IsAdjMatrix<VAR>i : V<GOAL>A i i = 0
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>A : Matrix V V α<VAR>MulZeroOneClass α<VAR>Nontrivial α<VAR>h : A.IsAdjMatrix<VAR>i : V<GOAL>¬A i i = 1
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>A : Matrix V V α<VAR>MulZeroOneClass α<VAR>Nontrivial α<VAR>h : A.IsAdjMatrix<VAR>i j : V<GOAL>¬A i j = 1 ↔ A i j = 0
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>A : Matrix V V α<VAR>MulZeroOneClass α<VAR>Nontrivial α<VAR>h : A.IsAdjMatrix<VAR>i j : V<GOAL>¬A i j = 0 ↔ A i j = 1
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>A : Matrix V V α<VAR>MulZeroOneClass α<VAR>Nontrivial α<VAR>h : A.IsAdjMatrix<VAR>i j : V<GOAL>h.toGraph.Adj i j = (A i j = 1)
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DecidableEq V<VAR>A : Matrix V V α<VAR>Zero α<VAR>One α<VAR>i : V<GOAL>A.compl i i = 0
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DecidableEq V<VAR>A : Matrix V V α<VAR>Zero α<VAR>One α<VAR>i j : V<GOAL>A.compl i j = 0 ∨ A.compl i j = 1
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DecidableEq V<VAR>A : Matrix V V α<VAR>Zero α<VAR>One α<VAR>h : A.IsSymm<GOAL>A.compl.IsSymm
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DecidableEq V<VAR>A : Matrix V V α<VAR>Zero α<VAR>One α<VAR>h : A.IsSymm<GOAL>A.compl.IsAdjMatrix
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DecidableEq V<VAR>A : Matrix V V α<VAR>Zero α<VAR>One α<VAR>h : A.IsAdjMatrix<GOAL>A.compl.IsAdjMatrix
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DecidableEq V<VAR>A : Matrix V V α<VAR>MulZeroOneClass α<VAR>Nontrivial α<VAR>h : A.IsAdjMatrix<GOAL>⋯.toGraph = h.toGraphᶜ
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>v w : V<VAR>Zero α<VAR>One α<GOAL>SimpleGraph.adjMatrix α G v w = if G.Adj v w then 1 else 0
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>Zero α<VAR>One α<GOAL>(SimpleGraph.adjMatrix α G)ᵀ = SimpleGraph.adjMatrix α G
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>Zero α<VAR>One α<GOAL>(SimpleGraph.adjMatrix α G).IsSymm
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>Zero α<VAR>One α<GOAL>(SimpleGraph.adjMatrix α G).IsAdjMatrix
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>MulZeroOneClass α<VAR>Nontrivial α<GOAL>⋯.toGraph = G