Composable arrows

If C is a category, the type of n-simplices in the nerve of C identifies to the type of functors Fin (n + 1) ⥤ C, which can be thought of as families of n composable arrows in C. In this file, we introduce and study this category ComposableArrows C n of n composable arrows in C.

If F : ComposableArrows C n, we define F.left as the leftmost object, F.right as the rightmost object, and F.hom : F.left ⟶ F.right is the canonical map.

The most significant definition in this file is the constructor F.precomp f : ComposableArrows C (n + 1) for F : ComposableArrows C n and f : X ⟶ F.left: "it shifts F towards the right and inserts f on the left". This precomp has good definitional properties.

In the namespace CategoryTheory.ComposableArrows, we provide constructors like mk₁ f, mk₂ f g, mk₃ f g h for ComposableArrows C n for small n.

TODO (@joelriou):

• construct some elements in ComposableArrows m (Fin (n + 1)) for small n the precomposition with which shall induce functors ComposableArrows C n ⥤ ComposableArrows C m which correspond to simplicial operations (specifically faces) with good definitional properties (this might be necessary for up to n = 7 in order to formalize spectral sequences following Verdier)

New simprocs that run even in dsimp have caused breakages in this file.

(e.g. dsimp can now simplify 2 + 3 to 5)

For now, we just turn off the offending simprocs in this file.

However, hopefully it is possible to refactor the material here so that no disabling of simprocs is needed.

See issue https://github.com/leanprover-community/mathlib4/issues/27382.

@[reducible, inline]

abbrev CategoryTheory.ComposableArrows (C : Type u_1) [Category.{v_1, u_1} C] (n : ℕ) : Type (max v_1 u_1)

ComposableArrows C n is the type of functors Fin (n + 1) ⥤ C.

def CategoryTheory.ComposableArrows.tacticValid : Lean.ParserDescr

A wrapper for omega which prefaces it with some quick and useful attempts

@[reducible, inline]

abbrev CategoryTheory.ComposableArrows.obj' {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) (i : ℕ) (hi : i ≤ n := by valid) : C

The ith object (with i : ℕ such that i ≤ n) of F : ComposableArrows C n.

@[reducible, inline]

abbrev CategoryTheory.ComposableArrows.map' {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) (i j : ℕ) (hij : i ≤ j := by valid) (hjn : j ≤ n := by valid) : F.obj ⟨i, ⋯⟩ ⟶ F.obj ⟨j, ⋯⟩

The map F.obj' i ⟶ F.obj' j when F : ComposableArrows C n, and i and j are natural numbers such that i ≤ j ≤ n.

theorem CategoryTheory.ComposableArrows.map'_self {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) (i : ℕ) (hi : i ≤ n := by valid) : F.map' i i ⋯ hi = CategoryStruct.id (F.obj ⟨i, ⋯⟩)

theorem CategoryTheory.ComposableArrows.map'_comp {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) (i j k : ℕ) (hij : i ≤ j := by valid) (hjk : j ≤ k := by valid) (hk : k ≤ n := by valid) : F.map' i k ⋯ hk = CategoryStruct.comp (F.map' i j hij ⋯) (F.map' j k hjk hk)

@[reducible, inline]

abbrev CategoryTheory.ComposableArrows.left {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) : C

The leftmost object of F : ComposableArrows C n.

@[reducible, inline]

abbrev CategoryTheory.ComposableArrows.right {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) : C

The rightmost object of F : ComposableArrows C n.

@[reducible, inline]

abbrev CategoryTheory.ComposableArrows.hom {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) : F.left ⟶ F.right

The canonical map F.left ⟶ F.right for F : ComposableArrows C n.

@[reducible, inline]

abbrev CategoryTheory.ComposableArrows.app' {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {F G : ComposableArrows C n} (φ : F ⟶ G) (i : ℕ) (hi : i ≤ n := by valid) : F.obj' i hi ⟶ G.obj' i hi

The map F.obj' i ⟶ G.obj' i induced on ith objects by a morphism F ⟶ G in ComposableArrows C n when i is a natural number such that i ≤ n.

theorem CategoryTheory.ComposableArrows.naturality' {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {F G : ComposableArrows C n} (φ : F ⟶ G) (i j : ℕ) (hij : i ≤ j := by valid) (hj : j ≤ n := by valid) : CategoryStruct.comp (F.map' i j hij hj) (app' φ j hj) = CategoryStruct.comp (app' φ i ⋯) (G.map' i j hij hj)

theorem CategoryTheory.ComposableArrows.naturality'_assoc {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {F G : ComposableArrows C n} (φ : F ⟶ G) (i j : ℕ) (hij : i ≤ j := by valid) (hj : j ≤ n := by valid) {Z : C} (h : G.obj' j hj ⟶ Z) : CategoryStruct.comp (F.map' i j hij hj) (CategoryStruct.comp (app' φ j hj) h) = CategoryStruct.comp (app' φ i ⋯) (CategoryStruct.comp (G.map' i j hij hj) h)

def CategoryTheory.ComposableArrows.mk₀ {C : Type u_1} [Category.{v_1, u_1} C] (X : C) : ComposableArrows C 0

Constructor for ComposableArrows C 0.

@[simp]

theorem CategoryTheory.ComposableArrows.mk₀_map {C : Type u_1} [Category.{v_1, u_1} C] (X : C) {X✝ Y✝ : Fin 1} (x✝ : X✝ ⟶ Y✝) : (mk₀ X).map x✝ = CategoryStruct.id X

@[simp]

theorem CategoryTheory.ComposableArrows.mk₀_obj {C : Type u_1} [Category.{v_1, u_1} C] (X : C) (x✝ : Fin 1) : (mk₀ X).obj x✝ = X

def CategoryTheory.ComposableArrows.Mk₁.obj {C : Type u_1} (X₀ X₁ : C) : Fin 2 → C

The map which sends 0 : Fin 2 to X₀ and 1 to X₁.

def CategoryTheory.ComposableArrows.Mk₁.map {C : Type u_1} [Category.{v_1, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) (i j : Fin 2) : i ≤ j → (obj X₀ X₁ i ⟶ obj X₀ X₁ j)

The obvious map obj X₀ X₁ i ⟶ obj X₀ X₁ j whenever i j : Fin 2 satisfy i ≤ j.

theorem CategoryTheory.ComposableArrows.Mk₁.map_id {C : Type u_1} [Category.{v_1, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) (i : Fin 2) : map f i i ⋯ = CategoryStruct.id (obj X₀ X₁ i)

theorem CategoryTheory.ComposableArrows.Mk₁.map_comp {C : Type u_1} [Category.{v_1, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) {i j k : Fin 2} (hij : i ≤ j) (hjk : j ≤ k) : map f i k ⋯ = CategoryStruct.comp (map f i j hij) (map f j k hjk)

def CategoryTheory.ComposableArrows.mk₁ {C : Type u_1} [Category.{v_1, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) : ComposableArrows C 1

Constructor for ComposableArrows C 1.

@[simp]

theorem CategoryTheory.ComposableArrows.mk₁_map {C : Type u_1} [Category.{v_1, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) {X✝ Y✝ : Fin (1 + 1)} (g : X✝ ⟶ Y✝) : (mk₁ f).map g = Mk₁.map f X✝ Y✝ ⋯

@[simp]

theorem CategoryTheory.ComposableArrows.mk₁_obj {C : Type u_1} [Category.{v_1, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) (a✝ : Fin 2) : (mk₁ f).obj a✝ = Mk₁.obj X₀ X₁ a✝

def CategoryTheory.ComposableArrows.homMk {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {F G : ComposableArrows C n} (app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i) (w : ∀ (i : ℕ) (hi : i < n), CategoryStruct.comp (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩) = CategoryStruct.comp (app ⟨i, ⋯⟩) (G.map' i (i + 1) ⋯ hi)) : F ⟶ G

Constructor for morphisms F ⟶ G in ComposableArrows C n which takes as inputs a family of morphisms F.obj i ⟶ G.obj i and the naturality condition only for the maps in Fin (n + 1) given by inequalities of the form i ≤ i + 1.

@[simp]

theorem CategoryTheory.ComposableArrows.homMk_app {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {F G : ComposableArrows C n} (app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i) (w : ∀ (i : ℕ) (hi : i < n), CategoryStruct.comp (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩) = CategoryStruct.comp (app ⟨i, ⋯⟩) (G.map' i (i + 1) ⋯ hi)) (i : Fin (n + 1)) : (homMk app w).app i = app i

def CategoryTheory.ComposableArrows.isoMk {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {F G : ComposableArrows C n} (app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i) (w : ∀ (i : ℕ) (hi : i < n), CategoryStruct.comp (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩).hom = CategoryStruct.comp (app ⟨i, ⋯⟩).hom (G.map' i (i + 1) ⋯ hi)) : F ≅ G

Constructor for isomorphisms F ≅ G in ComposableArrows C n which takes as inputs a family of isomorphisms F.obj i ≅ G.obj i and the naturality condition only for the maps in Fin (n + 1) given by inequalities of the form i ≤ i + 1.

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk_hom {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {F G : ComposableArrows C n} (app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i) (w : ∀ (i : ℕ) (hi : i < n), CategoryStruct.comp (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩).hom = CategoryStruct.comp (app ⟨i, ⋯⟩).hom (G.map' i (i + 1) ⋯ hi)) : (isoMk app w).hom = homMk (fun (i : Fin (n + 1)) => (app i).hom) w

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk_inv {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {F G : ComposableArrows C n} (app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i) (w : ∀ (i : ℕ) (hi : i < n), CategoryStruct.comp (F.map' i (i + 1) ⋯ hi) (app ⟨i + 1, ⋯⟩).hom = CategoryStruct.comp (app ⟨i, ⋯⟩).hom (G.map' i (i + 1) ⋯ hi)) : (isoMk app w).inv = homMk (fun (i : Fin (n + 1)) => (app i).inv) ⋯

theorem CategoryTheory.ComposableArrows.ext {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {F G : ComposableArrows C n} (h : ∀ (i : Fin (n + 1)), F.obj i = G.obj i) (w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (G.map' i (i + 1) ⋯ hi) (eqToHom ⋯))) : F = G

def CategoryTheory.ComposableArrows.homMk₀ {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 0} (f : F.obj' 0 homMk₀._proof_1 ⟶ G.obj' 0 homMk₀._proof_1) : F ⟶ G

Constructor for morphisms in ComposableArrows C 0.

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₀_app {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 0} (f : F.obj' 0 homMk₀._proof_1 ⟶ G.obj' 0 homMk₀._proof_1) (i : Fin (0 + 1)) : (homMk₀ f).app i = match i with | ⟨0, isLt⟩ => f

theorem CategoryTheory.ComposableArrows.hom_ext₀ {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 0} {φ φ' : F ⟶ G} (h : app' φ 0 homMk₀._proof_1 = app' φ' 0 homMk₀._proof_1) : φ = φ'

theorem CategoryTheory.ComposableArrows.hom_ext₀_iff {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 0} {φ φ' : F ⟶ G} : φ = φ' ↔ app' φ 0 homMk₀._proof_1 = app' φ' 0 homMk₀._proof_1

def CategoryTheory.ComposableArrows.isoMk₀ {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 0} (e : F.obj' 0 homMk₀._proof_1 ≅ G.obj' 0 homMk₀._proof_1) : F ≅ G

Constructor for isomorphisms in ComposableArrows C 0.

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₀_inv_app {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 0} (e : F.obj' 0 homMk₀._proof_1 ≅ G.obj' 0 homMk₀._proof_1) (i : Fin (0 + 1)) : (isoMk₀ e).inv.app i = match i with | ⟨0, isLt⟩ => e.inv

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₀_hom_app {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 0} (e : F.obj' 0 homMk₀._proof_1 ≅ G.obj' 0 homMk₀._proof_1) (i : Fin (0 + 1)) : (isoMk₀ e).hom.app i = match i with | ⟨0, isLt⟩ => e.hom

theorem CategoryTheory.ComposableArrows.isIso_iff₀ {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 0} (f : F ⟶ G) : IsIso f ↔ IsIso (f.app 0)

theorem CategoryTheory.ComposableArrows.ext₀ {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 0} (h : F.obj' 0 homMk₀._proof_1 = G.obj 0) : F = G

theorem CategoryTheory.ComposableArrows.mk₀_surjective {C : Type u_1} [Category.{v_1, u_1} C] (F : ComposableArrows C 0) : ∃ (X : C), F = mk₀ X

def CategoryTheory.ComposableArrows.homMk₁ {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 1} (left : F.obj' 0 homMk₁._proof_4 ⟶ G.obj' 0 homMk₁._proof_4) (right : F.obj' 1 homMk₁._proof_5 ⟶ G.obj' 1 homMk₁._proof_5) (w : CategoryStruct.comp (F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5) right = CategoryStruct.comp left (G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5) := by cat_disch) : F ⟶ G

Constructor for morphisms in ComposableArrows C 1.

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₁_app {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 1} (left : F.obj' 0 homMk₁._proof_4 ⟶ G.obj' 0 homMk₁._proof_4) (right : F.obj' 1 homMk₁._proof_5 ⟶ G.obj' 1 homMk₁._proof_5) (w : CategoryStruct.comp (F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5) right = CategoryStruct.comp left (G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5) := by cat_disch) (i : Fin (1 + 1)) : (homMk₁ left right w).app i = match i with | ⟨0, isLt⟩ => left | ⟨1, isLt⟩ => right

theorem CategoryTheory.ComposableArrows.hom_ext₁ {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 1} {φ φ' : F ⟶ G} (h₀ : app' φ 0 homMk₁._proof_4 = app' φ' 0 homMk₁._proof_4) (h₁ : app' φ 1 homMk₁._proof_5 = app' φ' 1 homMk₁._proof_5) : φ = φ'

theorem CategoryTheory.ComposableArrows.hom_ext₁_iff {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 1} {φ φ' : F ⟶ G} : φ = φ' ↔ app' φ 0 homMk₁._proof_4 = app' φ' 0 homMk₁._proof_4 ∧ app' φ 1 homMk₁._proof_5 = app' φ' 1 homMk₁._proof_5

def CategoryTheory.ComposableArrows.isoMk₁ {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 1} (left : F.obj' 0 homMk₁._proof_4 ≅ G.obj' 0 homMk₁._proof_4) (right : F.obj' 1 homMk₁._proof_5 ≅ G.obj' 1 homMk₁._proof_5) (w : CategoryStruct.comp (F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5) right.hom = CategoryStruct.comp left.hom (G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5) := by cat_disch) : F ≅ G

Constructor for isomorphisms in ComposableArrows C 1.

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₁_hom_app {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 1} (left : F.obj' 0 homMk₁._proof_4 ≅ G.obj' 0 homMk₁._proof_4) (right : F.obj' 1 homMk₁._proof_5 ≅ G.obj' 1 homMk₁._proof_5) (w : CategoryStruct.comp (F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5) right.hom = CategoryStruct.comp left.hom (G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5) := by cat_disch) (i : Fin (1 + 1)) : (isoMk₁ left right w).hom.app i = match i with | ⟨0, isLt⟩ => left.hom | ⟨1, isLt⟩ => right.hom

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₁_inv_app {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 1} (left : F.obj' 0 homMk₁._proof_4 ≅ G.obj' 0 homMk₁._proof_4) (right : F.obj' 1 homMk₁._proof_5 ≅ G.obj' 1 homMk₁._proof_5) (w : CategoryStruct.comp (F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5) right.hom = CategoryStruct.comp left.hom (G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5) := by cat_disch) (i : Fin (1 + 1)) : (isoMk₁ left right w).inv.app i = match i with | ⟨0, isLt⟩ => left.inv | ⟨1, isLt⟩ => right.inv

theorem CategoryTheory.ComposableArrows.map'_eq_hom₁ {C : Type u_1} [Category.{v_1, u_1} C] (F : ComposableArrows C 1) : F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 = F.hom

theorem CategoryTheory.ComposableArrows.isIso_iff₁ {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 1} (f : F ⟶ G) : IsIso f ↔ IsIso (f.app 0) ∧ IsIso (f.app 1)

theorem CategoryTheory.ComposableArrows.ext₁ {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 1} (left : F.left = G.left) (right : F.right = G.right) (w : F.hom = CategoryStruct.comp (eqToHom left) (CategoryStruct.comp G.hom (eqToHom ⋯))) : F = G

theorem CategoryTheory.ComposableArrows.mk₁_surjective {C : Type u_1} [Category.{v_1, u_1} C] (X : ComposableArrows C 1) : ∃ (X₀ : C) (X₁ : C) (f : X₀ ⟶ X₁), X = mk₁ f

theorem CategoryTheory.ComposableArrows.mk₁_eqToHom_comp {C : Type u_1} [Category.{v_1, u_1} C] {X₀' X₀ X₁ : C} (h : X₀' = X₀) (f : X₀ ⟶ X₁) : mk₁ (CategoryStruct.comp (eqToHom h) f) = mk₁ f

theorem CategoryTheory.ComposableArrows.mk₁_comp_eqToHom {C : Type u_1} [Category.{v_1, u_1} C] {X₀ X₁ X₁' : C} (f : X₀ ⟶ X₁) (h : X₁ = X₁') : mk₁ (CategoryStruct.comp f (eqToHom h)) = mk₁ f

theorem CategoryTheory.ComposableArrows.mk₁_hom {C : Type u_1} [Category.{v_1, u_1} C] (X : ComposableArrows C 1) : mk₁ X.hom = X

def CategoryTheory.ComposableArrows.arrowEquiv {C : Type u_1} [Category.{v_1, u_1} C] : ComposableArrows C 1 ≃ Arrow C

The bijection between ComposableArrows C 1 and Arrow C.

@[simp]

theorem CategoryTheory.ComposableArrows.arrowEquiv_apply {C : Type u_1} [Category.{v_1, u_1} C] (F : ComposableArrows C 1) : arrowEquiv F = Arrow.mk F.hom

@[simp]

theorem CategoryTheory.ComposableArrows.arrowEquiv_symm_apply {C : Type u_1} [Category.{v_1, u_1} C] (f : Arrow C) : arrowEquiv.symm f = mk₁ f.hom

def CategoryTheory.ComposableArrows.Precomp.obj {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) (X : C) : Fin (n + 1 + 1) → C

The map Fin (n + 1 + 1) → C which "shifts" F.obj' to the right and inserts X in the zeroth position.

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.obj_zero {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) (X : C) : obj F X 0 = X

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.obj_one {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) (X : C) : obj F X 1 = F.obj' 0 ⋯

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.obj_succ {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) (X : C) (i : ℕ) (hi : i + 1 < n + 1 + 1) : obj F X ⟨i + 1, hi⟩ = F.obj' i ⋯

def CategoryTheory.ComposableArrows.Precomp.map {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) {X : C} (f : X ⟶ F.left) (i j : Fin (n + 1 + 1)) : i ≤ j → (obj F X i ⟶ obj F X j)

Auxiliary definition for the action on maps of the functor F.precomp f. It sends 0 ≤ 1 to f and i + 1 ≤ j + 1 to F.map' i j.

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.map_zero_zero {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) {X : C} (f : X ⟶ F.left) : map F f 0 0 ⋯ = CategoryStruct.id X

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.map_one_one {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) {X : C} (f : X ⟶ F.left) : map F f 1 1 ⋯ = F.map (CategoryStruct.id ⟨0, ⋯⟩)

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.map_zero_one {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) {X : C} (f : X ⟶ F.left) : map F f 0 1 ⋯ = f

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.map_zero_one' {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) {X : C} (f : X ⟶ F.left) : map F f 0 ⟨0 + 1, ⋯⟩ ⋯ = f

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.map_zero_succ_succ {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) {X : C} (f : X ⟶ F.left) (j : ℕ) (hj : j + 2 < n + 1 + 1) : map F f 0 ⟨j + 2, hj⟩ ⋯ = CategoryStruct.comp f (F.map' 0 (j + 1) ⋯ ⋯)

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.map_succ_succ {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) {X : C} (f : X ⟶ F.left) (i j : ℕ) (hi : i + 1 < n + 1 + 1) (hj : j + 1 < n + 1 + 1) (hij : i + 1 ≤ j + 1) : map F f ⟨i + 1, hi⟩ ⟨j + 1, hj⟩ hij = F.map' i j ⋯ ⋯

@[simp]

theorem CategoryTheory.ComposableArrows.Precomp.map_one_succ {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) {X : C} (f : X ⟶ F.left) (j : ℕ) (hj : j + 1 < n + 1 + 1) : map F f 1 ⟨j + 1, hj⟩ ⋯ = F.map' 0 j ⋯ ⋯

theorem CategoryTheory.ComposableArrows.Precomp.map_id {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) {X : C} (f : X ⟶ F.left) (i : Fin (n + 1 + 1)) : map F f i i ⋯ = CategoryStruct.id (obj F X i)

theorem CategoryTheory.ComposableArrows.Precomp.map_comp {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) {X : C} (f : X ⟶ F.left) {i j k : Fin (n + 1 + 1)} (hij : i ≤ j) (hjk : j ≤ k) : map F f i k ⋯ = CategoryStruct.comp (map F f i j hij) (map F f j k hjk)

def CategoryTheory.ComposableArrows.precomp {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) {X : C} (f : X ⟶ F.left) : ComposableArrows C (n + 1)

"Precomposition" of F : ComposableArrows C n by a morphism f : X ⟶ F.left.

@[simp]

theorem CategoryTheory.ComposableArrows.precomp_map {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) {X : C} (f : X ⟶ F.left) {X✝ Y✝ : Fin (n + 1 + 1)} (g : X✝ ⟶ Y✝) : (F.precomp f).map g = Precomp.map F f X✝ Y✝ ⋯

@[simp]

theorem CategoryTheory.ComposableArrows.precomp_obj {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) {X : C} (f : X ⟶ F.left) (a✝ : Fin (n + 1 + 1)) : (F.precomp f).obj a✝ = Precomp.obj F X a✝

@[reducible, inline]

abbrev CategoryTheory.ComposableArrows.mk₂ {C : Type u_1} [Category.{v_1, u_1} C] {X₀ X₁ X₂ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) : ComposableArrows C 2

Constructor for ComposableArrows C 2.

@[reducible, inline]

abbrev CategoryTheory.ComposableArrows.mk₃ {C : Type u_1} [Category.{v_1, u_1} C] {X₀ X₁ X₂ X₃ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) : ComposableArrows C 3

Constructor for ComposableArrows C 3.

@[reducible, inline]

abbrev CategoryTheory.ComposableArrows.mk₄ {C : Type u_1} [Category.{v_1, u_1} C] {X₀ X₁ X₂ X₃ X₄ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) (i : X₃ ⟶ X₄) : ComposableArrows C 4

Constructor for ComposableArrows C 4.

@[reducible, inline]

abbrev CategoryTheory.ComposableArrows.mk₅ {C : Type u_1} [Category.{v_1, u_1} C] {X₀ X₁ X₂ X₃ X₄ X₅ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) (i : X₃ ⟶ X₄) (j : X₄ ⟶ X₅) : ComposableArrows C 5

Constructor for ComposableArrows C 5.

These examples are meant to test the good definitional properties of precomp, and that dsimp can see through.

def CategoryTheory.ComposableArrows.whiskerLeft {C : Type u_1} [Category.{v_1, u_1} C] {n m : ℕ} (F : ComposableArrows C m) (Φ : Functor (Fin (n + 1)) (Fin (m + 1))) : ComposableArrows C n

The map ComposableArrows C m → ComposableArrows C n obtained by precomposition with a functor Fin (n + 1) ⥤ Fin (m + 1).

@[simp]

theorem CategoryTheory.ComposableArrows.whiskerLeft_obj {C : Type u_1} [Category.{v_1, u_1} C] {n m : ℕ} (F : ComposableArrows C m) (Φ : Functor (Fin (n + 1)) (Fin (m + 1))) (X : Fin (n + 1)) : (F.whiskerLeft Φ).obj X = F.obj (Φ.obj X)

@[simp]

theorem CategoryTheory.ComposableArrows.whiskerLeft_map {C : Type u_1} [Category.{v_1, u_1} C] {n m : ℕ} (F : ComposableArrows C m) (Φ : Functor (Fin (n + 1)) (Fin (m + 1))) {X✝ Y✝ : Fin (n + 1)} (f : X✝ ⟶ Y✝) : (F.whiskerLeft Φ).map f = F.map (Φ.map f)

def CategoryTheory.ComposableArrows.whiskerLeftFunctor {C : Type u_1} [Category.{v_1, u_1} C] {n m : ℕ} (Φ : Functor (Fin (n + 1)) (Fin (m + 1))) : Functor (ComposableArrows C m) (ComposableArrows C n)

The functor ComposableArrows C m ⥤ ComposableArrows C n obtained by precomposition with a functor Fin (n + 1) ⥤ Fin (m + 1).

@[simp]

theorem CategoryTheory.ComposableArrows.whiskerLeftFunctor_map_app {C : Type u_1} [Category.{v_1, u_1} C] {n m : ℕ} (Φ : Functor (Fin (n + 1)) (Fin (m + 1))) {X✝ Y✝ : ComposableArrows C m} (f : X✝ ⟶ Y✝) (X : Fin (n + 1)) : ((whiskerLeftFunctor Φ).map f).app X = f.app (Φ.obj X)

@[simp]

theorem CategoryTheory.ComposableArrows.whiskerLeftFunctor_obj_obj {C : Type u_1} [Category.{v_1, u_1} C] {n m : ℕ} (Φ : Functor (Fin (n + 1)) (Fin (m + 1))) (F : ComposableArrows C m) (X : Fin (n + 1)) : ((whiskerLeftFunctor Φ).obj F).obj X = F.obj (Φ.obj X)

@[simp]

theorem CategoryTheory.ComposableArrows.whiskerLeftFunctor_obj_map {C : Type u_1} [Category.{v_1, u_1} C] {n m : ℕ} (Φ : Functor (Fin (n + 1)) (Fin (m + 1))) (F : ComposableArrows C m) {X✝ Y✝ : Fin (n + 1)} (f : X✝ ⟶ Y✝) : ((whiskerLeftFunctor Φ).obj F).map f = F.map (Φ.map f)

def Fin.succFunctor (n : ℕ) : CategoryTheory.Functor (Fin n) (Fin (n + 1))

The functor Fin n ⥤ Fin (n + 1) which sends i to i.succ.

@[simp]

theorem Fin.succFunctor_obj (n : ℕ) (i : Fin n) : (succFunctor n).obj i = i.succ

@[simp]

theorem Fin.succFunctor_map (n : ℕ) {x✝ x✝¹ : Fin n} (hij : x✝ ⟶ x✝¹) : (succFunctor n).map hij = CategoryTheory.homOfLE ⋯

def CategoryTheory.ComposableArrows.δ₀Functor {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} : Functor (ComposableArrows C (n + 1)) (ComposableArrows C n)

The functor ComposableArrows C (n + 1) ⥤ ComposableArrows C n which forgets the first arrow.

@[simp]

theorem CategoryTheory.ComposableArrows.δ₀Functor_obj_obj {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C (n + 1)) (X : Fin (n + 1)) : (δ₀Functor.obj F).obj X = F.obj X.succ

@[simp]

theorem CategoryTheory.ComposableArrows.δ₀Functor_obj_map {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C (n + 1)) {X✝ Y✝ : Fin (n + 1)} (f : X✝ ⟶ Y✝) : (δ₀Functor.obj F).map f = F.map (homOfLE ⋯)

@[simp]

theorem CategoryTheory.ComposableArrows.δ₀Functor_map_app {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {X✝ Y✝ : ComposableArrows C (n + 1)} (f : X✝ ⟶ Y✝) (X : Fin (n + 1)) : (δ₀Functor.map f).app X = f.app X.succ

@[reducible, inline]

abbrev CategoryTheory.ComposableArrows.δ₀ {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C (n + 1)) : ComposableArrows C n

The ComposableArrows C n obtained by forgetting the first arrow.

@[simp]

theorem CategoryTheory.ComposableArrows.precomp_δ₀ {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) {X : C} (f : X ⟶ F.left) : (F.precomp f).δ₀ = F

def Fin.castSuccFunctor (n : ℕ) : CategoryTheory.Functor (Fin n) (Fin (n + 1))

The functor Fin n ⥤ Fin (n + 1) which sends i to i.castSucc.

@[simp]

theorem Fin.castSuccFunctor_map (n : ℕ) {X✝ Y✝ : Fin n} (hij : X✝ ⟶ Y✝) : (castSuccFunctor n).map hij = hij

@[simp]

theorem Fin.castSuccFunctor_obj (n : ℕ) (i : Fin n) : (castSuccFunctor n).obj i = i.castSucc

def CategoryTheory.ComposableArrows.δlastFunctor {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} : Functor (ComposableArrows C (n + 1)) (ComposableArrows C n)

The functor ComposableArrows C (n + 1) ⥤ ComposableArrows C n which forgets the last arrow.

@[simp]

theorem CategoryTheory.ComposableArrows.δlastFunctor_map_app {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {X✝ Y✝ : ComposableArrows C (n + 1)} (f : X✝ ⟶ Y✝) (X : Fin (n + 1)) : (δlastFunctor.map f).app X = f.app X.castSucc

@[simp]

theorem CategoryTheory.ComposableArrows.δlastFunctor_obj_obj {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C (n + 1)) (X : Fin (n + 1)) : (δlastFunctor.obj F).obj X = F.obj X.castSucc

@[simp]

theorem CategoryTheory.ComposableArrows.δlastFunctor_obj_map {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C (n + 1)) {X✝ Y✝ : Fin (n + 1)} (f : X✝ ⟶ Y✝) : (δlastFunctor.obj F).map f = F.map f

@[reducible, inline]

abbrev CategoryTheory.ComposableArrows.δlast {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C (n + 1)) : ComposableArrows C n

The ComposableArrows C n obtained by forgetting the first arrow.

def CategoryTheory.ComposableArrows.homMkSucc {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {F G : ComposableArrows C (n + 1)} (α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯) (β : F.δ₀ ⟶ G.δ₀) (w : CategoryStruct.comp (F.map' 0 1 homMk₁._proof_4 ⋯) (app' β 0 ⋯) = CategoryStruct.comp α (G.map' 0 1 homMk₁._proof_4 ⋯)) : F ⟶ G

Inductive construction of morphisms in ComposableArrows C (n + 1): in order to construct a morphism F ⟶ G, it suffices to provide α : F.obj' 0 ⟶ G.obj' 0 and β : F.δ₀ ⟶ G.δ₀ such that F.map' 0 1 ≫ app' β 0 = α ≫ G.map' 0 1.

@[simp]

theorem CategoryTheory.ComposableArrows.homMkSucc_app_zero {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {F G : ComposableArrows C (n + 1)} (α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯) (β : F.δ₀ ⟶ G.δ₀) (w : CategoryStruct.comp (F.map' 0 1 homMk₁._proof_4 ⋯) (app' β 0 ⋯) = CategoryStruct.comp α (G.map' 0 1 homMk₁._proof_4 ⋯) := by cat_disch) : (homMkSucc α β w).app 0 = α

@[simp]

theorem CategoryTheory.ComposableArrows.homMkSucc_app_succ {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {F G : ComposableArrows C (n + 1)} (α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯) (β : F.δ₀ ⟶ G.δ₀) (w : CategoryStruct.comp (F.map' 0 1 homMk₁._proof_4 ⋯) (app' β 0 ⋯) = CategoryStruct.comp α (G.map' 0 1 homMk₁._proof_4 ⋯) := by cat_disch) (i : ℕ) (hi : i + 1 < n + 1 + 1) : (homMkSucc α β w).app ⟨i + 1, hi⟩ = app' β i ⋯

theorem CategoryTheory.ComposableArrows.hom_ext_succ {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {F G : ComposableArrows C (n + 1)} {f g : F ⟶ G} (h₀ : app' f 0 ⋯ = app' g 0 ⋯) (h₁ : δ₀Functor.map f = δ₀Functor.map g) : f = g

def CategoryTheory.ComposableArrows.isoMkSucc {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {F G : ComposableArrows C (n + 1)} (α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯) (β : F.δ₀ ≅ G.δ₀) (w : CategoryStruct.comp (F.map' 0 1 homMk₁._proof_4 ⋯) (app' β.hom 0 ⋯) = CategoryStruct.comp α.hom (G.map' 0 1 homMk₁._proof_4 ⋯)) : F ≅ G

Inductive construction of isomorphisms in ComposableArrows C (n + 1): in order to construct an isomorphism F ≅ G, it suffices to provide α : F.obj' 0 ≅ G.obj' 0 and β : F.δ₀ ≅ G.δ₀ such that F.map' 0 1 ≫ app' β.hom 0 = α.hom ≫ G.map' 0 1.

@[simp]

theorem CategoryTheory.ComposableArrows.isoMkSucc_hom {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {F G : ComposableArrows C (n + 1)} (α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯) (β : F.δ₀ ≅ G.δ₀) (w : CategoryStruct.comp (F.map' 0 1 homMk₁._proof_4 ⋯) (app' β.hom 0 ⋯) = CategoryStruct.comp α.hom (G.map' 0 1 homMk₁._proof_4 ⋯)) : (isoMkSucc α β w).hom = homMkSucc α.hom β.hom w

@[simp]

theorem CategoryTheory.ComposableArrows.isoMkSucc_inv {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {F G : ComposableArrows C (n + 1)} (α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯) (β : F.δ₀ ≅ G.δ₀) (w : CategoryStruct.comp (F.map' 0 1 homMk₁._proof_4 ⋯) (app' β.hom 0 ⋯) = CategoryStruct.comp α.hom (G.map' 0 1 homMk₁._proof_4 ⋯)) : (isoMkSucc α β w).inv = homMkSucc α.inv β.inv ⋯

theorem CategoryTheory.ComposableArrows.ext_succ {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} {F G : ComposableArrows C (n + 1)} (h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯) (h : F.δ₀ = G.δ₀) (w : F.map' 0 1 homMk₁._proof_4 ⋯ = CategoryStruct.comp (eqToHom h₀) (CategoryStruct.comp (G.map' 0 1 homMk₁._proof_4 ⋯) (eqToHom ⋯))) : F = G

theorem CategoryTheory.ComposableArrows.precomp_surjective {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C (n + 1)) : ∃ (F₀ : ComposableArrows C n) (X₀ : C) (f₀ : X₀ ⟶ F₀.left), F = F₀.precomp f₀

def CategoryTheory.ComposableArrows.homMk₂ {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 2} (app₀ : f.obj' 0 _proof_237✝ ⟶ g.obj' 0 _proof_237✝¹) (app₁ : f.obj' 1 _proof_238✝ ⟶ g.obj' 1 _proof_238✝¹) (app₂ : f.obj' 2 _proof_239✝ ⟶ g.obj' 2 _proof_239✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_238✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_238✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝⁴ _proof_239✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝⁵ _proof_239✝³) := by cat_disch) : f ⟶ g

Constructor for morphisms in ComposableArrows C 2.

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₂_app_zero {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 2} (app₀ : f.obj' 0 _proof_237✝ ⟶ g.obj' 0 _proof_237✝¹) (app₁ : f.obj' 1 _proof_238✝ ⟶ g.obj' 1 _proof_238✝¹) (app₂ : f.obj' 2 _proof_239✝ ⟶ g.obj' 2 _proof_239✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_238✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_238✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝⁴ _proof_239✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝⁵ _proof_239✝³) := by cat_disch) : (homMk₂ app₀ app₁ app₂ w₀ w₁).app 0 = app₀

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₂_app_one {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 2} (app₀ : f.obj' 0 _proof_237✝ ⟶ g.obj' 0 _proof_237✝¹) (app₁ : f.obj' 1 _proof_238✝ ⟶ g.obj' 1 _proof_238✝¹) (app₂ : f.obj' 2 _proof_239✝ ⟶ g.obj' 2 _proof_239✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_238✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_238✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝⁴ _proof_239✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝⁵ _proof_239✝³) := by cat_disch) : (homMk₂ app₀ app₁ app₂ w₀ w₁).app 1 = app₁

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₂_app_two {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 2} (app₀ : f.obj' 0 _proof_237✝ ⟶ g.obj' 0 _proof_237✝¹) (app₁ : f.obj' 1 _proof_238✝ ⟶ g.obj' 1 _proof_238✝¹) (app₂ : f.obj' 2 _proof_239✝ ⟶ g.obj' 2 _proof_239✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_238✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_238✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝⁴ _proof_239✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝⁵ _proof_239✝³) := by cat_disch) : (homMk₂ app₀ app₁ app₂ w₀ w₁).app 2 = app₂

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₂_app_two' {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 2} (app₀ : f.obj' 0 _proof_237✝ ⟶ g.obj' 0 _proof_237✝¹) (app₁ : f.obj' 1 _proof_238✝ ⟶ g.obj' 1 _proof_238✝¹) (app₂ : f.obj' 2 _proof_239✝ ⟶ g.obj' 2 _proof_239✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_238✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_238✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝⁴ _proof_239✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝⁵ _proof_239✝³) := by cat_disch) : (homMk₂ app₀ app₁ app₂ w₀ w₁).app ⟨2, homMk₂._proof_3⟩ = app₂

theorem CategoryTheory.ComposableArrows.hom_ext₂ {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 2} {φ φ' : f ⟶ g} (h₀ : app' φ 0 _proof_237✝ = app' φ' 0 _proof_237✝¹) (h₁ : app' φ 1 _proof_238✝ = app' φ' 1 _proof_238✝¹) (h₂ : app' φ 2 _proof_239✝ = app' φ' 2 _proof_239✝¹) : φ = φ'

theorem CategoryTheory.ComposableArrows.hom_ext₂_iff {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 2} {φ φ' : f ⟶ g} : φ = φ' ↔ app' φ 0 _proof_237✝ = app' φ' 0 _proof_237✝¹ ∧ app' φ 1 _proof_238✝ = app' φ' 1 _proof_238✝¹ ∧ app' φ 2 _proof_239✝ = app' φ' 2 _proof_239✝¹

def CategoryTheory.ComposableArrows.isoMk₂ {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 2} (app₀ : f.obj' 0 _proof_237✝ ≅ g.obj' 0 _proof_237✝¹) (app₁ : f.obj' 1 _proof_238✝ ≅ g.obj' 1 _proof_238✝¹) (app₂ : f.obj' 2 _proof_239✝ ≅ g.obj' 2 _proof_239✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_238✝²) app₁.hom = CategoryStruct.comp app₀.hom (g.map' 0 1 homMk₁._proof_4 _proof_238✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝⁴ _proof_239✝²) app₂.hom = CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_238✝⁵ _proof_239✝³) := by cat_disch) : f ≅ g

Constructor for isomorphisms in ComposableArrows C 2.

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₂_hom {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 2} (app₀ : f.obj' 0 _proof_237✝ ≅ g.obj' 0 _proof_237✝¹) (app₁ : f.obj' 1 _proof_238✝ ≅ g.obj' 1 _proof_238✝¹) (app₂ : f.obj' 2 _proof_239✝ ≅ g.obj' 2 _proof_239✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_238✝²) app₁.hom = CategoryStruct.comp app₀.hom (g.map' 0 1 homMk₁._proof_4 _proof_238✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝⁴ _proof_239✝²) app₂.hom = CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_238✝⁵ _proof_239✝³) := by cat_disch) : (isoMk₂ app₀ app₁ app₂ w₀ w₁).hom = homMk₂ app₀.hom app₁.hom app₂.hom w₀ w₁

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₂_inv {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 2} (app₀ : f.obj' 0 _proof_237✝ ≅ g.obj' 0 _proof_237✝¹) (app₁ : f.obj' 1 _proof_238✝ ≅ g.obj' 1 _proof_238✝¹) (app₂ : f.obj' 2 _proof_239✝ ≅ g.obj' 2 _proof_239✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_238✝²) app₁.hom = CategoryStruct.comp app₀.hom (g.map' 0 1 homMk₁._proof_4 _proof_238✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝⁴ _proof_239✝²) app₂.hom = CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_238✝⁵ _proof_239✝³) := by cat_disch) : (isoMk₂ app₀ app₁ app₂ w₀ w₁).inv = homMk₂ app₀.inv app₁.inv app₂.inv ⋯ ⋯

theorem CategoryTheory.ComposableArrows.isIso_iff₂ {C : Type u_1} [Category.{v_1, u_1} C] {F G : ComposableArrows C 2} (f : F ⟶ G) : IsIso f ↔ IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2)

theorem CategoryTheory.ComposableArrows.ext₂ {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 2} (h₀ : f.obj' 0 _proof_237✝ = g.obj' 0 _proof_237✝¹) (h₁ : f.obj' 1 _proof_238✝ = g.obj' 1 _proof_238✝¹) (h₂ : f.obj' 2 _proof_239✝ = g.obj' 2 _proof_239✝¹) (w₀ : f.map' 0 1 homMk₁._proof_4 _proof_238✝² = CategoryStruct.comp (eqToHom h₀) (CategoryStruct.comp (g.map' 0 1 homMk₁._proof_4 _proof_238✝³) (eqToHom ⋯))) (w₁ : f.map' 1 2 _proof_238✝⁴ _proof_239✝² = CategoryStruct.comp (eqToHom h₁) (CategoryStruct.comp (g.map' 1 2 _proof_238✝⁵ _proof_239✝³) (eqToHom ⋯))) : f = g

theorem CategoryTheory.ComposableArrows.mk₂_surjective {C : Type u_1} [Category.{v_1, u_1} C] (X : ComposableArrows C 2) : ∃ (X₀ : C) (X₁ : C) (X₂ : C) (f₀ : X₀ ⟶ X₁) (f₁ : X₁ ⟶ X₂), X = mk₂ f₀ f₁

theorem CategoryTheory.ComposableArrows.ext₂_of_arrow {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 2} (h₀₁ : Arrow.mk (f.map' 0 1 homMk₁._proof_4 _proof_238✝) = Arrow.mk (g.map' 0 1 homMk₁._proof_4 _proof_238✝¹)) (h₁₂ : Arrow.mk (f.map' 1 2 _proof_238✝² _proof_239✝) = Arrow.mk (g.map' 1 2 _proof_238✝³ _proof_239✝¹)) : f = g

def CategoryTheory.ComposableArrows.homMk₃ {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 3} (app₀ : f.obj' 0 _proof_289✝ ⟶ g.obj' 0 _proof_289✝¹) (app₁ : f.obj' 1 _proof_290✝ ⟶ g.obj' 1 _proof_290✝¹) (app₂ : f.obj' 2 _proof_291✝ ⟶ g.obj' 2 _proof_291✝¹) (app₃ : f.obj' 3 _proof_292✝ ⟶ g.obj' 3 _proof_292✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_290✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_290✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_291✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_291✝³) := by cat_disch) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝⁴ _proof_292✝²) app₃ = CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝⁵ _proof_292✝³) := by cat_disch) : f ⟶ g

Constructor for morphisms in ComposableArrows C 3.

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₃_app_zero {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 3} (app₀ : f.obj' 0 _proof_289✝ ⟶ g.obj' 0 _proof_289✝¹) (app₁ : f.obj' 1 _proof_290✝ ⟶ g.obj' 1 _proof_290✝¹) (app₂ : f.obj' 2 _proof_291✝ ⟶ g.obj' 2 _proof_291✝¹) (app₃ : f.obj' 3 _proof_292✝ ⟶ g.obj' 3 _proof_292✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_290✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_290✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_291✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_291✝³) := by cat_disch) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝⁴ _proof_292✝²) app₃ = CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝⁵ _proof_292✝³) := by cat_disch) : (homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app 0 = app₀

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₃_app_one {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 3} (app₀ : f.obj' 0 _proof_289✝ ⟶ g.obj' 0 _proof_289✝¹) (app₁ : f.obj' 1 _proof_290✝ ⟶ g.obj' 1 _proof_290✝¹) (app₂ : f.obj' 2 _proof_291✝ ⟶ g.obj' 2 _proof_291✝¹) (app₃ : f.obj' 3 _proof_292✝ ⟶ g.obj' 3 _proof_292✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_290✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_290✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_291✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_291✝³) := by cat_disch) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝⁴ _proof_292✝²) app₃ = CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝⁵ _proof_292✝³) := by cat_disch) : (homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app 1 = app₁

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₃_app_two {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 3} (app₀ : f.obj' 0 _proof_289✝ ⟶ g.obj' 0 _proof_289✝¹) (app₁ : f.obj' 1 _proof_290✝ ⟶ g.obj' 1 _proof_290✝¹) (app₂ : f.obj' 2 _proof_291✝ ⟶ g.obj' 2 _proof_291✝¹) (app₃ : f.obj' 3 _proof_292✝ ⟶ g.obj' 3 _proof_292✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_290✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_290✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_291✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_291✝³) := by cat_disch) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝⁴ _proof_292✝²) app₃ = CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝⁵ _proof_292✝³) := by cat_disch) : (homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app ⟨2, homMk₃._proof_3⟩ = app₂

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₃_app_three {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 3} (app₀ : f.obj' 0 _proof_289✝ ⟶ g.obj' 0 _proof_289✝¹) (app₁ : f.obj' 1 _proof_290✝ ⟶ g.obj' 1 _proof_290✝¹) (app₂ : f.obj' 2 _proof_291✝ ⟶ g.obj' 2 _proof_291✝¹) (app₃ : f.obj' 3 _proof_292✝ ⟶ g.obj' 3 _proof_292✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_290✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_290✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_291✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_291✝³) := by cat_disch) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝⁴ _proof_292✝²) app₃ = CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝⁵ _proof_292✝³) := by cat_disch) : (homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app ⟨3, homMk₃._proof_4⟩ = app₃

theorem CategoryTheory.ComposableArrows.hom_ext₃ {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 3} {φ φ' : f ⟶ g} (h₀ : app' φ 0 _proof_289✝ = app' φ' 0 _proof_289✝¹) (h₁ : app' φ 1 _proof_290✝ = app' φ' 1 _proof_290✝¹) (h₂ : app' φ 2 _proof_291✝ = app' φ' 2 _proof_291✝¹) (h₃ : app' φ 3 _proof_292✝ = app' φ' 3 _proof_292✝¹) : φ = φ'

theorem CategoryTheory.ComposableArrows.hom_ext₃_iff {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 3} {φ φ' : f ⟶ g} : φ = φ' ↔ app' φ 0 _proof_289✝ = app' φ' 0 _proof_289✝¹ ∧ app' φ 1 _proof_290✝ = app' φ' 1 _proof_290✝¹ ∧ app' φ 2 _proof_291✝ = app' φ' 2 _proof_291✝¹ ∧ app' φ 3 _proof_292✝ = app' φ' 3 _proof_292✝¹

def CategoryTheory.ComposableArrows.isoMk₃ {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 3} (app₀ : f.obj' 0 _proof_289✝ ≅ g.obj' 0 _proof_289✝¹) (app₁ : f.obj' 1 _proof_290✝ ≅ g.obj' 1 _proof_290✝¹) (app₂ : f.obj' 2 _proof_291✝ ≅ g.obj' 2 _proof_291✝¹) (app₃ : f.obj' 3 _proof_292✝ ≅ g.obj' 3 _proof_292✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_290✝²) app₁.hom = CategoryStruct.comp app₀.hom (g.map' 0 1 homMk₁._proof_4 _proof_290✝³)) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_291✝²) app₂.hom = CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_238✝¹ _proof_291✝³)) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝⁴ _proof_292✝²) app₃.hom = CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_291✝⁵ _proof_292✝³)) : f ≅ g

Constructor for isomorphisms in ComposableArrows C 3.

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₃_inv {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 3} (app₀ : f.obj' 0 _proof_289✝ ≅ g.obj' 0 _proof_289✝¹) (app₁ : f.obj' 1 _proof_290✝ ≅ g.obj' 1 _proof_290✝¹) (app₂ : f.obj' 2 _proof_291✝ ≅ g.obj' 2 _proof_291✝¹) (app₃ : f.obj' 3 _proof_292✝ ≅ g.obj' 3 _proof_292✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_290✝²) app₁.hom = CategoryStruct.comp app₀.hom (g.map' 0 1 homMk₁._proof_4 _proof_290✝³)) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_291✝²) app₂.hom = CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_238✝¹ _proof_291✝³)) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝⁴ _proof_292✝²) app₃.hom = CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_291✝⁵ _proof_292✝³)) : (isoMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).inv = homMk₃ app₀.inv app₁.inv app₂.inv app₃.inv ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₃_hom {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 3} (app₀ : f.obj' 0 _proof_289✝ ≅ g.obj' 0 _proof_289✝¹) (app₁ : f.obj' 1 _proof_290✝ ≅ g.obj' 1 _proof_290✝¹) (app₂ : f.obj' 2 _proof_291✝ ≅ g.obj' 2 _proof_291✝¹) (app₃ : f.obj' 3 _proof_292✝ ≅ g.obj' 3 _proof_292✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_290✝²) app₁.hom = CategoryStruct.comp app₀.hom (g.map' 0 1 homMk₁._proof_4 _proof_290✝³)) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_291✝²) app₂.hom = CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_238✝¹ _proof_291✝³)) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝⁴ _proof_292✝²) app₃.hom = CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_291✝⁵ _proof_292✝³)) : (isoMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).hom = homMk₃ app₀.hom app₁.hom app₂.hom app₃.hom w₀ w₁ w₂

theorem CategoryTheory.ComposableArrows.ext₃ {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 3} (h₀ : f.obj' 0 _proof_289✝ = g.obj' 0 _proof_289✝¹) (h₁ : f.obj' 1 _proof_290✝ = g.obj' 1 _proof_290✝¹) (h₂ : f.obj' 2 _proof_291✝ = g.obj' 2 _proof_291✝¹) (h₃ : f.obj' 3 _proof_292✝ = g.obj' 3 _proof_292✝¹) (w₀ : f.map' 0 1 homMk₁._proof_4 _proof_290✝² = CategoryStruct.comp (eqToHom h₀) (CategoryStruct.comp (g.map' 0 1 homMk₁._proof_4 _proof_290✝³) (eqToHom ⋯))) (w₁ : f.map' 1 2 _proof_238✝ _proof_291✝² = CategoryStruct.comp (eqToHom h₁) (CategoryStruct.comp (g.map' 1 2 _proof_238✝¹ _proof_291✝³) (eqToHom ⋯))) (w₂ : f.map' 2 3 _proof_291✝⁴ _proof_292✝² = CategoryStruct.comp (eqToHom h₂) (CategoryStruct.comp (g.map' 2 3 _proof_291✝⁵ _proof_292✝³) (eqToHom ⋯))) : f = g

theorem CategoryTheory.ComposableArrows.mk₃_surjective {C : Type u_1} [Category.{v_1, u_1} C] (X : ComposableArrows C 3) : ∃ (X₀ : C) (X₁ : C) (X₂ : C) (X₃ : C) (f₀ : X₀ ⟶ X₁) (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃), X = mk₃ f₀ f₁ f₂

def CategoryTheory.ComposableArrows.homMk₄ {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 4} (app₀ : f.obj' 0 _proof_353✝ ⟶ g.obj' 0 _proof_353✝¹) (app₁ : f.obj' 1 _proof_354✝ ⟶ g.obj' 1 _proof_354✝¹) (app₂ : f.obj' 2 _proof_355✝ ⟶ g.obj' 2 _proof_355✝¹) (app₃ : f.obj' 3 _proof_356✝ ⟶ g.obj' 3 _proof_356✝¹) (app₄ : f.obj' 4 _proof_357✝ ⟶ g.obj' 4 _proof_357✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_354✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_354✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_355✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_355✝³) := by cat_disch) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_356✝²) app₃ = CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝¹ _proof_356✝³) := by cat_disch) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝⁴ _proof_357✝²) app₄ = CategoryStruct.comp app₃ (g.map' 3 4 _proof_356✝⁵ _proof_357✝³) := by cat_disch) : f ⟶ g

Constructor for morphisms in ComposableArrows C 4.

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₄_app_zero {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 4} (app₀ : f.obj' 0 _proof_353✝ ⟶ g.obj' 0 _proof_353✝¹) (app₁ : f.obj' 1 _proof_354✝ ⟶ g.obj' 1 _proof_354✝¹) (app₂ : f.obj' 2 _proof_355✝ ⟶ g.obj' 2 _proof_355✝¹) (app₃ : f.obj' 3 _proof_356✝ ⟶ g.obj' 3 _proof_356✝¹) (app₄ : f.obj' 4 _proof_357✝ ⟶ g.obj' 4 _proof_357✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_354✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_354✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_355✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_355✝³) := by cat_disch) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_356✝²) app₃ = CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝¹ _proof_356✝³) := by cat_disch) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝⁴ _proof_357✝²) app₄ = CategoryStruct.comp app₃ (g.map' 3 4 _proof_356✝⁵ _proof_357✝³) := by cat_disch) : (homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app 0 = app₀

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₄_app_one {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 4} (app₀ : f.obj' 0 _proof_353✝ ⟶ g.obj' 0 _proof_353✝¹) (app₁ : f.obj' 1 _proof_354✝ ⟶ g.obj' 1 _proof_354✝¹) (app₂ : f.obj' 2 _proof_355✝ ⟶ g.obj' 2 _proof_355✝¹) (app₃ : f.obj' 3 _proof_356✝ ⟶ g.obj' 3 _proof_356✝¹) (app₄ : f.obj' 4 _proof_357✝ ⟶ g.obj' 4 _proof_357✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_354✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_354✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_355✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_355✝³) := by cat_disch) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_356✝²) app₃ = CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝¹ _proof_356✝³) := by cat_disch) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝⁴ _proof_357✝²) app₄ = CategoryStruct.comp app₃ (g.map' 3 4 _proof_356✝⁵ _proof_357✝³) := by cat_disch) : (homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app 1 = app₁

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₄_app_two {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 4} (app₀ : f.obj' 0 _proof_353✝ ⟶ g.obj' 0 _proof_353✝¹) (app₁ : f.obj' 1 _proof_354✝ ⟶ g.obj' 1 _proof_354✝¹) (app₂ : f.obj' 2 _proof_355✝ ⟶ g.obj' 2 _proof_355✝¹) (app₃ : f.obj' 3 _proof_356✝ ⟶ g.obj' 3 _proof_356✝¹) (app₄ : f.obj' 4 _proof_357✝ ⟶ g.obj' 4 _proof_357✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_354✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_354✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_355✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_355✝³) := by cat_disch) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_356✝²) app₃ = CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝¹ _proof_356✝³) := by cat_disch) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝⁴ _proof_357✝²) app₄ = CategoryStruct.comp app₃ (g.map' 3 4 _proof_356✝⁵ _proof_357✝³) := by cat_disch) : (homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app ⟨2, homMk₄._proof_3⟩ = app₂

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₄_app_three {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 4} (app₀ : f.obj' 0 _proof_353✝ ⟶ g.obj' 0 _proof_353✝¹) (app₁ : f.obj' 1 _proof_354✝ ⟶ g.obj' 1 _proof_354✝¹) (app₂ : f.obj' 2 _proof_355✝ ⟶ g.obj' 2 _proof_355✝¹) (app₃ : f.obj' 3 _proof_356✝ ⟶ g.obj' 3 _proof_356✝¹) (app₄ : f.obj' 4 _proof_357✝ ⟶ g.obj' 4 _proof_357✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_354✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_354✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_355✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_355✝³) := by cat_disch) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_356✝²) app₃ = CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝¹ _proof_356✝³) := by cat_disch) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝⁴ _proof_357✝²) app₄ = CategoryStruct.comp app₃ (g.map' 3 4 _proof_356✝⁵ _proof_357✝³) := by cat_disch) : (homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app ⟨3, homMk₄._proof_4⟩ = app₃

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₄_app_four {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 4} (app₀ : f.obj' 0 _proof_353✝ ⟶ g.obj' 0 _proof_353✝¹) (app₁ : f.obj' 1 _proof_354✝ ⟶ g.obj' 1 _proof_354✝¹) (app₂ : f.obj' 2 _proof_355✝ ⟶ g.obj' 2 _proof_355✝¹) (app₃ : f.obj' 3 _proof_356✝ ⟶ g.obj' 3 _proof_356✝¹) (app₄ : f.obj' 4 _proof_357✝ ⟶ g.obj' 4 _proof_357✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_354✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_354✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_355✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_355✝³) := by cat_disch) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_356✝²) app₃ = CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝¹ _proof_356✝³) := by cat_disch) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝⁴ _proof_357✝²) app₄ = CategoryStruct.comp app₃ (g.map' 3 4 _proof_356✝⁵ _proof_357✝³) := by cat_disch) : (homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app ⟨4, homMk₄._proof_5⟩ = app₄

theorem CategoryTheory.ComposableArrows.hom_ext₄ {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 4} {φ φ' : f ⟶ g} (h₀ : app' φ 0 _proof_353✝ = app' φ' 0 _proof_353✝¹) (h₁ : app' φ 1 _proof_354✝ = app' φ' 1 _proof_354✝¹) (h₂ : app' φ 2 _proof_355✝ = app' φ' 2 _proof_355✝¹) (h₃ : app' φ 3 _proof_356✝ = app' φ' 3 _proof_356✝¹) (h₄ : app' φ 4 _proof_357✝ = app' φ' 4 _proof_357✝¹) : φ = φ'

theorem CategoryTheory.ComposableArrows.hom_ext₄_iff {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 4} {φ φ' : f ⟶ g} : φ = φ' ↔ app' φ 0 _proof_353✝ = app' φ' 0 _proof_353✝¹ ∧ app' φ 1 _proof_354✝ = app' φ' 1 _proof_354✝¹ ∧ app' φ 2 _proof_355✝ = app' φ' 2 _proof_355✝¹ ∧ app' φ 3 _proof_356✝ = app' φ' 3 _proof_356✝¹ ∧ app' φ 4 _proof_357✝ = app' φ' 4 _proof_357✝¹

theorem CategoryTheory.ComposableArrows.map'_inv_eq_inv_map' {C : Type u_1} [Category.{v_1, u_1} C] {n m : ℕ} (h : n + 1 ≤ m) {f g : ComposableArrows C m} (app : f.obj' n ⋯ ≅ g.obj' n ⋯) (app' : f.obj' (n + 1) h ≅ g.obj' (n + 1) h) (w : CategoryStruct.comp (f.map' n (n + 1) ⋯ h) app'.hom = CategoryStruct.comp app.hom (g.map' n (n + 1) ⋯ h)) : CategoryStruct.comp (g.map' n (n + 1) ⋯ h) app'.inv = CategoryStruct.comp app.inv (f.map' n (n + 1) ⋯ h)

def CategoryTheory.ComposableArrows.isoMk₄ {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 4} (app₀ : f.obj' 0 _proof_353✝ ≅ g.obj' 0 _proof_353✝¹) (app₁ : f.obj' 1 _proof_354✝ ≅ g.obj' 1 _proof_354✝¹) (app₂ : f.obj' 2 _proof_355✝ ≅ g.obj' 2 _proof_355✝¹) (app₃ : f.obj' 3 _proof_356✝ ≅ g.obj' 3 _proof_356✝¹) (app₄ : f.obj' 4 _proof_357✝ ≅ g.obj' 4 _proof_357✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_354✝²) app₁.hom = CategoryStruct.comp app₀.hom (g.map' 0 1 homMk₁._proof_4 _proof_354✝³)) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_355✝²) app₂.hom = CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_238✝¹ _proof_355✝³)) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_356✝²) app₃.hom = CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_291✝¹ _proof_356✝³)) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝⁴ _proof_357✝²) app₄.hom = CategoryStruct.comp app₃.hom (g.map' 3 4 _proof_356✝⁵ _proof_357✝³)) : f ≅ g

Constructor for isomorphisms in ComposableArrows C 4.

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₄_hom {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 4} (app₀ : f.obj' 0 _proof_353✝ ≅ g.obj' 0 _proof_353✝¹) (app₁ : f.obj' 1 _proof_354✝ ≅ g.obj' 1 _proof_354✝¹) (app₂ : f.obj' 2 _proof_355✝ ≅ g.obj' 2 _proof_355✝¹) (app₃ : f.obj' 3 _proof_356✝ ≅ g.obj' 3 _proof_356✝¹) (app₄ : f.obj' 4 _proof_357✝ ≅ g.obj' 4 _proof_357✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_354✝²) app₁.hom = CategoryStruct.comp app₀.hom (g.map' 0 1 homMk₁._proof_4 _proof_354✝³)) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_355✝²) app₂.hom = CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_238✝¹ _proof_355✝³)) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_356✝²) app₃.hom = CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_291✝¹ _proof_356✝³)) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝⁴ _proof_357✝²) app₄.hom = CategoryStruct.comp app₃.hom (g.map' 3 4 _proof_356✝⁵ _proof_357✝³)) : (isoMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).hom = homMk₄ app₀.hom app₁.hom app₂.hom app₃.hom app₄.hom w₀ w₁ w₂ w₃

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₄_inv {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 4} (app₀ : f.obj' 0 _proof_353✝ ≅ g.obj' 0 _proof_353✝¹) (app₁ : f.obj' 1 _proof_354✝ ≅ g.obj' 1 _proof_354✝¹) (app₂ : f.obj' 2 _proof_355✝ ≅ g.obj' 2 _proof_355✝¹) (app₃ : f.obj' 3 _proof_356✝ ≅ g.obj' 3 _proof_356✝¹) (app₄ : f.obj' 4 _proof_357✝ ≅ g.obj' 4 _proof_357✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_354✝²) app₁.hom = CategoryStruct.comp app₀.hom (g.map' 0 1 homMk₁._proof_4 _proof_354✝³)) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_355✝²) app₂.hom = CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_238✝¹ _proof_355✝³)) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_356✝²) app₃.hom = CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_291✝¹ _proof_356✝³)) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝⁴ _proof_357✝²) app₄.hom = CategoryStruct.comp app₃.hom (g.map' 3 4 _proof_356✝⁵ _proof_357✝³)) : (isoMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).inv = homMk₄ app₀.inv app₁.inv app₂.inv app₃.inv app₄.inv ⋯ ⋯ ⋯ ⋯

theorem CategoryTheory.ComposableArrows.ext₄ {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 4} (h₀ : f.obj' 0 _proof_353✝ = g.obj' 0 _proof_353✝¹) (h₁ : f.obj' 1 _proof_354✝ = g.obj' 1 _proof_354✝¹) (h₂ : f.obj' 2 _proof_355✝ = g.obj' 2 _proof_355✝¹) (h₃ : f.obj' 3 _proof_356✝ = g.obj' 3 _proof_356✝¹) (h₄ : f.obj' 4 _proof_357✝ = g.obj' 4 _proof_357✝¹) (w₀ : f.map' 0 1 homMk₁._proof_4 _proof_354✝² = CategoryStruct.comp (eqToHom h₀) (CategoryStruct.comp (g.map' 0 1 homMk₁._proof_4 _proof_354✝³) (eqToHom ⋯))) (w₁ : f.map' 1 2 _proof_238✝ _proof_355✝² = CategoryStruct.comp (eqToHom h₁) (CategoryStruct.comp (g.map' 1 2 _proof_238✝¹ _proof_355✝³) (eqToHom ⋯))) (w₂ : f.map' 2 3 _proof_291✝ _proof_356✝² = CategoryStruct.comp (eqToHom h₂) (CategoryStruct.comp (g.map' 2 3 _proof_291✝¹ _proof_356✝³) (eqToHom ⋯))) (w₃ : f.map' 3 4 _proof_356✝⁴ _proof_357✝² = CategoryStruct.comp (eqToHom h₃) (CategoryStruct.comp (g.map' 3 4 _proof_356✝⁵ _proof_357✝³) (eqToHom ⋯))) : f = g

theorem CategoryTheory.ComposableArrows.mk₄_surjective {C : Type u_1} [Category.{v_1, u_1} C] (X : ComposableArrows C 4) : ∃ (X₀ : C) (X₁ : C) (X₂ : C) (X₃ : C) (X₄ : C) (f₀ : X₀ ⟶ X₁) (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (f₃ : X₃ ⟶ X₄), X = mk₄ f₀ f₁ f₂ f₃

def CategoryTheory.ComposableArrows.homMk₅ {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 5} (app₀ : f.obj' 0 _proof_441✝ ⟶ g.obj' 0 _proof_441✝¹) (app₁ : f.obj' 1 _proof_442✝ ⟶ g.obj' 1 _proof_442✝¹) (app₂ : f.obj' 2 _proof_443✝ ⟶ g.obj' 2 _proof_443✝¹) (app₃ : f.obj' 3 _proof_444✝ ⟶ g.obj' 3 _proof_444✝¹) (app₄ : f.obj' 4 _proof_445✝ ⟶ g.obj' 4 _proof_445✝¹) (app₅ : f.obj' 5 _proof_446✝ ⟶ g.obj' 5 _proof_446✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_442✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_442✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_443✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_443✝³) := by cat_disch) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_444✝²) app₃ = CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝¹ _proof_444✝³) := by cat_disch) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝ _proof_445✝²) app₄ = CategoryStruct.comp app₃ (g.map' 3 4 _proof_356✝¹ _proof_445✝³) := by cat_disch) (w₄ : CategoryStruct.comp (f.map' 4 5 _proof_445✝⁴ _proof_446✝²) app₅ = CategoryStruct.comp app₄ (g.map' 4 5 _proof_445✝⁵ _proof_446✝³) := by cat_disch) : f ⟶ g

Constructor for morphisms in ComposableArrows C 5.

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₅_app_zero {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 5} (app₀ : f.obj' 0 _proof_441✝ ⟶ g.obj' 0 _proof_441✝¹) (app₁ : f.obj' 1 _proof_442✝ ⟶ g.obj' 1 _proof_442✝¹) (app₂ : f.obj' 2 _proof_443✝ ⟶ g.obj' 2 _proof_443✝¹) (app₃ : f.obj' 3 _proof_444✝ ⟶ g.obj' 3 _proof_444✝¹) (app₄ : f.obj' 4 _proof_445✝ ⟶ g.obj' 4 _proof_445✝¹) (app₅ : f.obj' 5 _proof_446✝ ⟶ g.obj' 5 _proof_446✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_442✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_442✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_443✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_443✝³) := by cat_disch) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_444✝²) app₃ = CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝¹ _proof_444✝³) := by cat_disch) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝ _proof_445✝²) app₄ = CategoryStruct.comp app₃ (g.map' 3 4 _proof_356✝¹ _proof_445✝³) := by cat_disch) (w₄ : CategoryStruct.comp (f.map' 4 5 _proof_445✝⁴ _proof_446✝²) app₅ = CategoryStruct.comp app₄ (g.map' 4 5 _proof_445✝⁵ _proof_446✝³) := by cat_disch) : (homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app 0 = app₀

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₅_app_one {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 5} (app₀ : f.obj' 0 _proof_441✝ ⟶ g.obj' 0 _proof_441✝¹) (app₁ : f.obj' 1 _proof_442✝ ⟶ g.obj' 1 _proof_442✝¹) (app₂ : f.obj' 2 _proof_443✝ ⟶ g.obj' 2 _proof_443✝¹) (app₃ : f.obj' 3 _proof_444✝ ⟶ g.obj' 3 _proof_444✝¹) (app₄ : f.obj' 4 _proof_445✝ ⟶ g.obj' 4 _proof_445✝¹) (app₅ : f.obj' 5 _proof_446✝ ⟶ g.obj' 5 _proof_446✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_442✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_442✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_443✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_443✝³) := by cat_disch) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_444✝²) app₃ = CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝¹ _proof_444✝³) := by cat_disch) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝ _proof_445✝²) app₄ = CategoryStruct.comp app₃ (g.map' 3 4 _proof_356✝¹ _proof_445✝³) := by cat_disch) (w₄ : CategoryStruct.comp (f.map' 4 5 _proof_445✝⁴ _proof_446✝²) app₅ = CategoryStruct.comp app₄ (g.map' 4 5 _proof_445✝⁵ _proof_446✝³) := by cat_disch) : (homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app 1 = app₁

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₅_app_two {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 5} (app₀ : f.obj' 0 _proof_441✝ ⟶ g.obj' 0 _proof_441✝¹) (app₁ : f.obj' 1 _proof_442✝ ⟶ g.obj' 1 _proof_442✝¹) (app₂ : f.obj' 2 _proof_443✝ ⟶ g.obj' 2 _proof_443✝¹) (app₃ : f.obj' 3 _proof_444✝ ⟶ g.obj' 3 _proof_444✝¹) (app₄ : f.obj' 4 _proof_445✝ ⟶ g.obj' 4 _proof_445✝¹) (app₅ : f.obj' 5 _proof_446✝ ⟶ g.obj' 5 _proof_446✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_442✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_442✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_443✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_443✝³) := by cat_disch) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_444✝²) app₃ = CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝¹ _proof_444✝³) := by cat_disch) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝ _proof_445✝²) app₄ = CategoryStruct.comp app₃ (g.map' 3 4 _proof_356✝¹ _proof_445✝³) := by cat_disch) (w₄ : CategoryStruct.comp (f.map' 4 5 _proof_445✝⁴ _proof_446✝²) app₅ = CategoryStruct.comp app₄ (g.map' 4 5 _proof_445✝⁵ _proof_446✝³) := by cat_disch) : (homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨2, homMk₅._proof_3⟩ = app₂

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₅_app_three {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 5} (app₀ : f.obj' 0 _proof_441✝ ⟶ g.obj' 0 _proof_441✝¹) (app₁ : f.obj' 1 _proof_442✝ ⟶ g.obj' 1 _proof_442✝¹) (app₂ : f.obj' 2 _proof_443✝ ⟶ g.obj' 2 _proof_443✝¹) (app₃ : f.obj' 3 _proof_444✝ ⟶ g.obj' 3 _proof_444✝¹) (app₄ : f.obj' 4 _proof_445✝ ⟶ g.obj' 4 _proof_445✝¹) (app₅ : f.obj' 5 _proof_446✝ ⟶ g.obj' 5 _proof_446✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_442✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_442✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_443✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_443✝³) := by cat_disch) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_444✝²) app₃ = CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝¹ _proof_444✝³) := by cat_disch) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝ _proof_445✝²) app₄ = CategoryStruct.comp app₃ (g.map' 3 4 _proof_356✝¹ _proof_445✝³) := by cat_disch) (w₄ : CategoryStruct.comp (f.map' 4 5 _proof_445✝⁴ _proof_446✝²) app₅ = CategoryStruct.comp app₄ (g.map' 4 5 _proof_445✝⁵ _proof_446✝³) := by cat_disch) : (homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨3, homMk₅._proof_4⟩ = app₃

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₅_app_four {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 5} (app₀ : f.obj' 0 _proof_441✝ ⟶ g.obj' 0 _proof_441✝¹) (app₁ : f.obj' 1 _proof_442✝ ⟶ g.obj' 1 _proof_442✝¹) (app₂ : f.obj' 2 _proof_443✝ ⟶ g.obj' 2 _proof_443✝¹) (app₃ : f.obj' 3 _proof_444✝ ⟶ g.obj' 3 _proof_444✝¹) (app₄ : f.obj' 4 _proof_445✝ ⟶ g.obj' 4 _proof_445✝¹) (app₅ : f.obj' 5 _proof_446✝ ⟶ g.obj' 5 _proof_446✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_442✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_442✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_443✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_443✝³) := by cat_disch) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_444✝²) app₃ = CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝¹ _proof_444✝³) := by cat_disch) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝ _proof_445✝²) app₄ = CategoryStruct.comp app₃ (g.map' 3 4 _proof_356✝¹ _proof_445✝³) := by cat_disch) (w₄ : CategoryStruct.comp (f.map' 4 5 _proof_445✝⁴ _proof_446✝²) app₅ = CategoryStruct.comp app₄ (g.map' 4 5 _proof_445✝⁵ _proof_446✝³) := by cat_disch) : (homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨4, homMk₅._proof_5⟩ = app₄

@[simp]

theorem CategoryTheory.ComposableArrows.homMk₅_app_five {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 5} (app₀ : f.obj' 0 _proof_441✝ ⟶ g.obj' 0 _proof_441✝¹) (app₁ : f.obj' 1 _proof_442✝ ⟶ g.obj' 1 _proof_442✝¹) (app₂ : f.obj' 2 _proof_443✝ ⟶ g.obj' 2 _proof_443✝¹) (app₃ : f.obj' 3 _proof_444✝ ⟶ g.obj' 3 _proof_444✝¹) (app₄ : f.obj' 4 _proof_445✝ ⟶ g.obj' 4 _proof_445✝¹) (app₅ : f.obj' 5 _proof_446✝ ⟶ g.obj' 5 _proof_446✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_442✝²) app₁ = CategoryStruct.comp app₀ (g.map' 0 1 homMk₁._proof_4 _proof_442✝³) := by cat_disch) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_443✝²) app₂ = CategoryStruct.comp app₁ (g.map' 1 2 _proof_238✝¹ _proof_443✝³) := by cat_disch) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_444✝²) app₃ = CategoryStruct.comp app₂ (g.map' 2 3 _proof_291✝¹ _proof_444✝³) := by cat_disch) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝ _proof_445✝²) app₄ = CategoryStruct.comp app₃ (g.map' 3 4 _proof_356✝¹ _proof_445✝³) := by cat_disch) (w₄ : CategoryStruct.comp (f.map' 4 5 _proof_445✝⁴ _proof_446✝²) app₅ = CategoryStruct.comp app₄ (g.map' 4 5 _proof_445✝⁵ _proof_446✝³) := by cat_disch) : (homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨5, homMk₅._proof_6⟩ = app₅

theorem CategoryTheory.ComposableArrows.hom_ext₅ {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 5} {φ φ' : f ⟶ g} (h₀ : app' φ 0 _proof_441✝ = app' φ' 0 _proof_441✝¹) (h₁ : app' φ 1 _proof_442✝ = app' φ' 1 _proof_442✝¹) (h₂ : app' φ 2 _proof_443✝ = app' φ' 2 _proof_443✝¹) (h₃ : app' φ 3 _proof_444✝ = app' φ' 3 _proof_444✝¹) (h₄ : app' φ 4 _proof_445✝ = app' φ' 4 _proof_445✝¹) (h₅ : app' φ 5 _proof_446✝ = app' φ' 5 _proof_446✝¹) : φ = φ'

theorem CategoryTheory.ComposableArrows.hom_ext₅_iff {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 5} {φ φ' : f ⟶ g} : φ = φ' ↔ app' φ 0 _proof_441✝ = app' φ' 0 _proof_441✝¹ ∧ app' φ 1 _proof_442✝ = app' φ' 1 _proof_442✝¹ ∧ app' φ 2 _proof_443✝ = app' φ' 2 _proof_443✝¹ ∧ app' φ 3 _proof_444✝ = app' φ' 3 _proof_444✝¹ ∧ app' φ 4 _proof_445✝ = app' φ' 4 _proof_445✝¹ ∧ app' φ 5 _proof_446✝ = app' φ' 5 _proof_446✝¹

def CategoryTheory.ComposableArrows.isoMk₅ {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 5} (app₀ : f.obj' 0 _proof_441✝ ≅ g.obj' 0 _proof_441✝¹) (app₁ : f.obj' 1 _proof_442✝ ≅ g.obj' 1 _proof_442✝¹) (app₂ : f.obj' 2 _proof_443✝ ≅ g.obj' 2 _proof_443✝¹) (app₃ : f.obj' 3 _proof_444✝ ≅ g.obj' 3 _proof_444✝¹) (app₄ : f.obj' 4 _proof_445✝ ≅ g.obj' 4 _proof_445✝¹) (app₅ : f.obj' 5 _proof_446✝ ≅ g.obj' 5 _proof_446✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_442✝²) app₁.hom = CategoryStruct.comp app₀.hom (g.map' 0 1 homMk₁._proof_4 _proof_442✝³)) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_443✝²) app₂.hom = CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_238✝¹ _proof_443✝³)) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_444✝²) app₃.hom = CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_291✝¹ _proof_444✝³)) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝ _proof_445✝²) app₄.hom = CategoryStruct.comp app₃.hom (g.map' 3 4 _proof_356✝¹ _proof_445✝³)) (w₄ : CategoryStruct.comp (f.map' 4 5 _proof_445✝⁴ _proof_446✝²) app₅.hom = CategoryStruct.comp app₄.hom (g.map' 4 5 _proof_445✝⁵ _proof_446✝³)) : f ≅ g

Constructor for isomorphisms in ComposableArrows C 5.

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₅_hom {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 5} (app₀ : f.obj' 0 _proof_441✝ ≅ g.obj' 0 _proof_441✝¹) (app₁ : f.obj' 1 _proof_442✝ ≅ g.obj' 1 _proof_442✝¹) (app₂ : f.obj' 2 _proof_443✝ ≅ g.obj' 2 _proof_443✝¹) (app₃ : f.obj' 3 _proof_444✝ ≅ g.obj' 3 _proof_444✝¹) (app₄ : f.obj' 4 _proof_445✝ ≅ g.obj' 4 _proof_445✝¹) (app₅ : f.obj' 5 _proof_446✝ ≅ g.obj' 5 _proof_446✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_442✝²) app₁.hom = CategoryStruct.comp app₀.hom (g.map' 0 1 homMk₁._proof_4 _proof_442✝³)) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_443✝²) app₂.hom = CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_238✝¹ _proof_443✝³)) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_444✝²) app₃.hom = CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_291✝¹ _proof_444✝³)) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝ _proof_445✝²) app₄.hom = CategoryStruct.comp app₃.hom (g.map' 3 4 _proof_356✝¹ _proof_445✝³)) (w₄ : CategoryStruct.comp (f.map' 4 5 _proof_445✝⁴ _proof_446✝²) app₅.hom = CategoryStruct.comp app₄.hom (g.map' 4 5 _proof_445✝⁵ _proof_446✝³)) : (isoMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).hom = homMk₅ app₀.hom app₁.hom app₂.hom app₃.hom app₄.hom app₅.hom w₀ w₁ w₂ w₃ w₄

@[simp]

theorem CategoryTheory.ComposableArrows.isoMk₅_inv {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 5} (app₀ : f.obj' 0 _proof_441✝ ≅ g.obj' 0 _proof_441✝¹) (app₁ : f.obj' 1 _proof_442✝ ≅ g.obj' 1 _proof_442✝¹) (app₂ : f.obj' 2 _proof_443✝ ≅ g.obj' 2 _proof_443✝¹) (app₃ : f.obj' 3 _proof_444✝ ≅ g.obj' 3 _proof_444✝¹) (app₄ : f.obj' 4 _proof_445✝ ≅ g.obj' 4 _proof_445✝¹) (app₅ : f.obj' 5 _proof_446✝ ≅ g.obj' 5 _proof_446✝¹) (w₀ : CategoryStruct.comp (f.map' 0 1 homMk₁._proof_4 _proof_442✝²) app₁.hom = CategoryStruct.comp app₀.hom (g.map' 0 1 homMk₁._proof_4 _proof_442✝³)) (w₁ : CategoryStruct.comp (f.map' 1 2 _proof_238✝ _proof_443✝²) app₂.hom = CategoryStruct.comp app₁.hom (g.map' 1 2 _proof_238✝¹ _proof_443✝³)) (w₂ : CategoryStruct.comp (f.map' 2 3 _proof_291✝ _proof_444✝²) app₃.hom = CategoryStruct.comp app₂.hom (g.map' 2 3 _proof_291✝¹ _proof_444✝³)) (w₃ : CategoryStruct.comp (f.map' 3 4 _proof_356✝ _proof_445✝²) app₄.hom = CategoryStruct.comp app₃.hom (g.map' 3 4 _proof_356✝¹ _proof_445✝³)) (w₄ : CategoryStruct.comp (f.map' 4 5 _proof_445✝⁴ _proof_446✝²) app₅.hom = CategoryStruct.comp app₄.hom (g.map' 4 5 _proof_445✝⁵ _proof_446✝³)) : (isoMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).inv = homMk₅ app₀.inv app₁.inv app₂.inv app₃.inv app₄.inv app₅.inv ⋯ ⋯ ⋯ ⋯ ⋯

theorem CategoryTheory.ComposableArrows.ext₅ {C : Type u_1} [Category.{v_1, u_1} C] {f g : ComposableArrows C 5} (h₀ : f.obj' 0 _proof_441✝ = g.obj' 0 _proof_441✝¹) (h₁ : f.obj' 1 _proof_442✝ = g.obj' 1 _proof_442✝¹) (h₂ : f.obj' 2 _proof_443✝ = g.obj' 2 _proof_443✝¹) (h₃ : f.obj' 3 _proof_444✝ = g.obj' 3 _proof_444✝¹) (h₄ : f.obj' 4 _proof_445✝ = g.obj' 4 _proof_445✝¹) (h₅ : f.obj' 5 _proof_446✝ = g.obj' 5 _proof_446✝¹) (w₀ : f.map' 0 1 homMk₁._proof_4 _proof_442✝² = CategoryStruct.comp (eqToHom h₀) (CategoryStruct.comp (g.map' 0 1 homMk₁._proof_4 _proof_442✝³) (eqToHom ⋯))) (w₁ : f.map' 1 2 _proof_238✝ _proof_443✝² = CategoryStruct.comp (eqToHom h₁) (CategoryStruct.comp (g.map' 1 2 _proof_238✝¹ _proof_443✝³) (eqToHom ⋯))) (w₂ : f.map' 2 3 _proof_291✝ _proof_444✝² = CategoryStruct.comp (eqToHom h₂) (CategoryStruct.comp (g.map' 2 3 _proof_291✝¹ _proof_444✝³) (eqToHom ⋯))) (w₃ : f.map' 3 4 _proof_356✝ _proof_445✝² = CategoryStruct.comp (eqToHom h₃) (CategoryStruct.comp (g.map' 3 4 _proof_356✝¹ _proof_445✝³) (eqToHom ⋯))) (w₄ : f.map' 4 5 _proof_445✝⁴ _proof_446✝² = CategoryStruct.comp (eqToHom h₄) (CategoryStruct.comp (g.map' 4 5 _proof_445✝⁵ _proof_446✝³) (eqToHom ⋯))) : f = g

theorem CategoryTheory.ComposableArrows.mk₅_surjective {C : Type u_1} [Category.{v_1, u_1} C] (X : ComposableArrows C 5) : ∃ (X₀ : C) (X₁ : C) (X₂ : C) (X₃ : C) (X₄ : C) (X₅ : C) (f₀ : X₀ ⟶ X₁) (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (f₃ : X₃ ⟶ X₄) (f₄ : X₄ ⟶ X₅), X = mk₅ f₀ f₁ f₂ f₃ f₄

def CategoryTheory.ComposableArrows.arrow {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (F : ComposableArrows C n) (i : ℕ) (hi : i < n := by valid) : ComposableArrows C 1

The ith arrow of F : ComposableArrows C n.

theorem CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_exists {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ) : ∃ (F : ComposableArrows C n) (e : (i : Fin (n + 1)) → F.obj i ≅ obj i), ∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩ = CategoryStruct.comp (e ⟨i, ⋯⟩).inv (CategoryStruct.comp (F.map' i (i + 1) ⋯ hi) (e ⟨i + 1, ⋯⟩).hom)

noncomputable def CategoryTheory.ComposableArrows.mkOfObjOfMapSucc {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ) : ComposableArrows C n

Given obj : Fin (n + 1) → C and mapSucc i : obj i.castSucc ⟶ obj i.succ for all i : Fin n, this is F : ComposableArrows C n such that F.obj i is definitionally equal to obj i and such that F.map' i (i + 1) = mapSucc ⟨i, hi⟩.

@[simp]

theorem CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_obj {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ) (i : Fin (n + 1)) : (mkOfObjOfMapSucc obj mapSucc).obj i = obj i

theorem CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_map_succ {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ) (i : ℕ) (hi : i < n := by valid) : (mkOfObjOfMapSucc obj mapSucc).map' i (i + 1) ⋯ hi = mapSucc ⟨i, hi⟩

theorem CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_arrow {C : Type u_1} [Category.{v_1, u_1} C] {n : ℕ} (obj : Fin (n + 1) → C) (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ) (i : ℕ) (hi : i < n := by valid) : (mkOfObjOfMapSucc obj mapSucc).arrow i hi = mk₁ (mapSucc ⟨i, hi⟩)

noncomputable def CategoryTheory.ComposableArrows.opEquivalence (C : Type u_1) [Category.{v_1, u_1} C] (n : ℕ) : (ComposableArrows C n)ᵒᵖ ≌ ComposableArrows Cᵒᵖ n

The equivalence (ComposableArrows C n)ᵒᵖ ≌ ComposableArrows Cᵒᵖ n obtained by reversing the arrows.

@[simp]

theorem CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_app (C : Type u_1) [Category.{v_1, u_1} C] (n : ℕ) (X : ComposableArrows Cᵒᵖ n) (X✝ : Fin (n + 1)) : ((opEquivalence C n).counitIso.inv.app X).app X✝ = X.map (((orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).unitInv.app (Opposite.op X✝)).unop

@[simp]

theorem CategoryTheory.ComposableArrows.opEquivalence_inverse_map (C : Type u_1) [Category.{v_1, u_1} C] (n : ℕ) {X✝ Y✝ : ComposableArrows Cᵒᵖ n} (f : X✝ ⟶ Y✝) : (opEquivalence C n).inverse.map f = ((⋯.functor.comp (orderDualEquivalence (Fin (n + 1))).functor).whiskerLeft (NatTrans.leftOp f)).op

@[simp]

theorem CategoryTheory.ComposableArrows.opEquivalence_inverse_obj (C : Type u_1) [Category.{v_1, u_1} C] (n : ℕ) (X : ComposableArrows Cᵒᵖ n) : (opEquivalence C n).inverse.obj X = Opposite.op ((⋯.functor.comp (orderDualEquivalence (Fin (n + 1))).functor).comp (Functor.leftOp X))

@[simp]

theorem CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_app (C : Type u_1) [Category.{v_1, u_1} C] (n : ℕ) (X : ComposableArrows Cᵒᵖ n) (X✝ : Fin (n + 1)) : ((opEquivalence C n).counitIso.hom.app X).app X✝ = X.map (((orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.counitInv.app (Opposite.op X✝)).unop

@[simp]

theorem CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_app (C : Type u_1) [Category.{v_1, u_1} C] (n : ℕ) (X : (Functor (Fin (n + 1)) C)ᵒᵖ) : (opEquivalence C n).unitIso.hom.app X = CategoryStruct.comp (((orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.funInvIdAssoc (Opposite.unop X)).hom.op ((⋯.functor.comp (orderDualEquivalence (Fin (n + 1))).functor).whiskerLeft (((orderDualEquivalence (Fin (n + 1))).inverse.comp ⋯.functor).comp (Opposite.unop X)).rightOpLeftOpIso.hom.op.unop).op

@[simp]

theorem CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_app (C : Type u_1) [Category.{v_1, u_1} C] (n : ℕ) (X : (Functor (Fin (n + 1)) C)ᵒᵖ) : (opEquivalence C n).unitIso.inv.app X = CategoryStruct.comp ((⋯.functor.comp (orderDualEquivalence (Fin (n + 1))).functor).whiskerLeft (((orderDualEquivalence (Fin (n + 1))).inverse.comp ⋯.functor).comp (Opposite.unop X)).rightOpLeftOpIso.inv.op.unop).op (((orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.funInvIdAssoc (Opposite.unop X)).inv.op

@[simp]

theorem CategoryTheory.ComposableArrows.opEquivalence_functor_obj_obj (C : Type u_1) [Category.{v_1, u_1} C] (n : ℕ) (X : (Functor (Fin (n + 1)) C)ᵒᵖ) (X✝ : Fin (n + 1)) : ((opEquivalence C n).functor.obj X).obj X✝ = Opposite.op ((Opposite.unop X).obj X✝.rev)

@[simp]

theorem CategoryTheory.ComposableArrows.opEquivalence_functor_obj_map (C : Type u_1) [Category.{v_1, u_1} C] (n : ℕ) (X : (Functor (Fin (n + 1)) C)ᵒᵖ) {X✝ Y✝ : Fin (n + 1)} (f : X✝ ⟶ Y✝) : ((opEquivalence C n).functor.obj X).map f = ((Opposite.unop X).map (⋯.functor.map (homOfLE ⋯))).op

@[simp]

theorem CategoryTheory.ComposableArrows.opEquivalence_functor_map_app (C : Type u_1) [Category.{v_1, u_1} C] (n : ℕ) {X✝ Y✝ : (Functor (Fin (n + 1)) C)ᵒᵖ} (f : X✝ ⟶ Y✝) (x✝ : Fin (n + 1)) : ((opEquivalence C n).functor.map f).app x✝ = (f.unop.app x✝.rev).op

def CategoryTheory.Functor.mapComposableArrows {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (G : Functor C D) (n : ℕ) : Functor (ComposableArrows C n) (ComposableArrows D n)

The functor ComposableArrows C n ⥤ ComposableArrows D n obtained by postcomposition with a functor C ⥤ D.

@[simp]

theorem CategoryTheory.Functor.mapComposableArrows_map_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (G : Functor C D) (n : ℕ) {X✝ Y✝ : Functor (Fin (n + 1)) C} (α : X✝ ⟶ Y✝) (X : Fin (n + 1)) : ((G.mapComposableArrows n).map α).app X = G.map (α.app X)

@[simp]

theorem CategoryTheory.Functor.mapComposableArrows_obj_map {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (G : Functor C D) (n : ℕ) (F : Functor (Fin (n + 1)) C) {X✝ Y✝ : Fin (n + 1)} (f : X✝ ⟶ Y✝) : ((G.mapComposableArrows n).obj F).map f = G.map (F.map f)

@[simp]

theorem CategoryTheory.Functor.mapComposableArrows_obj_obj {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (G : Functor C D) (n : ℕ) (F : Functor (Fin (n + 1)) C) (X : Fin (n + 1)) : ((G.mapComposableArrows n).obj F).obj X = G.obj (F.obj X)

def CategoryTheory.Functor.mapComposableArrowsObjMk₁Iso {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (G : Functor C D) {X Y : C} (f : X ⟶ Y) : (G.mapComposableArrows 1).obj (ComposableArrows.mk₁ f) ≅ ComposableArrows.mk₁ (G.map f)

The isomorphism between (G.mapComposableArrows 1).obj (.mk₁ f) and .mk₁ (G.map f).

@[simp]

theorem CategoryTheory.Functor.mapComposableArrowsObjMk₁Iso_hom_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (G : Functor C D) {X Y : C} (f : X ⟶ Y) (i : Fin (1 + 1)) : (G.mapComposableArrowsObjMk₁Iso f).hom.app i = match i with | ⟨0, isLt⟩ => CategoryStruct.id (G.obj X) | ⟨1, isLt⟩ => CategoryStruct.id (G.obj Y)

@[simp]

theorem CategoryTheory.Functor.mapComposableArrowsObjMk₁Iso_inv_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (G : Functor C D) {X Y : C} (f : X ⟶ Y) (i : Fin (1 + 1)) : (G.mapComposableArrowsObjMk₁Iso f).inv.app i = match i with | ⟨0, isLt⟩ => CategoryStruct.id (G.obj X) | ⟨1, isLt⟩ => CategoryStruct.id (G.obj Y)

def CategoryTheory.Functor.mapComposableArrowsObjMk₂Iso {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (G : Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (G.mapComposableArrows 2).obj (ComposableArrows.mk₂ f g) ≅ ComposableArrows.mk₂ (G.map f) (G.map g)

The isomorphism between (G.mapComposableArrows 2).obj (.mk₂ f g) and .mk₂ (G.map f) (G.map g).

@[simp]

theorem CategoryTheory.Functor.mapComposableArrowsObjMk₂Iso_hom_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (G : Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (i : Fin (1 + 1 + 1)) : (G.mapComposableArrowsObjMk₂Iso f g).hom.app i = match i with | ⟨0, isLt⟩ => CategoryStruct.id (G.obj X) | ⟨i.succ, hi⟩ => match ⟨i, ⋯⟩ with | ⟨0, isLt⟩ => CategoryStruct.id (G.obj Y) | ⟨1, isLt⟩ => CategoryStruct.id (G.obj Z)

@[simp]

theorem CategoryTheory.Functor.mapComposableArrowsObjMk₂Iso_inv_app {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (G : Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (i : Fin (1 + 1 + 1)) : (G.mapComposableArrowsObjMk₂Iso f g).inv.app i = match i with | ⟨0, isLt⟩ => CategoryStruct.id (G.obj X) | ⟨i.succ, hi⟩ => match ⟨i, ⋯⟩ with | ⟨0, isLt⟩ => CategoryStruct.id (G.obj Y) | ⟨1, isLt⟩ => CategoryStruct.id (G.obj Z)

noncomputable def CategoryTheory.Functor.mapComposableArrowsOpIso {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (G : Functor C D) (n : ℕ) : (G.mapComposableArrows n).comp (ComposableArrows.opEquivalence D n).functor.rightOp ≅ (ComposableArrows.opEquivalence C n).functor.rightOp.comp (G.op.mapComposableArrows n).op

The functor ComposableArrows C n ⥤ ComposableArrows D n induced by G : C ⥤ D commutes with opEquivalence.