ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>X : (C × D)ᵒᵖ<GOAL>(CategoryTheory.prodOpEquiv C).functor.obj X = (Opposite.op (Opposite.unop X).1, Opposite.op (Opposite.unop X).2)
<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<GOAL>∀ {X Y : (C × D)ᵒᵖ} (f : X ⟶ Y), (CategoryTheory.prodOpEquiv C).functor.map f = (f.unop.1.op, f.unop.2.op)
<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<GOAL>(CategoryTheory.prodOpEquiv C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (C × D)ᵒᵖ)
<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<GOAL>∀ {X Y : Cᵒᵖ × Dᵒᵖ} (x : X ⟶ Y), (CategoryTheory.prodOpEquiv C).inverse.map x = match x with | (f, g) => Opposite.op (f.unop, g.unop)
<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<GOAL>(CategoryTheory.prodOpEquiv C).counitIso = CategoryTheory.Iso.refl ({ obj := fun x => match x with | (X, Y) => Opposite.op (Opposite.unop X, Opposite.unop Y), map := fun {X Y} x => match x with | (f, g) => Opposite.op (f.unop, g.unop), map_id := ⋯, map_comp := ⋯ }.comp { obj := fun X => (Opposite.op (Opposite.unop X).1, Opposite.op (Opposite.unop X).2), map := fun {X Y} f => (f.unop.1.op, f.unop.2.op), map_id := ⋯, map_comp := ⋯ })
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>X : T.Algebra<GOAL>(CategoryTheory.Monad.FreeCoequalizer.topMap X).f = T.map X.a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>X : T.Algebra<GOAL>(CategoryTheory.Monad.FreeCoequalizer.bottomMap X).f = T.μ.app X.A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>X : T.Algebra<GOAL>(CategoryTheory.Monad.FreeCoequalizer.π X).f = X.a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>X : T.Algebra<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Monad.FreeCoequalizer.topMap X) (CategoryTheory.Monad.FreeCoequalizer.π X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Monad.FreeCoequalizer.bottomMap X) (CategoryTheory.Monad.FreeCoequalizer.π X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>X : T.Algebra<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingParallelPair), (CategoryTheory.Monad.beckAlgebraCofork X).ι.app X_1 = CategoryTheory.Limits.WalkingParallelPair.rec (CategoryTheory.CategoryStruct.comp (CategoryTheory.Monad.FreeCoequalizer.topMap X) (CategoryTheory.Monad.FreeCoequalizer.π X)) (CategoryTheory.Monad.FreeCoequalizer.π X) X_1
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>X : T.Algebra<GOAL>(CategoryTheory.Monad.beckAlgebraCofork X).pt = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>X : T.Algebra<GOAL>(CategoryTheory.Monad.beckCofork X).pt = X.A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>X : T.Algebra<GOAL>(CategoryTheory.Monad.beckCofork X).π = X.a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>X : T.Algebra<VAR>s : CategoryTheory.Limits.Cofork (T.map X.a) (T.μ.app X.A)<GOAL>(CategoryTheory.Monad.beckCoequalizer X).desc s = CategoryTheory.CategoryStruct.comp (T.η.app X.A) s.π
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>X : C<VAR>Y : D<VAR>f : Sum.inl X ⟶ Sum.inr Y<GOAL>False
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>X : C<VAR>Y : D<VAR>f : Sum.inr X ⟶ Sum.inl Y<GOAL>False
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>P Q R : C<VAR>f : Sum.inl P ⟶ Sum.inl Q<VAR>g : Sum.inl Q ⟶ Sum.inl R<GOAL>CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>P Q R : D<VAR>f : Sum.inr P ⟶ Sum.inr Q<VAR>g : Sum.inr Q ⟶ Sum.inr R<GOAL>CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Sum.inl_ C D).map f = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>X : C<GOAL>(CategoryTheory.Sum.inl_ C D).obj X = Sum.inl X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Sum.inr_ C D).map f = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>X : D<GOAL>(CategoryTheory.Sum.inr_ C D).obj X = Sum.inr X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>X : C<GOAL>(CategoryTheory.Sum.swap C D).obj (Sum.inl X) = Sum.inr X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>X : D<GOAL>(CategoryTheory.Sum.swap C D).obj (Sum.inr X) = Sum.inl X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>X Y : C<VAR>f : Sum.inl X ⟶ Sum.inl Y<GOAL>(CategoryTheory.Sum.swap C D).map f = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>X Y : D<VAR>f : Sum.inr X ⟶ Sum.inr Y<GOAL>(CategoryTheory.Sum.swap C D).map f = f
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>F : CategoryTheory.Functor A C<VAR>G : CategoryTheory.Functor B C<VAR>X : A<GOAL>(F.inlCompSum' G).hom.app X = CategoryTheory.CategoryStruct.id ((F.sum' G).obj (Sum.inl X))
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>F : CategoryTheory.Functor A C<VAR>G : CategoryTheory.Functor B C<VAR>X : A<GOAL>(F.inlCompSum' G).inv.app X = CategoryTheory.CategoryStruct.id ((F.sum' G).obj (Sum.inl X))
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>F : CategoryTheory.Functor A C<VAR>G : CategoryTheory.Functor B C<VAR>X : B<GOAL>(F.inrCompSum' G).hom.app X = CategoryTheory.CategoryStruct.id ((F.sum' G).obj (Sum.inr X))
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>F : CategoryTheory.Functor A C<VAR>G : CategoryTheory.Functor B C<VAR>X : B<GOAL>(F.inrCompSum' G).inv.app X = CategoryTheory.CategoryStruct.id ((F.sum' G).obj (Sum.inr X))
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>F : CategoryTheory.Functor A B<VAR>G : CategoryTheory.Functor C D<VAR>a : A<GOAL>(F.sum G).obj (Sum.inl a) = Sum.inl (F.obj a)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>F : CategoryTheory.Functor A B<VAR>G : CategoryTheory.Functor C D<VAR>c : C<GOAL>(F.sum G).obj (Sum.inr c) = Sum.inr (G.obj c)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>F : CategoryTheory.Functor A B<VAR>G : CategoryTheory.Functor C D<VAR>a a' : A<VAR>f : Sum.inl a ⟶ Sum.inl a'<GOAL>(F.sum G).map f = F.map f
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>F : CategoryTheory.Functor A B<VAR>G : CategoryTheory.Functor C D<VAR>c c' : C<VAR>f : Sum.inr c ⟶ Sum.inr c'<GOAL>(F.sum G).map f = G.map f
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>F G : CategoryTheory.Functor A B<VAR>H I : CategoryTheory.Functor C D<VAR>α : F ⟶ G<VAR>β : H ⟶ I<VAR>a : A<GOAL>(CategoryTheory.NatTrans.sum α β).app (Sum.inl a) = α.app a
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} B<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>F G : CategoryTheory.Functor A B<VAR>H I : CategoryTheory.Functor C D<VAR>α : F ⟶ G<VAR>β : H ⟶ I<VAR>c : C<GOAL>(CategoryTheory.NatTrans.sum α β).app (Sum.inr c) = β.app c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>T : CategoryTheory.Monad C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Kleisli.Adjunction.toKleisli T).map f = CategoryTheory.CategoryStruct.comp f (T.η.app Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>T : CategoryTheory.Monad C<VAR>X : C<GOAL>(CategoryTheory.Kleisli.Adjunction.toKleisli T).obj X = X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>T : CategoryTheory.Monad C<GOAL>∀ {x Y : CategoryTheory.Kleisli T} (f : x ⟶ Y), (CategoryTheory.Kleisli.Adjunction.fromKleisli T).map f = CategoryTheory.CategoryStruct.comp (T.map f) (T.μ.app Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>T : CategoryTheory.Monad C<VAR>X : CategoryTheory.Kleisli T<GOAL>(CategoryTheory.Kleisli.Adjunction.fromKleisli T).obj X = T.obj X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>U : CategoryTheory.Comonad C<VAR>X : C<GOAL>(CategoryTheory.Cokleisli.Adjunction.toCokleisli U).obj X = X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>U : CategoryTheory.Comonad C<VAR>X : C<GOAL>∀ {x : C} (f : X ⟶ x), (CategoryTheory.Cokleisli.Adjunction.toCokleisli U).map f = CategoryTheory.CategoryStruct.comp (U.ε.app X) f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>U : CategoryTheory.Comonad C<VAR>X : CategoryTheory.Cokleisli U<GOAL>∀ {x : CategoryTheory.Cokleisli U} (f : X ⟶ x), (CategoryTheory.Cokleisli.Adjunction.fromCokleisli U).map f = CategoryTheory.CategoryStruct.comp (U.δ.app X) (U.map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>U : CategoryTheory.Comonad C<VAR>X : CategoryTheory.Cokleisli U<GOAL>(CategoryTheory.Cokleisli.Adjunction.fromCokleisli U).obj X = U.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Comonad C<VAR>X : T.Coalgebra<GOAL>(CategoryTheory.Comonad.CofreeEqualizer.topMap X).f = T.map X.a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Comonad C<VAR>X : T.Coalgebra<GOAL>(CategoryTheory.Comonad.CofreeEqualizer.bottomMap X).f = T.δ.app X.A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Comonad C<VAR>X : T.Coalgebra<GOAL>(CategoryTheory.Comonad.CofreeEqualizer.ι X).f = X.a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Comonad C<VAR>X : T.Coalgebra<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Comonad.CofreeEqualizer.ι X) (CategoryTheory.Comonad.CofreeEqualizer.topMap X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Comonad.CofreeEqualizer.ι X) (CategoryTheory.Comonad.CofreeEqualizer.bottomMap X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Comonad C<VAR>X : T.Coalgebra<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingParallelPair), (CategoryTheory.Comonad.beckCoalgebraFork X).π.app X_1 = CategoryTheory.Limits.WalkingParallelPair.rec (motive := fun t => X_1 = t → (X ⟶ (CategoryTheory.Limits.parallelPair (CategoryTheory.Comonad.CofreeEqualizer.topMap X) (CategoryTheory.Comonad.CofreeEqualizer.bottomMap X)).obj X_1)) (fun h => ⋯ ▸ CategoryTheory.Comonad.CofreeEqualizer.ι X) (fun h => ⋯ ▸ CategoryTheory.CategoryStruct.comp (CategoryTheory.Comonad.CofreeEqualizer.ι X) (CategoryTheory.Comonad.CofreeEqualizer.topMap X)) X_1 ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Comonad C<VAR>X : T.Coalgebra<GOAL>(CategoryTheory.Comonad.beckCoalgebraFork X).pt = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Comonad C<VAR>X : T.Coalgebra<GOAL>(CategoryTheory.Comonad.beckFork X).pt = X.A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Comonad C<VAR>X : T.Coalgebra<GOAL>(CategoryTheory.Comonad.beckFork X).ι = X.a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Comonad C<VAR>X : T.Coalgebra<VAR>s : CategoryTheory.Limits.Fork (T.map X.a) (T.δ.app X.A)<GOAL>(CategoryTheory.Comonad.beckEqualizer X).lift s = CategoryTheory.CategoryStruct.comp s.ι (T.ε.app X.A)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<GOAL>(X.tensorObj Y).src = (X.src ⨯ Y.src)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<GOAL>(X.tensorObj Y).tgt = (X.tgt ⨯ Y.tgt)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<GOAL>(X.tensorObj Y).rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst)).obj X.rel ⊓ (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)).obj Y.rel
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X₁ X₂ Y₁ Y₂ : CategoryTheory.Dial C<VAR>f : X₁ ⟶ X₂<VAR>g : Y₁ ⟶ Y₂<GOAL>(CategoryTheory.Dial.tensorHom f g).F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) f.F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) g.F)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X₁ X₂ Y₁ Y₂ : CategoryTheory.Dial C<VAR>f : X₁ ⟶ X₂<VAR>g : Y₁ ⟶ Y₂<GOAL>(CategoryTheory.Dial.tensorHom f g).f = CategoryTheory.Limits.prod.map f.f g.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<GOAL>CategoryTheory.Dial.tensorUnit.rel = ⊤
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<GOAL>CategoryTheory.Dial.tensorUnit.src = ⊤_ C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<GOAL>CategoryTheory.Dial.tensorUnit.tgt = ⊤_ C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>X.leftUnitor.hom.F = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.terminal.from (((⊤_ C) ⨯ X.src) ⨯ X.tgt)) CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>X.leftUnitor.inv.F = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>X.leftUnitor.inv.f = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.terminal.from X.src) (CategoryTheory.CategoryStruct.id X.src)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>X.leftUnitor.hom.f = CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>X.rightUnitor.hom.F = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd (CategoryTheory.Limits.terminal.from ((X.src ⨯ ⊤_ C) ⨯ X.tgt))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>X.rightUnitor.hom.f = CategoryTheory.Limits.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>X.rightUnitor.inv.F = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>X.rightUnitor.inv.f = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X.src) (CategoryTheory.Limits.terminal.from X.src)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : CategoryTheory.Dial C<GOAL>(X.associator Y Z).inv.F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst)) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : CategoryTheory.Dial C<GOAL>(X.associator Y Z).hom.F = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst))) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : CategoryTheory.Dial C<GOAL>(X.associator Y Z).hom.f = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) CategoryTheory.Limits.prod.snd)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : CategoryTheory.Dial C<GOAL>(X.associator Y Z).inv.f = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).hom.F = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.terminal.from (((⊤_ C) ⨯ X.src) ⨯ X.tgt)) CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).inv.F = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<GOAL>(𝟙_ (CategoryTheory.Dial C)).tgt = ⊤_ C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<GOAL>∀ {X₁ Y₁ X₂ Y₂ : CategoryTheory.Dial C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), (CategoryTheory.MonoidalCategory.tensorHom f g).f = CategoryTheory.Limits.prod.map f.f g.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).inv.f = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.terminal.from X.src) (CategoryTheory.CategoryStruct.id X.src)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).hom.F = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd (CategoryTheory.Limits.terminal.from ((X.src ⨯ ⊤_ C) ⨯ X.tgt))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : CategoryTheory.Dial C<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).hom.F = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst))) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<GOAL>(CategoryTheory.MonoidalCategory.tensorObj X Y).tgt = (X.tgt ⨯ Y.tgt)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : CategoryTheory.Dial C<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).hom.f = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) CategoryTheory.Limits.prod.snd)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).inv.F = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<GOAL>(CategoryTheory.MonoidalCategory.tensorObj X Y).src = (X.src ⨯ Y.src)