ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u<VAR>Monoid M<GOAL>(MonoidHom.id M).toFunctor = 𝟭 (CategoryTheory.SingleObj M)
<VAR>M : Type u<VAR>N : Type v<VAR>Monoid M<VAR>Monoid N<VAR>e : M ≃* N<GOAL>∀ {X Y : CategoryTheory.SingleObj M} (a : M), e.toSingleObjEquiv.functor.map a = e a
<VAR>M : Type u<VAR>N : Type v<VAR>Monoid M<VAR>Monoid N<VAR>e : M ≃* N<GOAL>e.toSingleObjEquiv.unitIso.inv = CategoryTheory.eqToHom ⋯
<VAR>M : Type u<VAR>N : Type v<VAR>Monoid M<VAR>Monoid N<VAR>e : M ≃* N<VAR>a : CategoryTheory.SingleObj N<GOAL>e.toSingleObjEquiv.inverse.obj a = a
<VAR>M : Type u<VAR>N : Type v<VAR>Monoid M<VAR>Monoid N<VAR>e : M ≃* N<GOAL>∀ {X Y : CategoryTheory.SingleObj N} (a : N), e.toSingleObjEquiv.inverse.map a = e.symm a
<VAR>M : Type u<VAR>N : Type v<VAR>Monoid M<VAR>Monoid N<VAR>e : M ≃* N<GOAL>e.toSingleObjEquiv.counitIso.inv = CategoryTheory.eqToHom ⋯
<VAR>M : Type u<VAR>N : Type v<VAR>Monoid M<VAR>Monoid N<VAR>e : M ≃* N<VAR>a : CategoryTheory.SingleObj M<GOAL>e.toSingleObjEquiv.functor.obj a = a
<VAR>M : Type u<VAR>N : Type v<VAR>Monoid M<VAR>Monoid N<VAR>e : M ≃* N<GOAL>e.toSingleObjEquiv.unitIso.hom = CategoryTheory.eqToHom ⋯
<VAR>M : Type u<VAR>N : Type v<VAR>Monoid M<VAR>Monoid N<VAR>e : M ≃* N<GOAL>e.toSingleObjEquiv.counitIso.hom = CategoryTheory.eqToHom ⋯
<VAR>M : Type u<VAR>Monoid M<VAR>x : Mˣ<GOAL>((Units.toAut M) x).hom = (CategoryTheory.SingleObj.toEnd M) ↑x
<VAR>M : Type u<VAR>Monoid M<VAR>x : Mˣ<GOAL>((Units.toAut M) x).inv = (CategoryTheory.SingleObj.toEnd M) ↑x⁻¹
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>F₁ F₂ : CategoryTheory.Functor J C<VAR>j : J<GOAL>(F₁.chosenProd F₂).obj j = CategoryTheory.MonoidalCategory.tensorObj (F₁.obj j) (F₂.obj j)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>F₁ F₂ : CategoryTheory.Functor J C<GOAL>∀ {X Y : J} (φ : X ⟶ Y), (F₁.chosenProd F₂).map φ = CategoryTheory.MonoidalCategory.tensorHom (F₁.map φ) (F₂.map φ)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>F₁ F₂ : CategoryTheory.Functor J C<GOAL>∀ (x : J), (CategoryTheory.Functor.chosenProd.fst F₁ F₂).app x = CategoryTheory.ChosenFiniteProducts.fst (F₁.obj x) (F₂.obj x)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>F₁ F₂ : CategoryTheory.Functor J C<VAR>j : J<GOAL>(CategoryTheory.Functor.chosenProd.snd F₁ F₂).app j = CategoryTheory.ChosenFiniteProducts.snd (F₁.obj j) (F₂.obj j)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>F : CategoryTheory.Functor J C<VAR>j : J<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor F).hom.app j = (CategoryTheory.MonoidalCategory.leftUnitor (F.obj j)).hom
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>F : CategoryTheory.Functor J C<VAR>j : J<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor F).inv.app j = (CategoryTheory.MonoidalCategory.leftUnitor (F.obj j)).inv
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>F : CategoryTheory.Functor J C<VAR>j : J<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor F).hom.app j = (CategoryTheory.MonoidalCategory.rightUnitor (F.obj j)).hom
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>F : CategoryTheory.Functor J C<VAR>j : J<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor F).inv.app j = (CategoryTheory.MonoidalCategory.rightUnitor (F.obj j)).inv
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>F₁ F₁' F₂ F₂' : CategoryTheory.Functor J C<VAR>f : F₁ ⟶ F₁'<VAR>g : F₂ ⟶ F₂'<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.tensorHom f g).app j) (CategoryTheory.ChosenFiniteProducts.fst (F₁'.obj j) (F₂'.obj j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (F₁.obj j) (F₂.obj j)) (f.app j)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>F₁ F₁' F₂ F₂' : CategoryTheory.Functor J C<VAR>f : F₁ ⟶ F₁'<VAR>g : F₂ ⟶ F₂'<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.tensorHom f g).app j) (CategoryTheory.ChosenFiniteProducts.snd (F₁'.obj j) (F₂'.obj j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd (F₁.obj j) (F₂.obj j)) (g.app j)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>F₁ : CategoryTheory.Functor J C<VAR>F₂ F₂' : CategoryTheory.Functor J C<VAR>g : F₂ ⟶ F₂'<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.whiskerLeft F₁ g).app j) (CategoryTheory.ChosenFiniteProducts.fst (F₁.obj j) (F₂'.obj j)) = CategoryTheory.ChosenFiniteProducts.fst (F₁.obj j) (F₂.obj j)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>F₁ : CategoryTheory.Functor J C<VAR>F₂ F₂' : CategoryTheory.Functor J C<VAR>g : F₂ ⟶ F₂'<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.whiskerLeft F₁ g).app j) (CategoryTheory.ChosenFiniteProducts.snd (F₁.obj j) (F₂'.obj j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd (F₁.obj j) (F₂.obj j)) (g.app j)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>F₁ F₁' : CategoryTheory.Functor J C<VAR>f : F₁ ⟶ F₁'<VAR>F₂ : CategoryTheory.Functor J C<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.whiskerRight f F₂).app j) (CategoryTheory.ChosenFiniteProducts.fst (F₁'.obj j) (F₂.obj j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (F₁.obj j) (F₂.obj j)) (f.app j)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>F₁ F₁' : CategoryTheory.Functor J C<VAR>f : F₁ ⟶ F₁'<VAR>F₂ : CategoryTheory.Functor J C<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.whiskerRight f F₂).app j) (CategoryTheory.ChosenFiniteProducts.snd (F₁'.obj j) (F₂.obj j)) = CategoryTheory.ChosenFiniteProducts.snd (F₁.obj j) (F₂.obj j)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>F₁ F₂ F₃ : CategoryTheory.Functor J C<VAR>j : J<GOAL>(CategoryTheory.MonoidalCategory.associator F₁ F₂ F₃).hom.app j = (CategoryTheory.MonoidalCategory.associator (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>F₁ F₂ F₃ : CategoryTheory.Functor J C<VAR>j : J<GOAL>(CategoryTheory.MonoidalCategory.associator F₁ F₂ F₃).inv.app j = (CategoryTheory.MonoidalCategory.associator (F₁.obj j) (F₂.obj j) (F₃.obj j)).inv
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>self : CategoryTheory.Bicategory.Strict B<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>self : CategoryTheory.Bicategory.Strict B<VAR>a b : B<VAR>f : a ⟶ b<GOAL>CategoryTheory.Bicategory.rightUnitor f = CategoryTheory.eqToIso ⋯
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>self : CategoryTheory.Bicategory.Strict B<VAR>a b : B<VAR>f : a ⟶ b<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f = f
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>self : CategoryTheory.Bicategory.Strict B<VAR>a b : B<VAR>f : a ⟶ b<GOAL>CategoryTheory.Bicategory.leftUnitor f = CategoryTheory.eqToIso ⋯
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>self : CategoryTheory.Bicategory.Strict B<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>CategoryTheory.Bicategory.associator f g h = CategoryTheory.eqToIso ⋯
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>self : CategoryTheory.Bicategory.Strict B<VAR>a b : B<VAR>f : a ⟶ b<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b) = f
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g h : b ⟶ c<VAR>η : g = h<GOAL>CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.eqToHom η) = CategoryTheory.eqToHom ⋯
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f g : a ⟶ b<VAR>η : f = g<VAR>h : b ⟶ c<GOAL>CategoryTheory.Bicategory.whiskerRight (CategoryTheory.eqToHom η) h = CategoryTheory.eqToHom ⋯
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>self : CategoryTheory.Bicategory.HasLeftKanExtension f g<GOAL>CategoryTheory.Limits.HasInitial (CategoryTheory.Bicategory.LeftExtension f g)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>t : CategoryTheory.Bicategory.LeftExtension f g<VAR>H : t.IsKan<GOAL>CategoryTheory.Bicategory.HasLeftKanExtension f g
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>CategoryTheory.Bicategory.HasLeftKanExtension f g<GOAL>(CategoryTheory.Bicategory.lanLeftExtension f g).extension = CategoryTheory.Bicategory.lan f g
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>CategoryTheory.Bicategory.HasLeftKanExtension f g<GOAL>(CategoryTheory.Bicategory.lanLeftExtension f g).unit = CategoryTheory.Bicategory.lanUnit f g
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>CategoryTheory.Bicategory.HasLeftKanExtension f g<VAR>s : CategoryTheory.Bicategory.LeftExtension f g<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanUnit f g) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.lanDesc s)) = s.unit
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>CategoryTheory.Bicategory.HasLeftKanExtension f g<VAR>s : CategoryTheory.Bicategory.LeftExtension f g<GOAL>(CategoryTheory.Bicategory.lanIsKan f g).desc s = CategoryTheory.Bicategory.lanDesc s
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>CategoryTheory.Bicategory.HasLeftKanExtension f g<VAR>s : CategoryTheory.Bicategory.LeftExtension f g<GOAL>∃! τ, CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanUnit f g) (CategoryTheory.Bicategory.whiskerLeft f τ) = s.unit
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>CategoryTheory.Bicategory.HasLeftKanExtension f g<VAR>x : B<VAR>h : c ⟶ x<VAR>self : CategoryTheory.Bicategory.Lan.CommuteWith f g h<GOAL>Nonempty ((CategoryTheory.Bicategory.lanLeftExtension f g).whisker h).IsKan
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>CategoryTheory.Bicategory.HasLeftKanExtension f g<VAR>t : CategoryTheory.Bicategory.LeftExtension f g<VAR>x : B<VAR>h : c ⟶ x<VAR>H : (t.whisker h).IsKan<VAR>i : t.whisker h ≅ (CategoryTheory.Bicategory.lanLeftExtension f g).whisker h<GOAL>CategoryTheory.Bicategory.Lan.CommuteWith f g h
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>CategoryTheory.Bicategory.HasLeftKanExtension f g<VAR>x : B<VAR>h : c ⟶ x<VAR>CategoryTheory.Bicategory.HasLeftKanExtension f (CategoryTheory.CategoryStruct.comp g h)<VAR>i : CategoryTheory.Bicategory.lan f (CategoryTheory.CategoryStruct.comp g h) ≅ CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lan f g) h<VAR>w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanUnit f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.whiskerLeft f i.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.lanUnit f g) h) (CategoryTheory.Bicategory.associator f (CategoryTheory.Bicategory.lan f g) h).hom<GOAL>CategoryTheory.Bicategory.Lan.CommuteWith f g h
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>CategoryTheory.Bicategory.HasLeftKanExtension f g<VAR>x : B<VAR>h : c ⟶ x<VAR>CategoryTheory.Bicategory.Lan.CommuteWith f g h<GOAL>(CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker f g h).hom.right = CategoryTheory.Bicategory.lanDesc ((CategoryTheory.Bicategory.lanLeftExtension f g).whisker h)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>CategoryTheory.Bicategory.HasLeftKanExtension f g<VAR>x : B<VAR>h : c ⟶ x<VAR>CategoryTheory.Bicategory.Lan.CommuteWith f g h<GOAL>(CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker f g h).inv.right = (CategoryTheory.Bicategory.Lan.CommuteWith.isKan f g h).desc (CategoryTheory.Bicategory.lanLeftExtension f (CategoryTheory.CategoryStruct.comp g h))
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>CategoryTheory.Bicategory.HasLeftKanExtension f g<VAR>x : B<VAR>h : c ⟶ x<VAR>CategoryTheory.Bicategory.Lan.CommuteWith f g h<GOAL>(CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso f g h).inv = (CategoryTheory.Bicategory.Lan.CommuteWith.isKan f g h).desc (CategoryTheory.Bicategory.lanLeftExtension f (CategoryTheory.CategoryStruct.comp g h))
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>CategoryTheory.Bicategory.HasLeftKanExtension f g<VAR>x : B<VAR>h : c ⟶ x<VAR>CategoryTheory.Bicategory.Lan.CommuteWith f g h<GOAL>(CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso f g h).hom = CategoryTheory.Bicategory.lanDesc ((CategoryTheory.Bicategory.lanLeftExtension f g).whisker h)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>self : CategoryTheory.Bicategory.HasAbsLeftKanExtension f g<VAR>x : B<VAR>h : c ⟶ x<GOAL>CategoryTheory.Bicategory.Lan.CommuteWith f g h
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>t : CategoryTheory.Bicategory.LeftExtension f g<VAR>H : t.IsAbsKan<GOAL>CategoryTheory.Bicategory.HasAbsLeftKanExtension f g
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>self : CategoryTheory.Bicategory.HasLeftKanLift f g<GOAL>CategoryTheory.Limits.HasInitial (CategoryTheory.Bicategory.LeftLift f g)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>t : CategoryTheory.Bicategory.LeftLift f g<VAR>H : t.IsKan<GOAL>CategoryTheory.Bicategory.HasLeftKanLift f g
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>CategoryTheory.Bicategory.HasLeftKanLift f g<GOAL>(CategoryTheory.Bicategory.lanLiftLeftLift f g).lift = CategoryTheory.Bicategory.lanLift f g
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>CategoryTheory.Bicategory.HasLeftKanLift f g<GOAL>(CategoryTheory.Bicategory.lanLiftLeftLift f g).unit = CategoryTheory.Bicategory.lanLiftUnit f g
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>CategoryTheory.Bicategory.HasLeftKanLift f g<VAR>s : CategoryTheory.Bicategory.LeftLift f g<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanLiftUnit f g) (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.lanLiftDesc s) f) = s.unit
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>CategoryTheory.Bicategory.HasLeftKanLift f g<VAR>s : CategoryTheory.Bicategory.LeftLift f g<GOAL>(CategoryTheory.Bicategory.lanLiftIsKan f g).desc s = CategoryTheory.Bicategory.lanLiftDesc s
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>CategoryTheory.Bicategory.HasLeftKanLift f g<VAR>s : CategoryTheory.Bicategory.LeftLift f g<GOAL>∃! τ, CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanLiftUnit f g) (CategoryTheory.Bicategory.whiskerRight τ f) = s.unit
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>CategoryTheory.Bicategory.HasLeftKanLift f g<VAR>x : B<VAR>h : x ⟶ c<VAR>self : CategoryTheory.Bicategory.LanLift.CommuteWith f g h<GOAL>Nonempty ((CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h).IsKan
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>CategoryTheory.Bicategory.HasLeftKanLift f g<VAR>t : CategoryTheory.Bicategory.LeftLift f g<VAR>x : B<VAR>h : x ⟶ c<VAR>H : (t.whisker h).IsKan<VAR>i : t.whisker h ≅ (CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h<GOAL>CategoryTheory.Bicategory.LanLift.CommuteWith f g h
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>CategoryTheory.Bicategory.HasLeftKanLift f g<VAR>x : B<VAR>h : x ⟶ c<VAR>CategoryTheory.Bicategory.HasLeftKanLift f (CategoryTheory.CategoryStruct.comp h g)<VAR>i : CategoryTheory.Bicategory.lanLift f (CategoryTheory.CategoryStruct.comp h g) ≅ CategoryTheory.CategoryStruct.comp h (CategoryTheory.Bicategory.lanLift f g)<VAR>w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.lanLiftUnit f (CategoryTheory.CategoryStruct.comp h g)) (CategoryTheory.Bicategory.whiskerRight i.hom f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft h (CategoryTheory.Bicategory.lanLiftUnit f g)) (CategoryTheory.Bicategory.associator h (CategoryTheory.Bicategory.lanLift f g) f).inv<GOAL>CategoryTheory.Bicategory.LanLift.CommuteWith f g h
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>CategoryTheory.Bicategory.HasLeftKanLift f g<VAR>x : B<VAR>h : x ⟶ c<VAR>CategoryTheory.Bicategory.LanLift.CommuteWith f g h<GOAL>(CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker f g h).hom.right = CategoryTheory.Bicategory.lanLiftDesc ((CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>CategoryTheory.Bicategory.HasLeftKanLift f g<VAR>x : B<VAR>h : x ⟶ c<VAR>CategoryTheory.Bicategory.LanLift.CommuteWith f g h<GOAL>(CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker f g h).inv.right = (CategoryTheory.Bicategory.LanLift.CommuteWith.isKan f g h).desc (CategoryTheory.Bicategory.lanLiftLeftLift f (CategoryTheory.CategoryStruct.comp h g))
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>CategoryTheory.Bicategory.HasLeftKanLift f g<VAR>x : B<VAR>h : x ⟶ c<VAR>CategoryTheory.Bicategory.LanLift.CommuteWith f g h<GOAL>(CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso f g h).hom = CategoryTheory.Bicategory.lanLiftDesc ((CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>CategoryTheory.Bicategory.HasLeftKanLift f g<VAR>x : B<VAR>h : x ⟶ c<VAR>CategoryTheory.Bicategory.LanLift.CommuteWith f g h<GOAL>(CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso f g h).inv = (CategoryTheory.Bicategory.LanLift.CommuteWith.isKan f g h).desc (CategoryTheory.Bicategory.lanLiftLeftLift f (CategoryTheory.CategoryStruct.comp h g))
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>self : CategoryTheory.Bicategory.HasAbsLeftKanLift f g<VAR>x : B<VAR>h : x ⟶ c<GOAL>CategoryTheory.Bicategory.LanLift.CommuteWith f g h
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>t : CategoryTheory.Bicategory.LeftLift f g<VAR>H : t.IsAbsKan<GOAL>CategoryTheory.Bicategory.HasAbsLeftKanLift f g
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>t : CategoryTheory.Bicategory.LeftExtension f g<VAR>H : t.IsKan<VAR>s : CategoryTheory.Bicategory.LeftExtension f g<GOAL>CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.Bicategory.whiskerLeft f (H.desc s)) = s.unit
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>t : CategoryTheory.Bicategory.LeftExtension f g<VAR>H : t.IsKan<VAR>k : b ⟶ c<VAR>τ τ' : t.extension ⟶ k<VAR>w : CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.Bicategory.whiskerLeft f τ) = CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.Bicategory.whiskerLeft f τ')<GOAL>τ = τ'
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>s t : CategoryTheory.Bicategory.LeftExtension f g<VAR>P : s.IsKan<VAR>Q : t.IsKan<GOAL>(P.uniqueUpToIso Q).hom.right = P.desc t
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : a ⟶ c<VAR>s t : CategoryTheory.Bicategory.LeftExtension f g<VAR>P : s.IsKan<VAR>Q : t.IsKan<GOAL>(P.uniqueUpToIso Q).inv.right = Q.desc s
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>t : CategoryTheory.Bicategory.LeftLift f g<VAR>H : t.IsKan<VAR>s : CategoryTheory.Bicategory.LeftLift f g<GOAL>CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.Bicategory.whiskerRight (H.desc s) f) = s.unit
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>t : CategoryTheory.Bicategory.LeftLift f g<VAR>H : t.IsKan<VAR>k : c ⟶ b<VAR>τ τ' : t.lift ⟶ k<VAR>w : CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.Bicategory.whiskerRight τ f) = CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.Bicategory.whiskerRight τ' f)<GOAL>τ = τ'
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>s t : CategoryTheory.Bicategory.LeftLift f g<VAR>P : s.IsKan<VAR>Q : t.IsKan<GOAL>(P.uniqueUpToIso Q).hom.right = P.desc t
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : b ⟶ a<VAR>g : c ⟶ a<VAR>s t : CategoryTheory.Bicategory.LeftLift f g<VAR>P : s.IsKan<VAR>Q : t.IsKan<GOAL>(P.uniqueUpToIso Q).inv.right = Q.desc s
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (𝟙_ C) f) (CategoryTheory.MonoidalCategory.leftUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom f
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X (𝟙_ C) Y).hom (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.leftUnitor Y).hom) = CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.rightUnitor X).hom Y
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f (𝟙_ C)) (CategoryTheory.MonoidalCategory.rightUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).hom f