ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X X' Y Y' Z : C<VAR>CategoryTheory.ExactPairing Y Y'<VAR>f : X ⟶ X'<VAR>g : X' ⟶ Z ⊗ Y'<GOAL>(CategoryTheory.tensorRightHomEquiv X Y Y' Z).symm (f ≫ g) = f ▷ Y ≫ (CategoryTheory.tensorRightHomEquiv X' Y Y' Z).symm g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X X' Y Y' Z Z' : C<VAR>CategoryTheory.ExactPairing Y Y'<VAR>f : X ⟶ Y ⊗ Z<VAR>g : X' ⟶ Z'<GOAL>(CategoryTheory.tensorLeftHomEquiv (X ⊗ X') Y Y' (Z ⊗ Z')).symm ((f ⊗ g) ≫ (α_ Y Z Z').hom) = (α_ Y' X X').inv ≫ ((CategoryTheory.tensorLeftHomEquiv X Y Y' Z).symm f ⊗ g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X X' Y Y' Z Z' : C<VAR>CategoryTheory.ExactPairing Y Y'<VAR>f : X ⟶ Z ⊗ Y'<VAR>g : X' ⟶ Z'<GOAL>(CategoryTheory.tensorRightHomEquiv (X' ⊗ X) Y Y' (Z' ⊗ Z)).symm ((g ⊗ f) ≫ (α_ Z' Z Y').inv) = (α_ X' X Y).hom ≫ (g ⊗ (CategoryTheory.tensorRightHomEquiv X Y Y' Z).symm f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>Y Y' Z : C<VAR>CategoryTheory.ExactPairing Y Y'<VAR>f : Y' ⟶ Z<GOAL>(CategoryTheory.tensorLeftHomEquiv (𝟙_ C) Y Y' Z).symm (η_ Y Y' ≫ Y ◁ f) = (ρ_ Y').hom ≫ f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.HasRightDual X<VAR>CategoryTheory.HasRightDual Y<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.tensorLeftHomEquiv (𝟙_ C) Y Yᘁ Xᘁ).symm (η_ X Xᘁ ≫ f ▷ Xᘁ) = (ρ_ Yᘁ).hom ≫ fᘁ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.HasLeftDual X<VAR>CategoryTheory.HasLeftDual Y<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.tensorRightHomEquiv (𝟙_ C) (ᘁY) Y ᘁX).symm (η_ (ᘁX) X ≫ ᘁX ◁ f) = (λ_ ᘁY).hom ≫ ᘁf
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>Y Y' Z : C<VAR>CategoryTheory.ExactPairing Y Y'<VAR>f : Y ⟶ Z<GOAL>(CategoryTheory.tensorRightHomEquiv (𝟙_ C) Y Y' Z).symm (η_ Y Y' ≫ f ▷ Y') = (λ_ Y).hom ≫ f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>Y Z : C<VAR>CategoryTheory.HasLeftDual Z<VAR>f : Y ⟶ ᘁZ<GOAL>(CategoryTheory.tensorLeftHomEquiv Y (ᘁZ) Z (𝟙_ C)) (Z ◁ f ≫ ε_ (ᘁZ) Z) = f ≫ (ρ_ ᘁZ).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.HasLeftDual X<VAR>CategoryTheory.HasLeftDual Y<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.tensorLeftHomEquiv (ᘁY) (ᘁX) X (𝟙_ C)) (f ▷ ᘁY ≫ ε_ (ᘁY) Y) = (ᘁf) ≫ (ρ_ ᘁX).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.HasRightDual X<VAR>CategoryTheory.HasRightDual Y<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.tensorRightHomEquiv Yᘁ X Xᘁ (𝟙_ C)) (Yᘁ ◁ f ≫ ε_ Y Yᘁ) = fᘁ ≫ (λ_ Xᘁ).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.HasRightDual X<VAR>f : Y ⟶ Xᘁ<GOAL>(CategoryTheory.tensorRightHomEquiv Y X Xᘁ (𝟙_ C)) (f ▷ X ≫ ε_ X Xᘁ) = f ≫ (λ_ Xᘁ).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.HasRightDual X<VAR>CategoryTheory.HasRightDual Y<VAR>f : X ⟶ Y<GOAL>η_ Y Yᘁ ≫ Y ◁ fᘁ = η_ X Xᘁ ≫ f ▷ Xᘁ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.HasLeftDual X<VAR>CategoryTheory.HasLeftDual Y<VAR>f : X ⟶ Y<GOAL>(X ◁ ᘁf) ≫ ε_ (ᘁX) X = f ▷ ᘁY ≫ ε_ (ᘁY) Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.HasLeftDual X<VAR>CategoryTheory.HasLeftDual Y<VAR>f : X ⟶ Y<GOAL>η_ (ᘁY) Y ≫ (ᘁf) ▷ Y = η_ (ᘁX) X ≫ ᘁX ◁ f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.HasRightDual X<VAR>CategoryTheory.HasRightDual Y<VAR>f : X ⟶ Y<GOAL>fᘁ ▷ X ≫ ε_ X Xᘁ = Yᘁ ◁ f ≫ ε_ Y Yᘁ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>p : CategoryTheory.ExactPairing X Y<GOAL>CategoryTheory.rightDualIso p p = CategoryTheory.Iso.refl Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>p : CategoryTheory.ExactPairing X Y<GOAL>CategoryTheory.leftDualIso p p = CategoryTheory.Iso.refl X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C n<VAR>i : ℕ<VAR>hi : i ≤ n := by valid<GOAL>F.map' i i ⋯ hi = CategoryTheory.CategoryStruct.id (F.obj ⟨i, ⋯⟩)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C n<VAR>i j k : ℕ<VAR>hij : i ≤ j := by valid<VAR>hjk : j ≤ k := by valid<VAR>hk : k ≤ n := by valid<GOAL>F.map' i k ⋯ hk = CategoryTheory.CategoryStruct.comp (F.map' i j hij ⋯) (F.map' j k hjk hk)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F G : CategoryTheory.ComposableArrows C n<VAR>φ : F ⟶ G<VAR>i j : ℕ<VAR>hij : i ≤ j := by valid<VAR>hj : j ≤ n := by valid<GOAL>CategoryTheory.CategoryStruct.comp (F.map' i j hij hj) (CategoryTheory.ComposableArrows.app' φ j hj) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.app' φ i ⋯) (G.map' i j hij hj)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : C<GOAL>∀ {X_1 Y : Fin 1} (x : X_1 ⟶ Y), (CategoryTheory.ComposableArrows.mk₀ X).map x = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : C<GOAL>∀ (x : Fin 1), (CategoryTheory.ComposableArrows.mk₀ X).obj x = X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X₀ X₁ : C<VAR>f : X₀ ⟶ X₁<VAR>i : Fin 2<GOAL>CategoryTheory.ComposableArrows.Mk₁.map f i i ⋯ = CategoryTheory.CategoryStruct.id (CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X₀ X₁ : C<VAR>f : X₀ ⟶ X₁<VAR>i j k : Fin 2<VAR>hij : i ≤ j<VAR>hjk : j ≤ k<GOAL>CategoryTheory.ComposableArrows.Mk₁.map f i k ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.Mk₁.map f i j hij) (CategoryTheory.ComposableArrows.Mk₁.map f j k hjk)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X₀ X₁ : C<VAR>f : X₀ ⟶ X₁<GOAL>∀ {X Y : Fin (1 + 1)} (g : X ⟶ Y), (CategoryTheory.ComposableArrows.mk₁ f).map g = CategoryTheory.ComposableArrows.Mk₁.map f X Y ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X₀ X₁ : C<VAR>f : X₀ ⟶ X₁<GOAL>∀ (a : Fin 2), (CategoryTheory.ComposableArrows.mk₁ f).obj a = CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ a
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F G : CategoryTheory.ComposableArrows C n<VAR>app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i<VAR>w : ∀ (i : ℕ) (hi : i < n), CategoryTheory.CategoryStruct.comp (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩) = CategoryTheory.CategoryStruct.comp (app ⟨i, ⋯⟩) (G.map' i (i + 1) ⋯ hi)<VAR>i : Fin (n + 1)<GOAL>(CategoryTheory.ComposableArrows.homMk app w).app i = app i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F G : CategoryTheory.ComposableArrows C n<VAR>app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i<VAR>w : ∀ (i : ℕ) (hi : i < n), CategoryTheory.CategoryStruct.comp (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩).hom = CategoryTheory.CategoryStruct.comp (app ⟨i, ⋯⟩).hom (G.map' i (i + 1) ⋯ hi)<GOAL>(CategoryTheory.ComposableArrows.isoMk app w).hom = CategoryTheory.ComposableArrows.homMk (fun i => (app i).hom) w
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F G : CategoryTheory.ComposableArrows C n<VAR>app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i<VAR>w : ∀ (i : ℕ) (hi : i < n), CategoryTheory.CategoryStruct.comp (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩).hom = CategoryTheory.CategoryStruct.comp (app ⟨i, ⋯⟩).hom (G.map' i (i + 1) ⋯ hi)<GOAL>(CategoryTheory.ComposableArrows.isoMk app w).inv = CategoryTheory.ComposableArrows.homMk (fun i => (app i).inv) ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F G : CategoryTheory.ComposableArrows C n<VAR>h : ∀ (i : Fin (n + 1)), F.obj i = G.obj i<VAR>w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (G.map' i (i + 1) ⋯ hi) (CategoryTheory.eqToHom ⋯))<GOAL>F = G
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>F G : CategoryTheory.ComposableArrows C 0<VAR>f : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯<VAR>i : Fin (0 + 1)<GOAL>(CategoryTheory.ComposableArrows.homMk₀ f).app i = match i with | ⟨0, isLt⟩ => f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>F G : CategoryTheory.ComposableArrows C 0<VAR>φ φ' : F ⟶ G<VAR>h : CategoryTheory.ComposableArrows.app' φ 0 ⋯ = CategoryTheory.ComposableArrows.app' φ' 0 ⋯<GOAL>φ = φ'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>F G : CategoryTheory.ComposableArrows C 0<VAR>e : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯<VAR>i : Fin (0 + 1)<GOAL>(CategoryTheory.ComposableArrows.isoMk₀ e).hom.app i = match i with | ⟨0, isLt⟩ => e.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>F G : CategoryTheory.ComposableArrows C 0<VAR>e : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯<VAR>i : Fin (0 + 1)<GOAL>(CategoryTheory.ComposableArrows.isoMk₀ e).inv.app i = match i with | ⟨0, isLt⟩ => e.inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>F G : CategoryTheory.ComposableArrows C 0<VAR>h : F.obj' 0 ⋯ = G.obj 0<GOAL>F = G
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>F : CategoryTheory.ComposableArrows C 0<GOAL>∃ X, F = CategoryTheory.ComposableArrows.mk₀ X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>F G : CategoryTheory.ComposableArrows C 1<VAR>left : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯<VAR>right : F.obj' 1 ⋯ ⟶ G.obj' 1 ⋯<VAR>w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 ⋯ ⋯) right = CategoryTheory.CategoryStruct.comp left (G.map' 0 1 ⋯ ⋯) := by aesop_cat<VAR>i : Fin (1 + 1)<GOAL>(CategoryTheory.ComposableArrows.homMk₁ left right w).app i = match i with | ⟨0, isLt⟩ => left | ⟨1, isLt⟩ => right
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>F G : CategoryTheory.ComposableArrows C 1<VAR>φ φ' : F ⟶ G<VAR>h₀ : CategoryTheory.ComposableArrows.app' φ 0 ⋯ = CategoryTheory.ComposableArrows.app' φ' 0 ⋯<VAR>h₁ : CategoryTheory.ComposableArrows.app' φ 1 ⋯ = CategoryTheory.ComposableArrows.app' φ' 1 ⋯<GOAL>φ = φ'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>F G : CategoryTheory.ComposableArrows C 1<VAR>left : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯<VAR>right : F.obj' 1 ⋯ ≅ G.obj' 1 ⋯<VAR>w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 ⋯ ⋯) right.hom = CategoryTheory.CategoryStruct.comp left.hom (G.map' 0 1 ⋯ ⋯) := by aesop_cat<VAR>i : Fin (1 + 1)<GOAL>(CategoryTheory.ComposableArrows.isoMk₁ left right w).hom.app i = match i with | ⟨0, isLt⟩ => left.hom | ⟨1, isLt⟩ => right.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>F G : CategoryTheory.ComposableArrows C 1<VAR>left : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯<VAR>right : F.obj' 1 ⋯ ≅ G.obj' 1 ⋯<VAR>w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 ⋯ ⋯) right.hom = CategoryTheory.CategoryStruct.comp left.hom (G.map' 0 1 ⋯ ⋯) := by aesop_cat<VAR>i : Fin (1 + 1)<GOAL>(CategoryTheory.ComposableArrows.isoMk₁ left right w).inv.app i = match i with | ⟨0, isLt⟩ => left.inv | ⟨1, isLt⟩ => right.inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>F : CategoryTheory.ComposableArrows C 1<GOAL>F.map' 0 1 ⋯ ⋯ = F.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>F G : CategoryTheory.ComposableArrows C 1<VAR>left : F.left = G.left<VAR>right : F.right = G.right<VAR>w : F.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom left) (CategoryTheory.CategoryStruct.comp G.hom (CategoryTheory.eqToHom ⋯))<GOAL>F = G
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.ComposableArrows C 1<GOAL>∃ X₀ X₁ f, X = CategoryTheory.ComposableArrows.mk₁ f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C n<VAR>X : C<GOAL>CategoryTheory.ComposableArrows.Precomp.obj F X 0 = X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C n<VAR>X : C<GOAL>CategoryTheory.ComposableArrows.Precomp.obj F X 1 = F.obj' 0 ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C n<VAR>X : C<VAR>i : ℕ<VAR>hi : i + 1 < n + 1 + 1<GOAL>CategoryTheory.ComposableArrows.Precomp.obj F X ⟨i + 1, hi⟩ = F.obj' i ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C n<VAR>X : C<VAR>f : X ⟶ F.left<GOAL>CategoryTheory.ComposableArrows.Precomp.map F f 0 0 ⋯ = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C n<VAR>X : C<VAR>f : X ⟶ F.left<GOAL>CategoryTheory.ComposableArrows.Precomp.map F f 1 1 ⋯ = F.map (CategoryTheory.CategoryStruct.id ⟨0, ⋯⟩)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C n<VAR>X : C<VAR>f : X ⟶ F.left<GOAL>CategoryTheory.ComposableArrows.Precomp.map F f 0 1 ⋯ = f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C n<VAR>X : C<VAR>f : X ⟶ F.left<GOAL>CategoryTheory.ComposableArrows.Precomp.map F f 0 ⟨0 + 1, ⋯⟩ ⋯ = f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C n<VAR>X : C<VAR>f : X ⟶ F.left<VAR>j : ℕ<VAR>hj : j + 2 < n + 1 + 1<GOAL>CategoryTheory.ComposableArrows.Precomp.map F f 0 ⟨j + 2, hj⟩ ⋯ = CategoryTheory.CategoryStruct.comp f (F.map' 0 (j + 1) ⋯ ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C n<VAR>X : C<VAR>f : X ⟶ F.left<VAR>i j : ℕ<VAR>hi : i + 1 < n + 1 + 1<VAR>hj : j + 1 < n + 1 + 1<VAR>hij : i + 1 ≤ j + 1<GOAL>CategoryTheory.ComposableArrows.Precomp.map F f ⟨i + 1, hi⟩ ⟨j + 1, hj⟩ hij = F.map' i j ⋯ ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C n<VAR>X : C<VAR>f : X ⟶ F.left<VAR>j : ℕ<VAR>hj : j + 1 < n + 1 + 1<GOAL>CategoryTheory.ComposableArrows.Precomp.map F f 1 ⟨j + 1, hj⟩ ⋯ = F.map' 0 j ⋯ ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C n<VAR>X : C<VAR>f : X ⟶ F.left<VAR>i : Fin (n + 1 + 1)<GOAL>CategoryTheory.ComposableArrows.Precomp.map F f i i ⋯ = CategoryTheory.CategoryStruct.id (CategoryTheory.ComposableArrows.Precomp.obj F X i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C n<VAR>X : C<VAR>f : X ⟶ F.left<VAR>i j k : Fin (n + 1 + 1)<VAR>hij : i ≤ j<VAR>hjk : j ≤ k<GOAL>CategoryTheory.ComposableArrows.Precomp.map F f i k ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.Precomp.map F f i j hij) (CategoryTheory.ComposableArrows.Precomp.map F f j k hjk)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C n<VAR>X : C<VAR>f : X ⟶ F.left<GOAL>∀ (a : Fin (n + 1 + 1)), (F.precomp f).obj a = CategoryTheory.ComposableArrows.Precomp.obj F X a
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C n<VAR>X : C<VAR>f : X ⟶ F.left<GOAL>∀ {X_1 Y : Fin (n + 1 + 1)} (g : X_1 ⟶ Y), (F.precomp f).map g = CategoryTheory.ComposableArrows.Precomp.map F f X_1 Y ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n m : ℕ<VAR>F : CategoryTheory.ComposableArrows C m<VAR>Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))<GOAL>∀ {X Y : Fin (n + 1)} (f : X ⟶ Y), (F.whiskerLeft Φ).map f = F.map (Φ.map f)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n m : ℕ<VAR>F : CategoryTheory.ComposableArrows C m<VAR>Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))<VAR>X : Fin (n + 1)<GOAL>(F.whiskerLeft Φ).obj X = F.obj (Φ.obj X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n m : ℕ<VAR>Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))<VAR>F : CategoryTheory.ComposableArrows C m<VAR>X : Fin (n + 1)<GOAL>((CategoryTheory.ComposableArrows.whiskerLeftFunctor Φ).obj F).obj X = F.obj (Φ.obj X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n m : ℕ<VAR>Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))<GOAL>∀ {X Y : CategoryTheory.ComposableArrows C m} (f : X ⟶ Y) (X_1 : Fin (n + 1)), ((CategoryTheory.ComposableArrows.whiskerLeftFunctor Φ).map f).app X_1 = f.app (Φ.obj X_1)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n m : ℕ<VAR>Φ : CategoryTheory.Functor (Fin (n + 1)) (Fin (m + 1))<VAR>F : CategoryTheory.ComposableArrows C m<GOAL>∀ {X Y : Fin (n + 1)} (f : X ⟶ Y), ((CategoryTheory.ComposableArrows.whiskerLeftFunctor Φ).obj F).map f = F.map (Φ.map f)
<VAR>n : ℕ<VAR>i : Fin n<GOAL>(Fin.succFunctor n).obj i = i.succ
<VAR>n : ℕ<VAR>i j : Fin n<VAR>hij : i ⟶ j<GOAL>(Fin.succFunctor n).map hij = CategoryTheory.homOfLE ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C (n + 1)<VAR>X : Fin (n + 1)<GOAL>(CategoryTheory.ComposableArrows.δ₀Functor.obj F).obj X = F.obj X.succ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<GOAL>∀ {X Y : CategoryTheory.ComposableArrows C (n + 1)} (f : X ⟶ Y) (X_1 : Fin (n + 1)), (CategoryTheory.ComposableArrows.δ₀Functor.map f).app X_1 = f.app X_1.succ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C (n + 1)<GOAL>∀ {X Y : Fin (n + 1)} (f : X ⟶ Y), (CategoryTheory.ComposableArrows.δ₀Functor.obj F).map f = F.map (CategoryTheory.homOfLE ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C n<VAR>X : C<VAR>f : X ⟶ F.left<GOAL>(F.precomp f).δ₀ = F
<VAR>n : ℕ<VAR>i : Fin n<GOAL>(Fin.castSuccFunctor n).obj i = i.castSucc
<VAR>n : ℕ<GOAL>∀ {X Y : Fin n} (hij : X ⟶ Y), (Fin.castSuccFunctor n).map hij = hij
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C (n + 1)<GOAL>∀ {X Y : Fin (n + 1)} (f : X ⟶ Y), (CategoryTheory.ComposableArrows.δlastFunctor.obj F).map f = F.map f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<GOAL>∀ {X Y : CategoryTheory.ComposableArrows C (n + 1)} (f : X ⟶ Y) (X_1 : Fin (n + 1)), (CategoryTheory.ComposableArrows.δlastFunctor.map f).app X_1 = f.app X_1.castSucc
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C (n + 1)<VAR>X : Fin (n + 1)<GOAL>(CategoryTheory.ComposableArrows.δlastFunctor.obj F).obj X = F.obj X.castSucc
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F G : CategoryTheory.ComposableArrows C (n + 1)<VAR>α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯<VAR>β : F.δ₀ ⟶ G.δ₀<VAR>w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 ⋯ ⋯) (CategoryTheory.ComposableArrows.app' β 0 ⋯) = CategoryTheory.CategoryStruct.comp α (G.map' 0 1 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMkSucc α β w).app 0 = α
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F G : CategoryTheory.ComposableArrows C (n + 1)<VAR>α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯<VAR>β : F.δ₀ ⟶ G.δ₀<VAR>w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 ⋯ ⋯) (CategoryTheory.ComposableArrows.app' β 0 ⋯) = CategoryTheory.CategoryStruct.comp α (G.map' 0 1 ⋯ ⋯)<VAR>i : ℕ<VAR>hi : i + 1 < n + 1 + 1<GOAL>(CategoryTheory.ComposableArrows.homMkSucc α β w).app ⟨i + 1, hi⟩ = CategoryTheory.ComposableArrows.app' β i ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F G : CategoryTheory.ComposableArrows C (n + 1)<VAR>f g : F ⟶ G<VAR>h₀ : CategoryTheory.ComposableArrows.app' f 0 ⋯ = CategoryTheory.ComposableArrows.app' g 0 ⋯<VAR>h₁ : CategoryTheory.ComposableArrows.δ₀Functor.map f = CategoryTheory.ComposableArrows.δ₀Functor.map g<GOAL>f = g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F G : CategoryTheory.ComposableArrows C (n + 1)<VAR>α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯<VAR>β : F.δ₀ ≅ G.δ₀<VAR>w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 ⋯ ⋯) (CategoryTheory.ComposableArrows.app' β.hom 0 ⋯) = CategoryTheory.CategoryStruct.comp α.hom (G.map' 0 1 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.isoMkSucc α β w).inv = CategoryTheory.ComposableArrows.homMkSucc α.inv β.inv ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F G : CategoryTheory.ComposableArrows C (n + 1)<VAR>α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯<VAR>β : F.δ₀ ≅ G.δ₀<VAR>w : CategoryTheory.CategoryStruct.comp (F.map' 0 1 ⋯ ⋯) (CategoryTheory.ComposableArrows.app' β.hom 0 ⋯) = CategoryTheory.CategoryStruct.comp α.hom (G.map' 0 1 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.isoMkSucc α β w).hom = CategoryTheory.ComposableArrows.homMkSucc α.hom β.hom w
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F G : CategoryTheory.ComposableArrows C (n + 1)<VAR>h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯<VAR>h : F.δ₀ = G.δ₀<VAR>w : F.map' 0 1 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀) (CategoryTheory.CategoryStruct.comp (G.map' 0 1 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))<GOAL>F = G
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n : ℕ<VAR>F : CategoryTheory.ComposableArrows C (n + 1)<GOAL>∃ F₀ X₀ f₀, F = F₀.precomp f₀
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 2<VAR>app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯<VAR>w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯)<VAR>w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁).app 0 = app₀
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 2<VAR>app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯<VAR>w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯)<VAR>w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁).app 1 = app₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 2<VAR>app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯<VAR>w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁ = CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 ⋯ ⋯)<VAR>w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂ = CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁).app ⟨2, ⋯⟩ = app₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 2<VAR>φ φ' : f ⟶ g<VAR>h₀ : CategoryTheory.ComposableArrows.app' φ 0 ⋯ = CategoryTheory.ComposableArrows.app' φ' 0 ⋯<VAR>h₁ : CategoryTheory.ComposableArrows.app' φ 1 ⋯ = CategoryTheory.ComposableArrows.app' φ' 1 ⋯<VAR>h₂ : CategoryTheory.ComposableArrows.app' φ 2 ⋯ = CategoryTheory.ComposableArrows.app' φ' 2 ⋯<GOAL>φ = φ'