ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Mul α<VAR>a b : αᵃᵒᵖ<GOAL>AddOpposite.unop (a * b) = AddOpposite.unop a * AddOpposite.unop b
<VAR>α : Type u_1<VAR>Inv α<VAR>a : α<GOAL>AddOpposite.op a⁻¹ = (AddOpposite.op a)⁻¹
<VAR>α : Type u_1<VAR>Inv α<VAR>a : αᵃᵒᵖ<GOAL>AddOpposite.unop a⁻¹ = (AddOpposite.unop a)⁻¹
<VAR>α : Type u_1<VAR>Div α<VAR>a b : α<GOAL>AddOpposite.op (a / b) = AddOpposite.op a / AddOpposite.op b
<VAR>α : Type u_1<VAR>Div α<VAR>a b : αᵃᵒᵖ<GOAL>AddOpposite.unop (a / b) = AddOpposite.unop a / AddOpposite.unop b
<VAR>B : Type u<VAR>Quiver B<VAR>a b : CategoryTheory.FreeBicategory B<VAR>f g h : a ⟶ b<VAR>η : CategoryTheory.FreeBicategory.Hom₂ f g<VAR>θ : CategoryTheory.FreeBicategory.Hom₂ g h<GOAL>(η.vcomp θ).mk = CategoryTheory.CategoryStruct.comp η.mk θ.mk
<VAR>B : Type u<VAR>Quiver B<VAR>a b c : CategoryTheory.FreeBicategory B<VAR>f : a ⟶ b<VAR>g h : b ⟶ c<VAR>η : CategoryTheory.FreeBicategory.Hom₂ g h<GOAL>(CategoryTheory.FreeBicategory.Hom₂.whisker_left f η).mk = CategoryTheory.Bicategory.whiskerLeft f η.mk
<VAR>B : Type u<VAR>Quiver B<VAR>a b c : CategoryTheory.FreeBicategory B<VAR>f g : a ⟶ b<VAR>η : CategoryTheory.FreeBicategory.Hom₂ f g<VAR>h : b ⟶ c<GOAL>(CategoryTheory.FreeBicategory.Hom₂.whisker_right h η).mk = CategoryTheory.Bicategory.whiskerRight η.mk h
<VAR>B : Type u<VAR>Quiver B<VAR>a b c : CategoryTheory.FreeBicategory B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>CategoryTheory.FreeBicategory.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g
<VAR>B : Type u<VAR>Quiver B<VAR>a b : CategoryTheory.FreeBicategory B<VAR>f : a ⟶ b<GOAL>Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.id f) = CategoryTheory.CategoryStruct.id f
<VAR>B : Type u<VAR>Quiver B<VAR>a b c d : CategoryTheory.FreeBicategory B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.associator f g h) = (CategoryTheory.Bicategory.associator f g h).hom
<VAR>B : Type u<VAR>Quiver B<VAR>a b c d : CategoryTheory.FreeBicategory B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.associator_inv f g h) = (CategoryTheory.Bicategory.associator f g h).inv
<VAR>B : Type u<VAR>Quiver B<VAR>a b : CategoryTheory.FreeBicategory B<VAR>f : a ⟶ b<GOAL>Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.left_unitor f) = (CategoryTheory.Bicategory.leftUnitor f).hom
<VAR>B : Type u<VAR>Quiver B<VAR>a b : CategoryTheory.FreeBicategory B<VAR>f : a ⟶ b<GOAL>Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.left_unitor_inv f) = (CategoryTheory.Bicategory.leftUnitor f).inv
<VAR>B : Type u<VAR>Quiver B<VAR>a b : CategoryTheory.FreeBicategory B<VAR>f : a ⟶ b<GOAL>Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.right_unitor f) = (CategoryTheory.Bicategory.rightUnitor f).hom
<VAR>B : Type u<VAR>Quiver B<VAR>a b : CategoryTheory.FreeBicategory B<VAR>f : a ⟶ b<GOAL>Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.right_unitor_inv f) = (CategoryTheory.Bicategory.rightUnitor f).inv
<VAR>B : Type u<VAR>Quiver B<GOAL>∀ (x x_1 : B) (f : x ⟶ x_1), CategoryTheory.FreeBicategory.of.map f = CategoryTheory.FreeBicategory.Hom.of f
<VAR>B : Type u<VAR>Quiver B<VAR>a : B<GOAL>CategoryTheory.FreeBicategory.of.obj a = id a
<VAR>B : Type u₁<VAR>Quiver B<VAR>C : Type u₂<VAR>CategoryTheory.CategoryStruct.{v₂, u₂} C<VAR>F : B ⥤q C<VAR>a : CategoryTheory.FreeBicategory B<GOAL>CategoryTheory.FreeBicategory.liftHom F (CategoryTheory.CategoryStruct.id a) = CategoryTheory.CategoryStruct.id (F.obj a)
<VAR>B : Type u₁<VAR>Quiver B<VAR>C : Type u₂<VAR>CategoryTheory.CategoryStruct.{v₂, u₂} C<VAR>F : B ⥤q C<VAR>a b c : CategoryTheory.FreeBicategory B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>CategoryTheory.FreeBicategory.liftHom F (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeBicategory.liftHom F f) (CategoryTheory.FreeBicategory.liftHom F g)
<VAR>B : Type u₁<VAR>Quiver B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : B ⥤q C<VAR>a b : CategoryTheory.FreeBicategory B<VAR>f g : a ⟶ b<VAR>η θ : CategoryTheory.FreeBicategory.Hom₂ f g<VAR>H : CategoryTheory.FreeBicategory.Rel η θ<GOAL>CategoryTheory.FreeBicategory.liftHom₂ F η = CategoryTheory.FreeBicategory.liftHom₂ F θ
<VAR>B : Type u₁<VAR>Quiver B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : B ⥤q C<GOAL>∀ {a b c : CategoryTheory.FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c), (CategoryTheory.FreeBicategory.lift F).mapComp f g = CategoryTheory.Iso.refl ({ obj := F.obj, map := fun {X Y} => CategoryTheory.FreeBicategory.liftHom F, map₂ := fun {a b} {f g} => Quot.lift (CategoryTheory.FreeBicategory.liftHom₂ F) ⋯, map₂_id := ⋯, map₂_comp := ⋯ }.map (CategoryTheory.CategoryStruct.comp f g))
<VAR>B : Type u₁<VAR>Quiver B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : B ⥤q C<GOAL>∀ {a b : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} (a_1 : Quot CategoryTheory.FreeBicategory.Rel), (CategoryTheory.FreeBicategory.lift F).map₂ a_1 = Quot.lift (CategoryTheory.FreeBicategory.liftHom₂ F) ⋯ a_1
<VAR>B : Type u₁<VAR>Quiver B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : B ⥤q C<VAR>a : CategoryTheory.FreeBicategory B<GOAL>(CategoryTheory.FreeBicategory.lift F).mapId a = CategoryTheory.Iso.refl ({ obj := F.obj, map := fun {X Y} => CategoryTheory.FreeBicategory.liftHom F, map₂ := fun {a b} {f g} => Quot.lift (CategoryTheory.FreeBicategory.liftHom₂ F) ⋯, map₂_id := ⋯, map₂_comp := ⋯ }.map (CategoryTheory.CategoryStruct.id a))
<VAR>B : Type u₁<VAR>Quiver B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : B ⥤q C<GOAL>∀ (a : B), (CategoryTheory.FreeBicategory.lift F).obj a = F.obj a
<VAR>B : Type u₁<VAR>Quiver B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : B ⥤q C<GOAL>∀ {X Y : CategoryTheory.FreeBicategory B} (a : X ⟶ Y), (CategoryTheory.FreeBicategory.lift F).map a = CategoryTheory.FreeBicategory.liftHom F a
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>self : CategoryTheory.Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom = CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.id b)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapId b).hom) (CategoryTheory.Bicategory.rightUnitor (self.map f)).hom)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>self : CategoryTheory.Pseudofunctor B C<VAR>a b c : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<VAR>h : b ⟶ c<GOAL>self.map₂ (CategoryTheory.Bicategory.whiskerRight η h) = CategoryTheory.CategoryStruct.comp (self.mapComp f h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map h)) (self.mapComp g h).inv)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>self : CategoryTheory.Pseudofunctor B C<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g h : b ⟶ c<VAR>η : g ⟶ h<GOAL>self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η) = CategoryTheory.CategoryStruct.comp (self.mapComp f g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.map₂ η)) (self.mapComp f h).inv)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>self : CategoryTheory.Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.id a) f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a).hom (self.map f)) (CategoryTheory.Bicategory.leftUnitor (self.map f)).hom)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>self : CategoryTheory.Pseudofunctor B C<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>self.map₂ (CategoryTheory.Bicategory.associator f g h).hom = CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g).hom (self.map h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h).inv) (self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv)))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<GOAL>F.toOplax.toPrelaxFunctor = F.toPrelaxFunctor
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<GOAL>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), F.toOplax.mapComp f g = (F.mapComp f g).hom
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>a : B<GOAL>F.toOplax.mapId a = (F.mapId a).hom
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<GOAL>F.toLax.toPrelaxFunctor = F.toPrelaxFunctor
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<GOAL>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), F.toLax.mapComp f g = (F.mapComp f g).inv
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>a : B<GOAL>F.toLax.mapId a = (F.mapId a).inv
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<GOAL>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (CategoryTheory.Pseudofunctor.id B).mapComp f g = CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.comp f g)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<GOAL>(CategoryTheory.Pseudofunctor.id B).toPrelaxFunctor = CategoryTheory.PrelaxFunctor.id B
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>a : B<GOAL>(CategoryTheory.Pseudofunctor.id B).mapId a = CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.id a)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>D : Type u₃<VAR>CategoryTheory.Bicategory D<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>G : CategoryTheory.Pseudofunctor C D<VAR>a : B<GOAL>(F.comp G).mapId a = G.map₂Iso (F.mapId a) ≪≫ G.mapId (F.obj a)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>D : Type u₃<VAR>CategoryTheory.Bicategory D<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>G : CategoryTheory.Pseudofunctor C D<GOAL>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (F.comp G).mapComp f g = G.map₂Iso (F.mapComp f g) ≪≫ G.mapComp (F.map f) (F.map g)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>D : Type u₃<VAR>CategoryTheory.Bicategory D<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>G : CategoryTheory.Pseudofunctor C D<GOAL>(F.comp G).toPrelaxFunctor = F.comp G.toPrelaxFunctor
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).hom (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h).hom) = CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h).inv) (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).hom (F.map h)) (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).hom))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).hom (F.map h)) = CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h).hom) (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h).hom) (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).inv))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h).inv) (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).inv (F.map h)) (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).inv (F.map₂ (CategoryTheory.Bicategory.associator f g h).hom)))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).inv (F.map h)) (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h).inv) (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv (F.map₂ (CategoryTheory.Bicategory.associator f g h).inv)))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>(F.mapComp (CategoryTheory.CategoryStruct.id a) f).hom = CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv (CategoryTheory.Bicategory.whiskerRight (F.mapId a).inv (F.map f)))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>F.mapComp (CategoryTheory.CategoryStruct.id a) f = F.map₂Iso (CategoryTheory.Bicategory.leftUnitor f) ≪≫ (CategoryTheory.Bicategory.leftUnitor (F.map f)).symm ≪≫ (CategoryTheory.Bicategory.whiskerRightIso (F.mapId a) (F.map f)).symm
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>(F.mapComp (CategoryTheory.CategoryStruct.id a) f).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a).hom (F.map f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>CategoryTheory.Bicategory.whiskerRightIso (F.mapId a) (F.map f) = (F.mapComp (CategoryTheory.CategoryStruct.id a) f).symm ≪≫ F.map₂Iso (CategoryTheory.Bicategory.leftUnitor f) ≪≫ (CategoryTheory.Bicategory.leftUnitor (F.map f)).symm
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>CategoryTheory.Bicategory.whiskerRight (F.mapId a).hom (F.map f) = CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.id a) f).inv (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom) (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>CategoryTheory.Bicategory.whiskerRight (F.mapId a).inv (F.map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv) (F.mapComp (CategoryTheory.CategoryStruct.id a) f).hom)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>(F.mapComp f (CategoryTheory.CategoryStruct.id b)).hom = CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b).inv))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>F.mapComp f (CategoryTheory.CategoryStruct.id b) = F.map₂Iso (CategoryTheory.Bicategory.rightUnitor f) ≪≫ (CategoryTheory.Bicategory.rightUnitor (F.map f)).symm ≪≫ (CategoryTheory.Bicategory.whiskerLeftIso (F.map f) (F.mapId b)).symm
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>(F.mapComp f (CategoryTheory.CategoryStruct.id b)).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>CategoryTheory.Bicategory.whiskerLeftIso (F.map f) (F.mapId b) = (F.mapComp f (CategoryTheory.CategoryStruct.id b)).symm ≪≫ F.map₂Iso (CategoryTheory.Bicategory.rightUnitor f) ≪≫ (CategoryTheory.Bicategory.rightUnitor (F.map f)).symm
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b).hom = CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.id b)).inv (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom) (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv) (F.mapComp f (CategoryTheory.CategoryStruct.id b)).hom)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.OplaxFunctor B C<VAR>F' : F.PseudoCore<GOAL>(CategoryTheory.Pseudofunctor.mkOfOplax F F').toPrelaxFunctor = F.toPrelaxFunctor
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.OplaxFunctor B C<VAR>F' : F.PseudoCore<GOAL>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (CategoryTheory.Pseudofunctor.mkOfOplax F F').mapComp f g = F'.mapCompIso f g
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.OplaxFunctor B C<VAR>F' : F.PseudoCore<VAR>a : B<GOAL>(CategoryTheory.Pseudofunctor.mkOfOplax F F').mapId a = F'.mapIdIso a
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.OplaxFunctor B C<VAR>∀ (a : B), CategoryTheory.IsIso (F.mapId a)<VAR>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)<GOAL>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), ((CategoryTheory.Pseudofunctor.mkOfOplax' F).mapComp f g).hom = F.mapComp f g
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.OplaxFunctor B C<VAR>∀ (a : B), CategoryTheory.IsIso (F.mapId a)<VAR>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)<GOAL>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), ((CategoryTheory.Pseudofunctor.mkOfOplax' F).mapComp f g).inv = CategoryTheory.inv (F.mapComp f g)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.OplaxFunctor B C<VAR>∀ (a : B), CategoryTheory.IsIso (F.mapId a)<VAR>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)<VAR>a : B<GOAL>((CategoryTheory.Pseudofunctor.mkOfOplax' F).mapId a).hom = F.mapId a
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.OplaxFunctor B C<VAR>∀ (a : B), CategoryTheory.IsIso (F.mapId a)<VAR>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)<GOAL>(CategoryTheory.Pseudofunctor.mkOfOplax' F).toPrelaxFunctor = F.toPrelaxFunctor
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.OplaxFunctor B C<VAR>∀ (a : B), CategoryTheory.IsIso (F.mapId a)<VAR>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)<VAR>a : B<GOAL>((CategoryTheory.Pseudofunctor.mkOfOplax' F).mapId a).inv = CategoryTheory.inv (F.mapId a)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.LaxFunctor B C<VAR>F' : F.PseudoCore<VAR>a : B<GOAL>(CategoryTheory.Pseudofunctor.mkOfLax F F').mapId a = F'.mapIdIso a
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.LaxFunctor B C<VAR>F' : F.PseudoCore<GOAL>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (CategoryTheory.Pseudofunctor.mkOfLax F F').mapComp f g = F'.mapCompIso f g
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.LaxFunctor B C<VAR>F' : F.PseudoCore<GOAL>(CategoryTheory.Pseudofunctor.mkOfLax F F').toPrelaxFunctor = F.toPrelaxFunctor
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.LaxFunctor B C<VAR>∀ (a : B), CategoryTheory.IsIso (F.mapId a)<VAR>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)<VAR>a : B<GOAL>((CategoryTheory.Pseudofunctor.mkOfLax' F).mapId a).inv = F.mapId a
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.LaxFunctor B C<VAR>∀ (a : B), CategoryTheory.IsIso (F.mapId a)<VAR>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)<GOAL>(CategoryTheory.Pseudofunctor.mkOfLax' F).toPrelaxFunctor = F.toPrelaxFunctor
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.LaxFunctor B C<VAR>∀ (a : B), CategoryTheory.IsIso (F.mapId a)<VAR>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)<GOAL>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), ((CategoryTheory.Pseudofunctor.mkOfLax' F).mapComp f g).inv = F.mapComp f g