ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : CategoryTheory.Functor J CategoryTheory.Cat<VAR>X : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)<GOAL>CategoryTheory.CategoryStruct.id X = CategoryTheory.Limits.Types.Limit.mk (CategoryTheory.Cat.HasLimits.homDiagram X X) (fun j => CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) j X)) ⋯
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : CategoryTheory.Functor J CategoryTheory.Cat<VAR>X Y Z : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp f g = CategoryTheory.Limits.Types.Limit.mk (CategoryTheory.Cat.HasLimits.homDiagram X Z) (fun j => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram X Y) j f) (CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram Y Z) j g)) ⋯
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : CategoryTheory.Functor J CategoryTheory.Cat<GOAL>(CategoryTheory.Cat.HasLimits.limitConeX F).str = inferInstance
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : CategoryTheory.Functor J CategoryTheory.Cat<GOAL>↑(CategoryTheory.Cat.HasLimits.limitConeX F) = CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : CategoryTheory.Functor J CategoryTheory.Cat<VAR>j : J<GOAL>∀ {X Y : ↑(((CategoryTheory.Functor.const J).obj (CategoryTheory.Cat.HasLimits.limitConeX F)).obj j)} (f : X ⟶ Y), ((CategoryTheory.Cat.HasLimits.limitCone F).π.app j).map f = CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram X Y) j f
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : CategoryTheory.Functor J CategoryTheory.Cat<VAR>j : J<GOAL>∀ (a : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)), ((CategoryTheory.Cat.HasLimits.limitCone F).π.app j).obj a = CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) j a
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : CategoryTheory.Functor J CategoryTheory.Cat<GOAL>(CategoryTheory.Cat.HasLimits.limitCone F).pt = CategoryTheory.Cat.HasLimits.limitConeX F
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : CategoryTheory.Functor J CategoryTheory.Cat<VAR>s : CategoryTheory.Limits.Cone F<GOAL>∀ (a : { pt := ↑s.pt, π := { app := fun j => (s.π.app j).obj, naturality := ⋯ } }.pt), (CategoryTheory.Cat.HasLimits.limitConeLift F s).obj a = CategoryTheory.Limits.limit.lift (F.comp CategoryTheory.Cat.objects) { pt := ↑s.pt, π := { app := fun j => (s.π.app j).obj, naturality := ⋯ } } a
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : CategoryTheory.Functor J CategoryTheory.Cat<VAR>s : CategoryTheory.Limits.Cone F<GOAL>∀ {X Y : ↑s.pt} (f : X ⟶ Y), (CategoryTheory.Cat.HasLimits.limitConeLift F s).map f = CategoryTheory.Limits.Types.Limit.mk (CategoryTheory.Cat.HasLimits.homDiagram (CategoryTheory.Limits.limit.lift (F.comp CategoryTheory.Cat.objects) { pt := ↑s.pt, π := { app := fun j => (s.π.app j).obj, naturality := ⋯ } } X) (CategoryTheory.Limits.limit.lift (F.comp CategoryTheory.Cat.objects) { pt := ↑s.pt, π := { app := fun j => (s.π.app j).obj, naturality := ⋯ } } Y)) (fun j => CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((s.π.app j).map f) (CategoryTheory.eqToHom ⋯))) ⋯
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : CategoryTheory.Functor J CategoryTheory.Cat<VAR>X Y : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)<VAR>j : J<VAR>h : X = Y<GOAL>CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram X Y) j (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
<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 Y : CategoryTheory.Comma L R<VAR>self : CategoryTheory.CommaMorphism X Y<GOAL>CategoryTheory.CategoryStruct.comp (L.map self.left) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R.map self.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 Y : CategoryTheory.Comma L R<VAR>f g : X ⟶ Y<VAR>h₁ : f.left = g.left<VAR>h₂ : f.right = g.right<GOAL>f = g
<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.CategoryStruct.id 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.CategoryStruct.id 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 Y Z : CategoryTheory.Comma L R<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.CategoryStruct.comp f g).left = CategoryTheory.CategoryStruct.comp f.left g.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 Y Z : CategoryTheory.Comma L R<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.CategoryStruct.comp f g).right = CategoryTheory.CategoryStruct.comp f.right g.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.fst L R).obj X = 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<GOAL>∀ {X Y : CategoryTheory.Comma L R} (f : X ⟶ Y), (CategoryTheory.Comma.fst L R).map f = 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 : CategoryTheory.Functor B T<VAR>X : CategoryTheory.Comma L R<GOAL>(CategoryTheory.Comma.snd L R).obj X = 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<GOAL>∀ {X Y : CategoryTheory.Comma L R} (f : X ⟶ Y), (CategoryTheory.Comma.snd L R).map f = 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 : CategoryTheory.Functor B T<VAR>X : CategoryTheory.Comma L R<GOAL>(CategoryTheory.Comma.natTrans L R).app X = 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>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>X Y : CategoryTheory.Comma L R<VAR>H : X = Y<GOAL>(CategoryTheory.eqToHom H).left = CategoryTheory.eqToHom ⋯
<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 Y : CategoryTheory.Comma L R<VAR>H : X = Y<GOAL>(CategoryTheory.eqToHom H).right = CategoryTheory.eqToHom ⋯
<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 Y : CategoryTheory.Comma L₁ R₁<VAR>α : X ≅ Y<GOAL>(CategoryTheory.Comma.leftIso α).inv = α.inv.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 Y : CategoryTheory.Comma L₁ R₁<VAR>α : X ≅ Y<GOAL>(CategoryTheory.Comma.leftIso α).hom = α.hom.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 Y : CategoryTheory.Comma L₁ R₁<VAR>α : X ≅ Y<GOAL>(CategoryTheory.Comma.rightIso α).hom = α.hom.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 Y : CategoryTheory.Comma L₁ R₁<VAR>α : X ≅ Y<GOAL>(CategoryTheory.Comma.rightIso α).inv = α.inv.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 Y : CategoryTheory.Comma L₁ R₁<VAR>l : X.left ≅ Y.left<VAR>r : X.right ≅ Y.right<VAR>h : CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom) := by aesop_cat<GOAL>(CategoryTheory.Comma.isoMk l r h).hom.right = r.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>L₁ : CategoryTheory.Functor A T<VAR>R₁ : CategoryTheory.Functor B T<VAR>X Y : CategoryTheory.Comma L₁ R₁<VAR>l : X.left ≅ Y.left<VAR>r : X.right ≅ Y.right<VAR>h : CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom) := by aesop_cat<GOAL>(CategoryTheory.Comma.isoMk l r h).inv.right = r.inv
<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 Y : CategoryTheory.Comma L₁ R₁<VAR>l : X.left ≅ Y.left<VAR>r : X.right ≅ Y.right<VAR>h : CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom) := by aesop_cat<GOAL>(CategoryTheory.Comma.isoMk l r h).inv.left = l.inv
<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 Y : CategoryTheory.Comma L₁ R₁<VAR>l : X.left ≅ Y.left<VAR>r : X.right ≅ Y.right<VAR>h : CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom) := by aesop_cat<GOAL>(CategoryTheory.Comma.isoMk l r h).hom.left = l.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>A' : Type u_1<VAR>B' : Type u_2<VAR>T' : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} A'<VAR>CategoryTheory.Category.{u_5, u_2} B'<VAR>CategoryTheory.Category.{u_6, u_3} T'<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>L' : CategoryTheory.Functor A' T'<VAR>R' : CategoryTheory.Functor B' T'<VAR>F₁ : CategoryTheory.Functor A A'<VAR>F₂ : CategoryTheory.Functor B B'<VAR>F : CategoryTheory.Functor T T'<VAR>α : F₁.comp L' ⟶ L.comp F<VAR>β : R.comp F ⟶ F₂.comp R'<VAR>X Y : CategoryTheory.Comma L R<VAR>φ : X ⟶ Y<GOAL>((CategoryTheory.Comma.map α β).map φ).right = F₂.map φ.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>A' : Type u_1<VAR>B' : Type u_2<VAR>T' : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} A'<VAR>CategoryTheory.Category.{u_5, u_2} B'<VAR>CategoryTheory.Category.{u_6, u_3} T'<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>L' : CategoryTheory.Functor A' T'<VAR>R' : CategoryTheory.Functor B' T'<VAR>F₁ : CategoryTheory.Functor A A'<VAR>F₂ : CategoryTheory.Functor B B'<VAR>F : CategoryTheory.Functor T T'<VAR>α : F₁.comp L' ⟶ L.comp F<VAR>β : R.comp F ⟶ F₂.comp R'<VAR>X : CategoryTheory.Comma L R<GOAL>((CategoryTheory.Comma.map α β).obj X).hom = CategoryTheory.CategoryStruct.comp (α.app X.left) (CategoryTheory.CategoryStruct.comp (F.map X.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>A' : Type u_1<VAR>B' : Type u_2<VAR>T' : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} A'<VAR>CategoryTheory.Category.{u_5, u_2} B'<VAR>CategoryTheory.Category.{u_6, u_3} T'<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>L' : CategoryTheory.Functor A' T'<VAR>R' : CategoryTheory.Functor B' T'<VAR>F₁ : CategoryTheory.Functor A A'<VAR>F₂ : CategoryTheory.Functor B B'<VAR>F : CategoryTheory.Functor T T'<VAR>α : F₁.comp L' ⟶ L.comp F<VAR>β : R.comp F ⟶ F₂.comp R'<VAR>X : CategoryTheory.Comma L R<GOAL>((CategoryTheory.Comma.map α β).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>A' : Type u_1<VAR>B' : Type u_2<VAR>T' : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} A'<VAR>CategoryTheory.Category.{u_5, u_2} B'<VAR>CategoryTheory.Category.{u_6, u_3} T'<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>L' : CategoryTheory.Functor A' T'<VAR>R' : CategoryTheory.Functor B' T'<VAR>F₁ : CategoryTheory.Functor A A'<VAR>F₂ : CategoryTheory.Functor B B'<VAR>F : CategoryTheory.Functor T T'<VAR>α : F₁.comp L' ⟶ L.comp F<VAR>β : R.comp F ⟶ F₂.comp R'<VAR>X Y : CategoryTheory.Comma L R<VAR>φ : X ⟶ Y<GOAL>((CategoryTheory.Comma.map α β).map φ).left = F₁.map φ.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>A' : Type u_1<VAR>B' : Type u_2<VAR>T' : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} A'<VAR>CategoryTheory.Category.{u_5, u_2} B'<VAR>CategoryTheory.Category.{u_6, u_3} T'<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>L' : CategoryTheory.Functor A' T'<VAR>R' : CategoryTheory.Functor B' T'<VAR>F₁ : CategoryTheory.Functor A A'<VAR>F₂ : CategoryTheory.Functor B B'<VAR>F : CategoryTheory.Functor T T'<VAR>α : F₁.comp L' ⟶ L.comp F<VAR>β : R.comp F ⟶ F₂.comp R'<VAR>X : CategoryTheory.Comma L R<GOAL>((CategoryTheory.Comma.map α β).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>R : CategoryTheory.Functor B T<VAR>L₁ L₂ : CategoryTheory.Functor A T<VAR>l : L₁ ⟶ L₂<VAR>X : CategoryTheory.Comma L₂ R<GOAL>((CategoryTheory.Comma.mapLeft R l).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>l : L₁ ⟶ L₂<GOAL>∀ {X Y : CategoryTheory.Comma L₂ R} (f : X ⟶ Y), ((CategoryTheory.Comma.mapLeft R l).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>l : L₁ ⟶ L₂<GOAL>∀ {X Y : CategoryTheory.Comma L₂ R} (f : X ⟶ Y), ((CategoryTheory.Comma.mapLeft R l).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>l : L₁ ⟶ L₂<VAR>X : CategoryTheory.Comma L₂ R<GOAL>((CategoryTheory.Comma.mapLeft R l).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>l : L₁ ⟶ L₂<VAR>X : CategoryTheory.Comma L₂ R<GOAL>((CategoryTheory.Comma.mapLeft R l).obj X).hom = CategoryTheory.CategoryStruct.comp (l.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>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>X : CategoryTheory.Comma L R<GOAL>((CategoryTheory.Comma.mapLeftId 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.mapLeftId 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 : CategoryTheory.Functor B T<VAR>X : CategoryTheory.Comma L R<GOAL>((CategoryTheory.Comma.mapLeftId 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.mapLeftId 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>R : CategoryTheory.Functor B T<VAR>L₁ L₂ L₃ : CategoryTheory.Functor A T<VAR>l : L₁ ⟶ L₂<VAR>l' : L₂ ⟶ L₃<VAR>X : CategoryTheory.Comma L₃ R<GOAL>((CategoryTheory.Comma.mapLeftComp R l l').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>R : CategoryTheory.Functor B T<VAR>L₁ L₂ L₃ : CategoryTheory.Functor A T<VAR>l : L₁ ⟶ L₂<VAR>l' : L₂ ⟶ L₃<VAR>X : CategoryTheory.Comma L₃ R<GOAL>((CategoryTheory.Comma.mapLeftComp R l l').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₂ L₃ : CategoryTheory.Functor A T<VAR>l : L₁ ⟶ L₂<VAR>l' : L₂ ⟶ L₃<VAR>X : CategoryTheory.Comma L₃ R<GOAL>((CategoryTheory.Comma.mapLeftComp R l l').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₂ L₃ : CategoryTheory.Functor A T<VAR>l : L₁ ⟶ L₂<VAR>l' : L₂ ⟶ L₃<VAR>X : CategoryTheory.Comma L₃ R<GOAL>((CategoryTheory.Comma.mapLeftComp R l l').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>l l' : L₁ ⟶ L₂<VAR>h : l = l'<VAR>X : CategoryTheory.Comma L₂ R<GOAL>((CategoryTheory.Comma.mapLeftEq R l l' 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>R : CategoryTheory.Functor B T<VAR>L₁ L₂ : CategoryTheory.Functor A T<VAR>l l' : L₁ ⟶ L₂<VAR>h : l = l'<VAR>X : CategoryTheory.Comma L₂ R<GOAL>((CategoryTheory.Comma.mapLeftEq R l l' 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>R : CategoryTheory.Functor B T<VAR>L₁ L₂ : CategoryTheory.Functor A T<VAR>l l' : L₁ ⟶ L₂<VAR>h : l = l'<VAR>X : CategoryTheory.Comma L₂ R<GOAL>((CategoryTheory.Comma.mapLeftEq R l l' 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>R : CategoryTheory.Functor B T<VAR>L₁ L₂ : CategoryTheory.Functor A T<VAR>l l' : L₁ ⟶ L₂<VAR>h : l = l'<VAR>X : CategoryTheory.Comma L₂ R<GOAL>((CategoryTheory.Comma.mapLeftEq R l l' 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>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).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₂<VAR>X : CategoryTheory.Comma L₁ R<GOAL>((CategoryTheory.Comma.mapLeftIso R 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>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.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>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.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.hom.app X).right = CategoryTheory.CategoryStruct.id X.right