ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>R : CategoryTheory.Functor B T<VAR>L₁ L₂ : CategoryTheory.Functor A T<VAR>i : L₁ ≅ L₂<VAR>X : CategoryTheory.Comma L₁ R<GOAL>((CategoryTheory.Comma.mapLeftIso R i).functor.obj X).left = X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>R : CategoryTheory.Functor B T<VAR>L₁ L₂ : CategoryTheory.Functor A T<VAR>i : L₁ ≅ L₂<GOAL>∀ {X Y : CategoryTheory.Comma L₂ R} (f : X ⟶ Y), ((CategoryTheory.Comma.mapLeftIso R i).inverse.map f).left = f.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>R : CategoryTheory.Functor B T<VAR>L₁ L₂ : CategoryTheory.Functor A T<VAR>i : L₁ ≅ L₂<VAR>X : CategoryTheory.Comma L₂ R<GOAL>((CategoryTheory.Comma.mapLeftIso R i).inverse.obj X).hom = CategoryTheory.CategoryStruct.comp (i.hom.app X.left) X.hom
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>R : CategoryTheory.Functor B T<VAR>L₁ L₂ : CategoryTheory.Functor A T<VAR>i : L₁ ≅ L₂<VAR>X : CategoryTheory.Comma L₂ R<GOAL>((CategoryTheory.Comma.mapLeftIso R i).counitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>R : CategoryTheory.Functor B T<VAR>L₁ L₂ : CategoryTheory.Functor A T<VAR>i : L₁ ≅ L₂<VAR>X : CategoryTheory.Comma L₂ R<GOAL>((CategoryTheory.Comma.mapLeftIso R i).counitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>R : CategoryTheory.Functor B T<VAR>L₁ L₂ : CategoryTheory.Functor A T<VAR>i : L₁ ≅ L₂<VAR>X : CategoryTheory.Comma L₁ R<GOAL>((CategoryTheory.Comma.mapLeftIso R i).unitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>R : CategoryTheory.Functor B T<VAR>L₁ L₂ : CategoryTheory.Functor A T<VAR>i : L₁ ≅ L₂<GOAL>∀ {X Y : CategoryTheory.Comma L₁ R} (f : X ⟶ Y), ((CategoryTheory.Comma.mapLeftIso R i).functor.map f).left = f.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>R : CategoryTheory.Functor B T<VAR>L₁ L₂ : CategoryTheory.Functor A T<VAR>i : L₁ ≅ L₂<VAR>X : CategoryTheory.Comma L₁ R<GOAL>((CategoryTheory.Comma.mapLeftIso R i).functor.obj X).hom = CategoryTheory.CategoryStruct.comp (i.inv.app X.left) X.hom
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>R : CategoryTheory.Functor B T<VAR>L₁ L₂ : CategoryTheory.Functor A T<VAR>i : L₁ ≅ L₂<VAR>X : CategoryTheory.Comma L₂ R<GOAL>((CategoryTheory.Comma.mapLeftIso R i).inverse.obj X).right = X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>R : CategoryTheory.Functor B T<VAR>L₁ L₂ : CategoryTheory.Functor A T<VAR>i : L₁ ≅ L₂<GOAL>∀ {X Y : CategoryTheory.Comma L₁ R} (f : X ⟶ Y), ((CategoryTheory.Comma.mapLeftIso R i).functor.map f).right = f.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>R : CategoryTheory.Functor B T<VAR>L₁ L₂ : CategoryTheory.Functor A T<VAR>i : L₁ ≅ L₂<VAR>X : CategoryTheory.Comma L₁ R<GOAL>((CategoryTheory.Comma.mapLeftIso R i).unitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>R : CategoryTheory.Functor B T<VAR>L₁ L₂ : CategoryTheory.Functor A T<VAR>i : L₁ ≅ L₂<VAR>X : CategoryTheory.Comma L₂ R<GOAL>((CategoryTheory.Comma.mapLeftIso R i).counitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>R : CategoryTheory.Functor B T<VAR>L₁ L₂ : CategoryTheory.Functor A T<VAR>i : L₁ ≅ L₂<GOAL>∀ {X Y : CategoryTheory.Comma L₂ R} (f : X ⟶ Y), ((CategoryTheory.Comma.mapLeftIso R i).inverse.map f).right = f.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>r : R₁ ⟶ R₂<VAR>X : CategoryTheory.Comma L R₁<GOAL>((CategoryTheory.Comma.mapRight L r).obj X).left = X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>r : R₁ ⟶ R₂<GOAL>∀ {X Y : CategoryTheory.Comma L R₁} (f : X ⟶ Y), ((CategoryTheory.Comma.mapRight L r).map f).right = f.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>r : R₁ ⟶ R₂<GOAL>∀ {X Y : CategoryTheory.Comma L R₁} (f : X ⟶ Y), ((CategoryTheory.Comma.mapRight L r).map f).left = f.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>r : R₁ ⟶ R₂<VAR>X : CategoryTheory.Comma L R₁<GOAL>((CategoryTheory.Comma.mapRight L r).obj X).right = X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>r : R₁ ⟶ R₂<VAR>X : CategoryTheory.Comma L R₁<GOAL>((CategoryTheory.Comma.mapRight L r).obj X).hom = CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>X : CategoryTheory.Comma L R<GOAL>((CategoryTheory.Comma.mapRightId L R).inv.app X).left = CategoryTheory.CategoryStruct.id X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>X : CategoryTheory.Comma L R<GOAL>((CategoryTheory.Comma.mapRightId L R).inv.app X).right = CategoryTheory.CategoryStruct.id X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>X : CategoryTheory.Comma L R<GOAL>((CategoryTheory.Comma.mapRightId L R).hom.app X).left = CategoryTheory.CategoryStruct.id X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>X : CategoryTheory.Comma L R<GOAL>((CategoryTheory.Comma.mapRightId L R).hom.app X).right = CategoryTheory.CategoryStruct.id X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ R₃ : CategoryTheory.Functor B T<VAR>r : R₁ ⟶ R₂<VAR>r' : R₂ ⟶ R₃<VAR>X : CategoryTheory.Comma L R₁<GOAL>((CategoryTheory.Comma.mapRightComp L r r').hom.app X).left = CategoryTheory.CategoryStruct.id X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ R₃ : CategoryTheory.Functor B T<VAR>r : R₁ ⟶ R₂<VAR>r' : R₂ ⟶ R₃<VAR>X : CategoryTheory.Comma L R₁<GOAL>((CategoryTheory.Comma.mapRightComp L r r').inv.app X).left = CategoryTheory.CategoryStruct.id X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ R₃ : CategoryTheory.Functor B T<VAR>r : R₁ ⟶ R₂<VAR>r' : R₂ ⟶ R₃<VAR>X : CategoryTheory.Comma L R₁<GOAL>((CategoryTheory.Comma.mapRightComp L r r').hom.app X).right = CategoryTheory.CategoryStruct.id X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ R₃ : CategoryTheory.Functor B T<VAR>r : R₁ ⟶ R₂<VAR>r' : R₂ ⟶ R₃<VAR>X : CategoryTheory.Comma L R₁<GOAL>((CategoryTheory.Comma.mapRightComp L r r').inv.app X).right = CategoryTheory.CategoryStruct.id X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>r r' : R₁ ⟶ R₂<VAR>h : r = r'<VAR>X : CategoryTheory.Comma L R₁<GOAL>((CategoryTheory.Comma.mapRightEq L r r' h).inv.app X).left = CategoryTheory.CategoryStruct.id X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>r r' : R₁ ⟶ R₂<VAR>h : r = r'<VAR>X : CategoryTheory.Comma L R₁<GOAL>((CategoryTheory.Comma.mapRightEq L r r' h).inv.app X).right = CategoryTheory.CategoryStruct.id X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>r r' : R₁ ⟶ R₂<VAR>h : r = r'<VAR>X : CategoryTheory.Comma L R₁<GOAL>((CategoryTheory.Comma.mapRightEq L r r' h).hom.app X).left = CategoryTheory.CategoryStruct.id X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>r r' : R₁ ⟶ R₂<VAR>h : r = r'<VAR>X : CategoryTheory.Comma L R₁<GOAL>((CategoryTheory.Comma.mapRightEq L r r' h).hom.app X).right = CategoryTheory.CategoryStruct.id X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>i : R₁ ≅ R₂<VAR>X : CategoryTheory.Comma L R₁<GOAL>((CategoryTheory.Comma.mapRightIso L i).functor.obj X).left = X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>i : R₁ ≅ R₂<VAR>X : CategoryTheory.Comma L R₂<GOAL>((CategoryTheory.Comma.mapRightIso L i).inverse.obj X).hom = CategoryTheory.CategoryStruct.comp X.hom (i.inv.app X.right)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>i : R₁ ≅ R₂<GOAL>∀ {X Y : CategoryTheory.Comma L R₁} (f : X ⟶ Y), ((CategoryTheory.Comma.mapRightIso L i).functor.map f).left = f.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>i : R₁ ≅ R₂<VAR>X : CategoryTheory.Comma L R₁<GOAL>((CategoryTheory.Comma.mapRightIso L i).functor.obj X).hom = CategoryTheory.CategoryStruct.comp X.hom (i.hom.app X.right)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>i : R₁ ≅ R₂<VAR>X : CategoryTheory.Comma L R₁<GOAL>((CategoryTheory.Comma.mapRightIso L i).unitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>i : R₁ ≅ R₂<VAR>X : CategoryTheory.Comma L R₂<GOAL>((CategoryTheory.Comma.mapRightIso L i).counitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>i : R₁ ≅ R₂<GOAL>∀ {X Y : CategoryTheory.Comma L R₂} (f : X ⟶ Y), ((CategoryTheory.Comma.mapRightIso L i).inverse.map f).left = f.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>i : R₁ ≅ R₂<GOAL>∀ {X Y : CategoryTheory.Comma L R₁} (f : X ⟶ Y), ((CategoryTheory.Comma.mapRightIso L i).functor.map f).right = f.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>i : R₁ ≅ R₂<VAR>X : CategoryTheory.Comma L R₂<GOAL>((CategoryTheory.Comma.mapRightIso L i).inverse.obj X).left = X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>i : R₁ ≅ R₂<VAR>X : CategoryTheory.Comma L R₁<GOAL>((CategoryTheory.Comma.mapRightIso L i).unitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>i : R₁ ≅ R₂<VAR>X : CategoryTheory.Comma L R₁<GOAL>((CategoryTheory.Comma.mapRightIso L i).functor.obj X).right = X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>i : R₁ ≅ R₂<GOAL>∀ {X Y : CategoryTheory.Comma L R₂} (f : X ⟶ Y), ((CategoryTheory.Comma.mapRightIso L i).inverse.map f).right = f.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>i : R₁ ≅ R₂<VAR>X : CategoryTheory.Comma L R₂<GOAL>((CategoryTheory.Comma.mapRightIso L i).counitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>i : R₁ ≅ R₂<VAR>X : CategoryTheory.Comma L R₁<GOAL>((CategoryTheory.Comma.mapRightIso L i).unitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>i : R₁ ≅ R₂<VAR>X : CategoryTheory.Comma L R₁<GOAL>((CategoryTheory.Comma.mapRightIso L i).unitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>i : R₁ ≅ R₂<VAR>X : CategoryTheory.Comma L R₂<GOAL>((CategoryTheory.Comma.mapRightIso L i).inverse.obj X).right = X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>i : R₁ ≅ R₂<VAR>X : CategoryTheory.Comma L R₂<GOAL>((CategoryTheory.Comma.mapRightIso L i).counitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R₁ R₂ : CategoryTheory.Functor B T<VAR>i : R₁ ≅ R₂<VAR>X : CategoryTheory.Comma L R₂<GOAL>((CategoryTheory.Comma.mapRightIso L i).counitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>C : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} C<VAR>F : CategoryTheory.Functor C A<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>X : CategoryTheory.Comma (F.comp L) R<GOAL>((CategoryTheory.Comma.preLeft F L R).obj X).left = F.obj X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>C : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} C<VAR>F : CategoryTheory.Functor C A<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>X : CategoryTheory.Comma (F.comp L) R<GOAL>((CategoryTheory.Comma.preLeft F L R).obj X).hom = X.hom
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>C : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} C<VAR>F : CategoryTheory.Functor C A<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<GOAL>∀ {X Y : CategoryTheory.Comma (F.comp L) R} (f : X ⟶ Y), ((CategoryTheory.Comma.preLeft F L R).map f).right = f.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>C : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} C<VAR>F : CategoryTheory.Functor C A<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>X : CategoryTheory.Comma (F.comp L) R<GOAL>((CategoryTheory.Comma.preLeft F L R).obj X).right = X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>C : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} C<VAR>F : CategoryTheory.Functor C A<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<GOAL>∀ {X Y : CategoryTheory.Comma (F.comp L) R} (f : X ⟶ Y), ((CategoryTheory.Comma.preLeft F L R).map f).left = F.map f.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>C : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} C<VAR>L : CategoryTheory.Functor A T<VAR>F : CategoryTheory.Functor C B<VAR>R : CategoryTheory.Functor B T<VAR>X : CategoryTheory.Comma L (F.comp R)<GOAL>((CategoryTheory.Comma.preRight L F R).obj X).left = X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>C : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} C<VAR>L : CategoryTheory.Functor A T<VAR>F : CategoryTheory.Functor C B<VAR>R : CategoryTheory.Functor B T<VAR>X : CategoryTheory.Comma L (F.comp R)<GOAL>((CategoryTheory.Comma.preRight L F R).obj X).right = F.obj X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>C : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} C<VAR>L : CategoryTheory.Functor A T<VAR>F : CategoryTheory.Functor C B<VAR>R : CategoryTheory.Functor B T<GOAL>∀ {X Y : CategoryTheory.Comma L (F.comp R)} (f : X ⟶ Y), ((CategoryTheory.Comma.preRight L F R).map f).right = F.map f.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>C : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} C<VAR>L : CategoryTheory.Functor A T<VAR>F : CategoryTheory.Functor C B<VAR>R : CategoryTheory.Functor B T<VAR>X : CategoryTheory.Comma L (F.comp R)<GOAL>((CategoryTheory.Comma.preRight L F R).obj X).hom = X.hom
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>C : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} C<VAR>L : CategoryTheory.Functor A T<VAR>F : CategoryTheory.Functor C B<VAR>R : CategoryTheory.Functor B T<GOAL>∀ {X Y : CategoryTheory.Comma L (F.comp R)} (f : X ⟶ Y), ((CategoryTheory.Comma.preRight L F R).map f).left = f.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>C : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} C<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor T C<VAR>X : CategoryTheory.Comma L R<GOAL>((CategoryTheory.Comma.post L R F).obj X).left = X.left
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>C : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} C<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor T C<GOAL>∀ {X Y : CategoryTheory.Comma L R} (f : X ⟶ Y), ((CategoryTheory.Comma.post L R F).map f).left = f.left