ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ C<GOAL>∀ {X Y : CategoryTheory.Discrete PUnit.{u + 1}} (x : X ⟶ Y), ((Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).obj A).map x = 𝟙 ((fun x => A.X) X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ C<GOAL>∀ (x x_1 : CategoryTheory.Discrete PUnit.{u + 1}), ((Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).obj A).μ x x_1 = A.mul
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>∀ {X Y : Mon_ C} (f : X ⟶ Y) (x : CategoryTheory.Discrete PUnit.{u + 1}), ((Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).map f).app x = f.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ C<GOAL>∀ (x : CategoryTheory.Discrete PUnit.{u + 1}), ((Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).obj A).obj x = A.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ C<GOAL>((Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).obj A).ε = A.one
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C<GOAL>∀ (X_1 : CategoryTheory.Discrete PUnit.{u + 1}), ((Mon_.EquivLaxMonoidalFunctorPUnit.unitIso C).inv.app X).app X_1 = 𝟙 (X.obj (𝟙_ (CategoryTheory.Discrete PUnit.{u + 1})))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C<GOAL>∀ (X_1 : CategoryTheory.Discrete PUnit.{u + 1}), ((Mon_.EquivLaxMonoidalFunctorPUnit.unitIso C).hom.app X).app X_1 = 𝟙 (X.obj X_1)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Mon_ C<GOAL>((Mon_.EquivLaxMonoidalFunctorPUnit.counitIso C).inv.app X).hom = 𝟙 X.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Mon_ C<GOAL>((Mon_.EquivLaxMonoidalFunctorPUnit.counitIso C).hom.app X).hom = 𝟙 X.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(Mon_.equivLaxMonoidalFunctorPUnit C).inverse = Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(Mon_.equivLaxMonoidalFunctorPUnit C).unitIso = Mon_.EquivLaxMonoidalFunctorPUnit.unitIso C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(Mon_.equivLaxMonoidalFunctorPUnit C).functor = Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(Mon_.equivLaxMonoidalFunctorPUnit C).counitIso = Mon_.EquivLaxMonoidalFunctorPUnit.counitIso C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M N P : Mon_ C<GOAL>((λ_ (𝟙_ C)).inv ≫ ((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one) ⊗ P.one)) ≫ (α_ M.X N.X P.X).hom = (λ_ (𝟙_ C)).inv ≫ (M.one ⊗ (λ_ (𝟙_ C)).inv ≫ (N.one ⊗ P.one))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M : Mon_ C<GOAL>((λ_ (𝟙_ C)).inv ≫ (𝟙 (𝟙_ C) ⊗ M.one)) ≫ (λ_ M.X).hom = M.one
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M : Mon_ C<GOAL>((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ 𝟙 (𝟙_ C))) ≫ (ρ_ M.X).hom = M.one
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>M N : Mon_ C<GOAL>((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one)) ▷ (M.X ⊗ N.X) ≫ CategoryTheory.tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul) = (λ_ (M.X ⊗ N.X)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>M N : Mon_ C<GOAL>(M.X ⊗ N.X) ◁ ((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one)) ≫ CategoryTheory.tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul) = (ρ_ (M.X ⊗ N.X)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>M N : Mon_ C<GOAL>(CategoryTheory.tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul)) ▷ (M.X ⊗ N.X) ≫ CategoryTheory.tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul) = (α_ (M.X ⊗ N.X) (M.X ⊗ N.X) (M.X ⊗ N.X)).hom ≫ (M.X ⊗ N.X) ◁ (CategoryTheory.tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul)) ≫ CategoryTheory.tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>M N P : Mon_ C<GOAL>(CategoryTheory.tensor_μ C (M.X ⊗ N.X, P.X) (M.X ⊗ N.X, P.X) ≫ (CategoryTheory.tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul) ⊗ P.mul)) ≫ (α_ M.X N.X P.X).hom = ((α_ M.X N.X P.X).hom ⊗ (α_ M.X N.X P.X).hom) ≫ CategoryTheory.tensor_μ C (M.X, N.X ⊗ P.X) (M.X, N.X ⊗ P.X) ≫ (M.mul ⊗ CategoryTheory.tensor_μ C (N.X, P.X) (N.X, P.X) ≫ (N.mul ⊗ P.mul))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>M : Mon_ C<GOAL>(CategoryTheory.tensor_μ C (𝟙_ C, M.X) (𝟙_ C, M.X) ≫ ((λ_ (𝟙_ C)).hom ⊗ M.mul)) ≫ (λ_ M.X).hom = ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ M.mul
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>M : Mon_ C<GOAL>(CategoryTheory.tensor_μ C (M.X, 𝟙_ C) (M.X, 𝟙_ C) ≫ (M.mul ⊗ (λ_ (𝟙_ C)).hom)) ≫ (ρ_ M.X).hom = ((ρ_ M.X).hom ⊗ (ρ_ M.X).hom) ≫ M.mul
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>M N : Mon_ C<GOAL>(M ⊗ N).X = M.X ⊗ N.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>∀ {X₁ Y₁ X₂ Y₂ : Mon_ C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), (f ⊗ g).hom = f.hom ⊗ g.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(𝟙_ (Mon_ C)).X = 𝟙_ C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(𝟙_ (Mon_ C)).one = 𝟙 (𝟙_ C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(𝟙_ (Mon_ C)).mul = (λ_ (𝟙_ C)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : Mon_ C<GOAL>(X ⊗ Y).one = (λ_ (𝟙_ C)).inv ≫ (X.one ⊗ Y.one)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : Mon_ C<GOAL>(X ⊗ Y).mul = CategoryTheory.tensor_μ C (X.X, Y.X) (X.X, Y.X) ≫ (X.mul ⊗ Y.mul)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : Mon_ C<VAR>f : X ⟶ Y<VAR>Z : Mon_ C<GOAL>(f ▷ Z).hom = f.hom ▷ Z.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : Mon_ C<VAR>Y Z : Mon_ C<VAR>f : Y ⟶ Z<GOAL>(X ◁ f).hom = X.X ◁ f.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : Mon_ C<GOAL>(λ_ X).hom.hom = (λ_ X.X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : Mon_ C<GOAL>(λ_ X).inv.hom = (λ_ X.X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : Mon_ C<GOAL>(ρ_ X).hom.hom = (ρ_ X.X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X : Mon_ C<GOAL>(ρ_ X).inv.hom = (ρ_ X.X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y Z : Mon_ C<GOAL>(α_ X Y Z).hom.hom = (α_ X.X Y.X Z.X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y Z : Mon_ C<GOAL>(α_ X Y Z).inv.hom = (α_ X.X Y.X Z.X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>M N : Mon_ C<GOAL>(M ⊗ N).one = (λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>M N : Mon_ C<GOAL>(M ⊗ N).mul = CategoryTheory.tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(Mon_.forgetMonoidal C).toFunctor = Mon_.forget C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(Mon_.forgetMonoidal C).ε = 𝟙 (𝟙_ C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : Mon_ C<GOAL>(Mon_.forgetMonoidal C).μ X Y = 𝟙 (X.X ⊗ Y.X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : Mon_ C<GOAL>(X ⊗ Y).one ≫ (β_ X.X Y.X).hom = (Y ⊗ X).one
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.SymmetricCategory C<VAR>X Y : Mon_ C<GOAL>(X ⊗ Y).mul ≫ (β_ X.X Y.X).hom = ((β_ X.X Y.X).hom ⊗ (β_ X.X Y.X).hom) ≫ (Y ⊗ X).mul
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>X : C<VAR>f g : X ⟶ 𝟙_ C<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>T X Y : C<VAR>f : T ⟶ X<VAR>g : T ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.lift f g) (CategoryTheory.ChosenFiniteProducts.fst X Y) = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>T X Y : C<VAR>f : T ⟶ X<VAR>g : T ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.lift f g) (CategoryTheory.ChosenFiniteProducts.snd X Y) = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>T X Y : C<VAR>f g : T ⟶ CategoryTheory.MonoidalCategory.tensorObj X Y<VAR>h_fst : CategoryTheory.CategoryStruct.comp f (CategoryTheory.ChosenFiniteProducts.fst X Y) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.ChosenFiniteProducts.fst X Y)<VAR>h_snd : CategoryTheory.CategoryStruct.comp f (CategoryTheory.ChosenFiniteProducts.snd X Y) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.ChosenFiniteProducts.snd X Y)<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>X₁ X₂ Y₁ Y₂ : C<VAR>f : X₁ ⟶ X₂<VAR>g : Y₁ ⟶ Y₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f g) (CategoryTheory.ChosenFiniteProducts.fst X₂ Y₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst X₁ Y₁) f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>X₁ X₂ Y₁ Y₂ : C<VAR>f : X₁ ⟶ X₂<VAR>g : Y₁ ⟶ Y₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f g) (CategoryTheory.ChosenFiniteProducts.snd X₂ Y₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X₁ Y₁) g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>X : C<VAR>Y₁ Y₂ : C<VAR>g : Y₁ ⟶ Y₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X g) (CategoryTheory.ChosenFiniteProducts.fst X Y₂) = CategoryTheory.ChosenFiniteProducts.fst X Y₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>X : C<VAR>Y₁ Y₂ : C<VAR>g : Y₁ ⟶ Y₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X g) (CategoryTheory.ChosenFiniteProducts.snd X Y₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X Y₁) g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<VAR>Y : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f Y) (CategoryTheory.ChosenFiniteProducts.fst X₂ Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst X₁ Y) f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<VAR>Y : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f Y) (CategoryTheory.ChosenFiniteProducts.snd X₂ Y) = CategoryTheory.ChosenFiniteProducts.snd X₁ Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.ChosenFiniteProducts.fst X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (CategoryTheory.ChosenFiniteProducts.fst X Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (CategoryTheory.ChosenFiniteProducts.fst Y Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (CategoryTheory.ChosenFiniteProducts.snd X Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (CategoryTheory.ChosenFiniteProducts.snd Y Z)) = CategoryTheory.ChosenFiniteProducts.snd (CategoryTheory.MonoidalCategory.tensorObj X Y) Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (CategoryTheory.ChosenFiniteProducts.fst X Y)) = CategoryTheory.ChosenFiniteProducts.fst X (CategoryTheory.MonoidalCategory.tensorObj Y Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.fst (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (CategoryTheory.ChosenFiniteProducts.snd X Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (CategoryTheory.ChosenFiniteProducts.fst Y Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ChosenFiniteProducts C<VAR>X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.ChosenFiniteProducts.snd (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.snd X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (CategoryTheory.ChosenFiniteProducts.snd Y Z)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>j : CategoryTheory.ConnectedComponents J<GOAL>∀ {X Y : CategoryTheory.InducedCategory J CategoryTheory.FullSubcategory.obj} (f : X ⟶ Y), (CategoryTheory.Component.ι j).map f = f
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>j : CategoryTheory.ConnectedComponents J<VAR>self : CategoryTheory.FullSubcategory fun k => Quotient.mk'' k = j<GOAL>(CategoryTheory.Component.ι j).obj self = self.obj
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<GOAL>∀ {X Y : (i : CategoryTheory.ConnectedComponents J) × CategoryTheory.Component i} (g : X ⟶ Y), (CategoryTheory.decomposedTo J).map g = CategoryTheory.Sigma.descMap CategoryTheory.Component.ι X Y g
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>X : (i : CategoryTheory.ConnectedComponents J) × CategoryTheory.Component i<GOAL>(CategoryTheory.decomposedTo J).obj X = X.snd.obj
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>j : CategoryTheory.ConnectedComponents J<GOAL>(CategoryTheory.inclusion j).comp (CategoryTheory.decomposedTo J) = CategoryTheory.Component.ι j
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<GOAL>CategoryTheory.decomposedEquiv.functor = CategoryTheory.decomposedTo J
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>self : F.Full<VAR>X Y : C<GOAL>Function.Surjective F.map
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>self : F.Faithful<VAR>X Y : C<GOAL>Function.Injective F.map
<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 : CategoryTheory.Functor C D<VAR>F.Faithful<GOAL>Function.Injective F.map
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>F.Faithful<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>F.map f = F.map g ↔ 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 : CategoryTheory.Functor C D<VAR>F.Faithful<GOAL>Function.Injective F.mapIso
<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 : CategoryTheory.Functor C D<VAR>F.Full<GOAL>Function.Surjective F.map
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>F.Full<VAR>X Y : C<VAR>f : F.obj X ⟶ F.obj Y<GOAL>F.map (F.preimage f) = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<VAR>F.Full<VAR>F.Faithful<GOAL>F.preimage (CategoryTheory.CategoryStruct.id (F.obj X)) = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y Z : C<VAR>F.Full<VAR>F.Faithful<VAR>f : F.obj X ⟶ F.obj Y<VAR>g : F.obj Y ⟶ F.obj Z<GOAL>F.preimage (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.preimage f) (F.preimage g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>F.Full<VAR>F.Faithful<VAR>f : X ⟶ Y<GOAL>F.preimage (F.map f) = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>F.Full<VAR>F.Faithful<VAR>f : F.obj X ≅ F.obj Y<GOAL>(F.preimageIso f).inv = F.preimage f.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>F.Full<VAR>F.Faithful<VAR>f : F.obj X ≅ F.obj Y<GOAL>(F.preimageIso f).hom = F.preimage f.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>F.Full<VAR>F.Faithful<VAR>f : X ≅ Y<GOAL>F.preimageIso (F.mapIso f) = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>self : F.FullyFaithful<VAR>X Y : C<VAR>f : F.obj X ⟶ F.obj Y<GOAL>F.map (self.preimage f) = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>self : F.FullyFaithful<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>self.preimage (F.map f) = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : C} (f : (CategoryTheory.Functor.id C).obj X ⟶ (CategoryTheory.Functor.id C).obj Y), (CategoryTheory.Functor.FullyFaithful.id C).preimage f = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>hF : F.FullyFaithful<VAR>X Y : C<GOAL>∀ (a : X ⟶ Y), hF.homEquiv a = F.map a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>hF : F.FullyFaithful<VAR>X Y : C<VAR>f : F.obj X ⟶ F.obj Y<GOAL>hF.homEquiv.symm f = hF.preimage f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>hF : F.FullyFaithful<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>h : F.map f = F.map g<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>hF : F.FullyFaithful<VAR>X Y : C<GOAL>Function.Surjective F.map
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>hF : F.FullyFaithful<VAR>X Y : C<GOAL>Function.Bijective F.map
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>hF : F.FullyFaithful<GOAL>F.Full
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>hF : F.FullyFaithful<GOAL>F.Faithful
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>hF : F.FullyFaithful<VAR>X Y : C<VAR>e : F.obj X ≅ F.obj Y<GOAL>(hF.preimageIso e).hom = hF.preimage e.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>hF : F.FullyFaithful<VAR>X Y : C<VAR>e : F.obj X ≅ F.obj Y<GOAL>(hF.preimageIso e).inv = hF.preimage e.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>hF : F.FullyFaithful<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso (F.map f)<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>hF : F.FullyFaithful<VAR>X Y : C<VAR>e : F.obj X ≅ F.obj Y<GOAL>hF.isoEquiv.symm e = hF.preimageIso e
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>hF : F.FullyFaithful<VAR>X Y : C<VAR>i : X ≅ Y<GOAL>hF.isoEquiv i = F.mapIso i