ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯)<VAR>w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.isoMk₂ app₀ app₁ app₂ w₀ w₁).inv = CategoryTheory.ComposableArrows.homMk₂ app₀.inv app₁.inv app₂.inv ⋯ ⋯
<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₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯)<VAR>w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.isoMk₂ app₀ app₁ app₂ w₀ w₁).hom = CategoryTheory.ComposableArrows.homMk₂ app₀.hom app₁.hom app₂.hom w₀ w₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 2<VAR>h₀ : f.obj' 0 ⋯ = g.obj' 0 ⋯<VAR>h₁ : f.obj' 1 ⋯ = g.obj' 1 ⋯<VAR>h₂ : f.obj' 2 ⋯ = g.obj' 2 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀) (CategoryTheory.CategoryStruct.comp (g.map' 0 1 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))<VAR>w₁ : f.map' 1 2 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁) (CategoryTheory.CategoryStruct.comp (g.map' 1 2 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))<GOAL>f = g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.ComposableArrows C 2<GOAL>∃ X₀ X₁ X₂ f₀ f₁, X = CategoryTheory.ComposableArrows.mk₂ f₀ f₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 3<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>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<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 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app 0 = app₀
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 3<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>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<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 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app 1 = app₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 3<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>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<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 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app ⟨2, ⋯⟩ = app₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 3<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>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<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 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app ⟨3, ⋯⟩ = app₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 3<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 ⋯<VAR>h₃ : CategoryTheory.ComposableArrows.app' φ 3 ⋯ = CategoryTheory.ComposableArrows.app' φ' 3 ⋯<GOAL>φ = φ'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 3<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>app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯<VAR>w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯)<VAR>w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.isoMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).hom = CategoryTheory.ComposableArrows.homMk₃ app₀.hom app₁.hom app₂.hom app₃.hom w₀ w₁ w₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 3<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>app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯<VAR>w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯)<VAR>w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.isoMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).inv = CategoryTheory.ComposableArrows.homMk₃ app₀.inv app₁.inv app₂.inv app₃.inv ⋯ ⋯ ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 3<VAR>h₀ : f.obj' 0 ⋯ = g.obj' 0 ⋯<VAR>h₁ : f.obj' 1 ⋯ = g.obj' 1 ⋯<VAR>h₂ : f.obj' 2 ⋯ = g.obj' 2 ⋯<VAR>h₃ : f.obj' 3 ⋯ = g.obj' 3 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀) (CategoryTheory.CategoryStruct.comp (g.map' 0 1 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))<VAR>w₁ : f.map' 1 2 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁) (CategoryTheory.CategoryStruct.comp (g.map' 1 2 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))<VAR>w₂ : f.map' 2 3 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₂) (CategoryTheory.CategoryStruct.comp (g.map' 2 3 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))<GOAL>f = g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.ComposableArrows C 3<GOAL>∃ X₀ X₁ X₂ X₃ f₀ f₁ f₂, X = CategoryTheory.ComposableArrows.mk₃ f₀ f₁ f₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 4<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>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯<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 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯)<VAR>w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app 0 = app₀
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 4<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>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯<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 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯)<VAR>w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app 1 = app₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 4<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>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯<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 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯)<VAR>w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app ⟨2, ⋯⟩ = app₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 4<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>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯<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 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯)<VAR>w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app ⟨3, ⋯⟩ = app₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 4<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>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯<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 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯)<VAR>w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app ⟨4, ⋯⟩ = app₄
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 4<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 ⋯<VAR>h₃ : CategoryTheory.ComposableArrows.app' φ 3 ⋯ = CategoryTheory.ComposableArrows.app' φ' 3 ⋯<VAR>h₄ : CategoryTheory.ComposableArrows.app' φ 4 ⋯ = CategoryTheory.ComposableArrows.app' φ' 4 ⋯<GOAL>φ = φ'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>n m : ℕ<VAR>h : n + 1 ≤ m<VAR>f g : CategoryTheory.ComposableArrows C m<VAR>app : f.obj' n ⋯ ≅ g.obj' n ⋯<VAR>app' : f.obj' (n + 1) h ≅ g.obj' (n + 1) h<VAR>w : CategoryTheory.CategoryStruct.comp (f.map' n (n + 1) ⋯ h) app'.hom = CategoryTheory.CategoryStruct.comp app.hom (g.map' n (n + 1) ⋯ h)<GOAL>CategoryTheory.CategoryStruct.comp (g.map' n (n + 1) ⋯ h) app'.inv = CategoryTheory.CategoryStruct.comp app.inv (f.map' n (n + 1) ⋯ h)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 4<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>app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯<VAR>w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯)<VAR>w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 ⋯ ⋯)<VAR>w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.isoMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).hom = CategoryTheory.ComposableArrows.homMk₄ app₀.hom app₁.hom app₂.hom app₃.hom app₄.hom w₀ w₁ w₂ w₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 4<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>app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ≅ g.obj' 4 ⋯<VAR>w₀ : CategoryTheory.CategoryStruct.comp (f.map' 0 1 ⋯ ⋯) app₁.hom = CategoryTheory.CategoryStruct.comp app₀.hom (g.map' 0 1 ⋯ ⋯)<VAR>w₁ : CategoryTheory.CategoryStruct.comp (f.map' 1 2 ⋯ ⋯) app₂.hom = CategoryTheory.CategoryStruct.comp app₁.hom (g.map' 1 2 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃.hom = CategoryTheory.CategoryStruct.comp app₂.hom (g.map' 2 3 ⋯ ⋯)<VAR>w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄.hom = CategoryTheory.CategoryStruct.comp app₃.hom (g.map' 3 4 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.isoMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).inv = CategoryTheory.ComposableArrows.homMk₄ app₀.inv app₁.inv app₂.inv app₃.inv app₄.inv ⋯ ⋯ ⋯ ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 4<VAR>h₀ : f.obj' 0 ⋯ = g.obj' 0 ⋯<VAR>h₁ : f.obj' 1 ⋯ = g.obj' 1 ⋯<VAR>h₂ : f.obj' 2 ⋯ = g.obj' 2 ⋯<VAR>h₃ : f.obj' 3 ⋯ = g.obj' 3 ⋯<VAR>h₄ : f.obj' 4 ⋯ = g.obj' 4 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀) (CategoryTheory.CategoryStruct.comp (g.map' 0 1 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))<VAR>w₁ : f.map' 1 2 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁) (CategoryTheory.CategoryStruct.comp (g.map' 1 2 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))<VAR>w₂ : f.map' 2 3 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₂) (CategoryTheory.CategoryStruct.comp (g.map' 2 3 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))<VAR>w₃ : f.map' 3 4 ⋯ ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₃) (CategoryTheory.CategoryStruct.comp (g.map' 3 4 ⋯ ⋯) (CategoryTheory.eqToHom ⋯))<GOAL>f = g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.ComposableArrows C 4<GOAL>∃ X₀ X₁ X₂ X₃ X₄ f₀ f₁ f₂ f₃, X = CategoryTheory.ComposableArrows.mk₄ f₀ f₁ f₂ f₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 5<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>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯<VAR>app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯<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 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯)<VAR>w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯)<VAR>w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ⋯ ⋯) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app 0 = app₀
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 5<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>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯<VAR>app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯<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 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯)<VAR>w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯)<VAR>w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ⋯ ⋯) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app 1 = app₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 5<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>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯<VAR>app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯<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 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯)<VAR>w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯)<VAR>w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ⋯ ⋯) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨2, ⋯⟩ = app₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 5<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>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯<VAR>app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯<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 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯)<VAR>w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯)<VAR>w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ⋯ ⋯) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨3, ⋯⟩ = app₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 5<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>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯<VAR>app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯<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 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯)<VAR>w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯)<VAR>w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ⋯ ⋯) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨4, ⋯⟩ = app₄
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 5<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>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯<VAR>app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯<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 ⋯ ⋯)<VAR>w₂ : CategoryTheory.CategoryStruct.comp (f.map' 2 3 ⋯ ⋯) app₃ = CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 ⋯ ⋯)<VAR>w₃ : CategoryTheory.CategoryStruct.comp (f.map' 3 4 ⋯ ⋯) app₄ = CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 ⋯ ⋯)<VAR>w₄ : CategoryTheory.CategoryStruct.comp (f.map' 4 5 ⋯ ⋯) app₅ = CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 ⋯ ⋯)<GOAL>(CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨5, ⋯⟩ = app₅
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>f g : CategoryTheory.ComposableArrows C 5<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 ⋯<VAR>h₃ : CategoryTheory.ComposableArrows.app' φ 3 ⋯ = CategoryTheory.ComposableArrows.app' φ' 3 ⋯<VAR>h₄ : CategoryTheory.ComposableArrows.app' φ 4 ⋯ = CategoryTheory.ComposableArrows.app' φ' 4 ⋯<VAR>h₅ : CategoryTheory.ComposableArrows.app' φ 5 ⋯ = CategoryTheory.ComposableArrows.app' φ' 5 ⋯<GOAL>φ = φ'