awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
X Y : D
mk :
  ∀
    (μIso :
      (X Y : D) → tensorObj.{v₁, u₁} (𝒞 := inst) (F.obj X) (F.obj Y) ≅ F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)),
    (∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂), F.map (X ◁ f) = (μIso X Y₁).inv ≫ F.obj X ◁ F.map f ≫ (μIso X Y₂).hom) →
      (∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D), F.map (f ▷ Y) = (μIso X₁ Y).inv ≫ F.map f ▷ F.obj Y ≫ (μIso X₂ Y).hom) →
        (∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
            F.map (f ⊗ₘ g) = (μIso X₁ X₂).inv ≫ (F.map f ⊗ₘ F.map g) ≫ (μIso Y₁ Y₂).hom) →
          ∀ (εIso : tensorUnit.{v₁, u₁} C (𝒞 := inst) ≅ F.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))),
            (∀ (X Y Z : D),
                F.map (Iso.hom (α_ X Y Z)) =
                  ((Iso.symm (μIso (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) Z) ≪≫
                        ((μIso X Y).symm ⊗ᵢ Iso.refl (F.obj Z))) ≪≫
                      α_ (F.obj X) (F.obj Y) (F.obj Z) ≪≫
                        (Iso.refl (F.obj X) ⊗ᵢ μIso Y Z) ≪≫ μIso X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)).hom) →
              (∀ (X : D),
                  F.map (Iso.hom (λ_ X)) =
                    ((Iso.symm (μIso (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) X) ≪≫ (εIso.symm ⊗ᵢ Iso.refl (F.obj X))) ≪≫
                        λ_ (F.obj X)).hom) →
                (∀ (X : D),
                    F.map (Iso.hom (ρ_ X)) =
                      ((Iso.symm (μIso X (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) ≪≫ (Iso.refl (F.obj X) ⊗ᵢ εIso.symm)) ≪≫
                          ρ_ (F.obj X)).hom) →
                  Eq (α :=
                    F.obj
                        (tensorObj.{v₂, u₂} (𝒞 := inst_2)
                          (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) Y) ⟶
                      F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
                    (F.map (Iso.hom (α_ X (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) Y) ≫ X ◁ Iso.hom (λ_ Y)))
                    (F.map (Iso.hom (ρ_ X) ▷ Y))
⊢ Eq (α :=
    F.obj
        (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
          Y) ⟶
      F.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
    (F.map (Iso.hom (α_ X (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) Y) ≫ X ◁ Iso.hom (λ_ Y))) (F.map (Iso.hom (ρ_ X) ▷ Y))

Tactic:
cases fData
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
this : MonoidalCategory.{v₂, u₂} D := induced F fData
X Y : D
x : X ⟶ Y
⊢ ∀ (X' : D), F.map x ▷ F.obj X' ≫ (fData.μIso Y X').hom = (fData.μIso X X').hom ≫ F.map (x ▷ X')

Tactic:
simp [fData.whiskerRight_eq]

Premises used: CategoryTheory.Monoidal.InducingFunctorData.whiskerRight_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
this : MonoidalCategory.{v₂, u₂} D := induced F fData
X Y x : D
⊢ ∀ (f : X ⟶ Y), F.obj x ◁ F.map f ≫ (fData.μIso x Y).hom = (fData.μIso x X).hom ≫ F.map (x ◁ f)

Tactic:
simp [fData.whiskerLeft_eq]

Premises used: CategoryTheory.Monoidal.InducingFunctorData.whiskerLeft_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
this : MonoidalCategory.{v₂, u₂} D := induced F fData
x x_1 x_2 : D
⊢ (fData.μIso x x_1).hom ▷ F.obj x_2 ≫
      Iso.hom (fData.μIso (tensorObj.{v₂, u₂} (𝒞 := inst_2) x x_1) x_2) ≫ F.map (Iso.hom (α_ x x_1 x_2)) =
    Iso.hom (α_ (F.obj x) (F.obj x_1) (F.obj x_2)) ≫
      F.obj x ◁ (fData.μIso x_1 x_2).hom ≫ Iso.hom (fData.μIso x (tensorObj.{v₂, u₂} (𝒞 := inst_2) x_1 x_2))

Tactic:
simp [fData.associator_eq]

Premises used: CategoryTheory.Monoidal.InducingFunctorData.associator_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
this : MonoidalCategory.{v₂, u₂} D := induced F fData
x : D
⊢ Iso.hom (λ_ (F.obj x)) =
    fData.εIso.hom ▷ F.obj x ≫ Iso.hom (fData.μIso (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) x) ≫ F.map (Iso.hom (λ_ x))

Tactic:
simp [fData.leftUnitor_eq]

Premises used: CategoryTheory.Monoidal.InducingFunctorData.leftUnitor_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
this : MonoidalCategory.{v₂, u₂} D := induced F fData
x : D
⊢ Iso.hom (ρ_ (F.obj x)) =
    F.obj x ◁ fData.εIso.hom ≫ Iso.hom (fData.μIso x (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) ≫ F.map (Iso.hom (ρ_ x))

Tactic:
simp [fData.rightUnitor_eq]

Premises used: CategoryTheory.Monoidal.InducingFunctorData.rightUnitor_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategoryStruct.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : F.Faithful
fData : InducingFunctorData F
this : MonoidalCategory.{v₂, u₂} D := induced F fData
⊢ F.CoreMonoidal

Tactic:
exact
    { εIso := fData.εIso
      μIso := fData.μIso
      μIso_hom_natural_left := fun _ ↦ by simp [fData.whiskerRight_eq]
      μIso_hom_natural_right := fun _ ↦ by simp [fData.whiskerLeft_eq]
      associativity := fun _ _ _ ↦ by simp [fData.associator_eq]
      left_unitality := fun _ ↦ by simp [fData.leftUnitor_eq]
      right_unitality := fun _ ↦ by simp [fData.rightUnitor_eq] }
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
this : MonoidalCategoryStruct.{v₂, u₂} D := transportStruct e
⊢ ∀ (X : D) {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂),
    Eq (α :=
      e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y₁) ⟶ e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y₂))
      (e.inverse.map (X ◁ f))
      (Iso.inv (e.unitIso.app (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj X) (e.inverse.obj Y₁))) ≫
        e.inverse.obj X ◁ e.inverse.map f ≫
          Iso.hom (e.unitIso.app (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj X) (e.inverse.obj Y₂))))

Tactic:
simp +zetaDelta +instances
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
this : MonoidalCategoryStruct.{v₂, u₂} D := transportStruct e
⊢ ∀ {X₁ X₂ : D} (f : X₁ ⟶ X₂) (Y : D),
    Eq (α :=
      e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X₁ Y) ⟶ e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X₂ Y))
      (e.inverse.map (f ▷ Y))
      (Iso.inv (e.unitIso.app (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj X₁) (e.inverse.obj Y))) ≫
        e.inverse.map f ▷ e.inverse.obj Y ≫
          Iso.hom (e.unitIso.app (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj X₂) (e.inverse.obj Y))))

Tactic:
simp +zetaDelta +instances
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
this : MonoidalCategoryStruct.{v₂, u₂} D := transportStruct e
⊢ ∀ {X₁ Y₁ X₂ Y₂ : D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    Eq (α :=
      e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X₁ X₂) ⟶ e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y₁ Y₂))
      (e.inverse.map (f ⊗ₘ g))
      (Iso.inv (e.unitIso.app (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj X₁) (e.inverse.obj X₂))) ≫
        (e.inverse.map f ⊗ₘ e.inverse.map g) ≫
          Iso.hom (e.unitIso.app (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj Y₁) (e.inverse.obj Y₂))))

Tactic:
simp +zetaDelta +instances
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
this : MonoidalCategoryStruct.{v₂, u₂} D := transportStruct e
⊢ ∀ (X Y Z : D),
    Eq (α :=
      e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) Z) ⟶
        e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
      (e.inverse.map (Iso.hom (α_ X Y Z)))
      (Iso.hom
        ((Iso.symm
              (e.unitIso.app
                (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
                  (e.inverse.obj Z))) ≪≫
            (Iso.symm (e.unitIso.app (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj X) (e.inverse.obj Y))) ⊗ᵢ
              Iso.refl (e.inverse.obj Z))) ≪≫
          α_ (e.inverse.obj X) (e.inverse.obj Y) (e.inverse.obj Z) ≪≫
            (Iso.refl (e.inverse.obj X) ⊗ᵢ
                e.unitIso.app (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj Y) (e.inverse.obj Z))) ≪≫
              e.unitIso.app
                (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj X)
                  (e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))))

Tactic:
simp +zetaDelta +instances
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
this : MonoidalCategoryStruct.{v₂, u₂} D := transportStruct e
⊢ ∀ (X : D),
    Eq (α := e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) X) ⟶ e.inverse.obj X)
      (e.inverse.map (Iso.hom (λ_ X)))
      (Iso.hom
        ((Iso.symm
              (e.unitIso.app
                (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
                  (e.inverse.obj X))) ≪≫
            (Iso.symm (e.unitIso.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⊗ᵢ Iso.refl (e.inverse.obj X))) ≪≫
          λ_ (e.inverse.obj X)))

Tactic:
simp +zetaDelta +instances
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
this : MonoidalCategoryStruct.{v₂, u₂} D := transportStruct e
⊢ ∀ (X : D),
    Eq (α := e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) ⟶ e.inverse.obj X)
      (e.inverse.map (Iso.hom (ρ_ X)))
      (Iso.hom
        ((Iso.symm
              (e.unitIso.app
                (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj X)
                  (e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))) ≪≫
            (Iso.refl (e.inverse.obj X) ⊗ᵢ Iso.symm (e.unitIso.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≪≫
          ρ_ (e.inverse.obj X)))

Tactic:
simp +zetaDelta +instances
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ (equivalenceTransported e).inverse.Monoidal

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ (equivalenceTransported e).symm.IsMonoidal

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ NatTrans.IsMonoidal (equivalenceTransported e).unit

Tactic:
inferInstanceAs (NatTrans.IsMonoidal (equivalenceTransported e).symm.counitIso.inv)

Premises used: _private.0.CategoryTheory.Monoidal.instIsMonoidalUnitTransportedEquivalenceTransported._proof_1
-- Module: Mathlib.CategoryTheory.Monoidal.Transport
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ NatTrans.IsMonoidal (equivalenceTransported e).counit

Tactic:
inferInstanceAs (NatTrans.IsMonoidal (equivalenceTransported e).symm.unitIso.inv)

Premises used: _private.0.CategoryTheory.Monoidal.instIsMonoidalTransportedCounitEquivalenceTransported._proof_1
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
X Y : Type u
⊢ tensorObj (𝒞 := types) X Y = (X × Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
⊢ (𝟙_ (Type u)) (𝒞 := types) = PUnit.{u + 1}

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
W X Y Z : Type u
f : W ⟶ X
g : Y ⟶ Z
p : tensorObj (𝒞 := types) W Y
⊢ Eq (α := X × Z) ((ConcreteCategory.hom (FC := TypeCat.Fun) (f ⊗ₘ g) : (a : W × Y) → X × Z) p : X × Z)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : W) → X) p.1,
        (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : Y) → Z) p.2) :
      X × Z)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
X Y Z : Type u
f : Y ⟶ Z
p : tensorObj (𝒞 := types) X Y
⊢ Eq (α := X × Z) ((ConcreteCategory.hom (FC := TypeCat.Fun) (X ◁ f) : (a : X × Y) → X × Z) p : X × Z)
    ((p.1, (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : Y) → Z) p.2) : X × Z)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
Y Z : Type u
f : Y ⟶ Z
X : Type u
p : tensorObj (𝒞 := types) Y X
⊢ Eq (α := Z × X) ((ConcreteCategory.hom (FC := TypeCat.Fun) (f ▷ X) : (a : Y × X) → Z × X) p : Z × X)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : Y) → Z) p.1, p.2) : Z × X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
X : Type u
x : X
p : PUnit.{u + 1}
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (λ_ X)) : (a : PUnit.{u + 1} × X) → X) (p, x) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
X : Type u
x : X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (λ_ X)) : (a : X) → PUnit.{u + 1} × X) x = (PUnit.unit, x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
X : Type u
x : X
p : PUnit.{u + 1}
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (ρ_ X)) : (a : X × PUnit.{u + 1}) → X) (x, p) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
X : Type u
x : X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (ρ_ X)) : (a : X) → X × PUnit.{u + 1}) x = (x, PUnit.unit)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
X Y Z : Type u
x : X
y : Y
z : Z
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (α_ X Y Z)) : (a : (X × Y) × Z) → X × Y × Z) ((x, y), z) =
    (x, y, z)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
X Y Z : Type u
x : X
y : Y
z : Z
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (α_ X Y Z)) : (a : X × Y × Z) → (X × Y) × Z) (x, y, z) =
    ((x, y), z)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
X Y Z : Type u
x : (fun (X : Type u) ↦ X) (tensorObj (𝒞 := types) (tensorObj (𝒞 := types) X Y) Z)
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (α_ X Y Z)) : (a : (X × Y) × Z) → X × Y × Z) x).1 = x.1.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
X Y Z : Type u
x : (fun (X : Type u) ↦ X) (tensorObj (𝒞 := types) (tensorObj (𝒞 := types) X Y) Z)
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (α_ X Y Z)) : (a : (X × Y) × Z) → X × Y × Z) x).2.1 = x.1.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
X Y Z : Type u
x : (fun (X : Type u) ↦ X) (tensorObj (𝒞 := types) (tensorObj (𝒞 := types) X Y) Z)
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (α_ X Y Z)) : (a : (X × Y) × Z) → X × Y × Z) x).2.2 = x.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
X Y Z : Type u
x : (fun (X : Type u) ↦ X) (tensorObj (𝒞 := types) X (tensorObj (𝒞 := types) Y Z))
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (α_ X Y Z)) : (a : X × Y × Z) → (X × Y) × Z) x).1.1 = x.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
X Y Z : Type u
x : (fun (X : Type u) ↦ X) (tensorObj (𝒞 := types) X (tensorObj (𝒞 := types) Y Z))
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (α_ X Y Z)) : (a : X × Y × Z) → (X × Y) × Z) x).1.2 = x.2.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
X Y Z : Type u
x : (fun (X : Type u) ↦ X) (tensorObj (𝒞 := types) X (tensorObj (𝒞 := types) Y Z))
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (α_ X Y Z)) : (a : X × Y × Z) → (X × Y) × Z) x).2 = x.2.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
X Y : Type u
x : X
y : Y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (β_ X Y)) : (a : X × Y) → Y × X) (x, y) = (y, x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
X Y : Type u
x : X
y : Y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (β_ X Y)) : (a : Y × X) → X × Y) (y, x) = (x, y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Basic
Goal:
X Y Z : Type u
f : X ⟶ Y
g : X ⟶ Z
x : X
⊢ Eq (α := Y × Z) ((ConcreteCategory.hom (FC := TypeCat.Fun) (lift f g) : (a : X) → Y × Z) x : Y × Z)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : X) → Y) x,
        (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : X) → Z) x) :
      Y × Z)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
h : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Z
f : tensorUnit.{v, u} C (𝒞 := inst) ⟶ X
g : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Y
h₁ :
  (Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (f ⊗ₘ g) ⊗ₘ h) ≫ Iso.hom (α_ X Y Z) =
    f ⊗ₘ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (g ⊗ₘ h)
⊢ (Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (f ⊗ₘ g) ⊗ₘ h)) ≫
      Iso.hom (α_ X Y Z) =
    Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (f ⊗ₘ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (g ⊗ₘ h))

Tactic:
simp only [Category.assoc, Iso.cancel_iso_inv_left]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.cancel_iso_inv_left
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
h : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Z
f : tensorUnit.{v, u} C (𝒞 := inst) ⟶ X
g : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Y
rw : tensorUnit.{v, u} C (𝒞 := inst) ◁ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (f ⊗ₘ g ⊗ₘ h)
| (Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (f ⊗ₘ g) ⊗ₘ h) ≫ Iso.hom (α_ X Y Z)

Tactic:
rw [← Category.id_comp h, ← tensorHom_comp_tensorHom, Category.assoc, associator_naturality,
          ← Category.assoc, unitors_inv_equal, tensorHom_id, triangle_assoc_comp_right_inv]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_inv, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.MonoidalCategory.associator_naturality, CategoryTheory.MonoidalCategory.unitors_inv_equal, CategoryTheory.MonoidalCategory.tensorHom_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
h : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Z
f : tensorUnit.{v, u} C (𝒞 := inst) ⟶ X
g : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Y
h₁ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)) ⟶
      tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z))
    (tensorUnit.{v, u} C (𝒞 := inst) ◁ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (f ⊗ₘ g ⊗ₘ h))
    (f ⊗ₘ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (g ⊗ₘ h))
⊢ (Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (f ⊗ₘ g) ⊗ₘ h) ≫ Iso.hom (α_ X Y Z) =
    f ⊗ₘ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (g ⊗ₘ h)

Tactic:
conv_lhs =>
        rw [← Category.id_comp h, ← tensorHom_comp_tensorHom, Category.assoc, associator_naturality,
          ← Category.assoc, unitors_inv_equal, tensorHom_id, triangle_assoc_comp_right_inv]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_inv, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.MonoidalCategory.associator_naturality, CategoryTheory.MonoidalCategory.unitors_inv_equal, CategoryTheory.MonoidalCategory.tensorHom_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
h : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Z
f : tensorUnit.{v, u} C (𝒞 := inst) ⟶ X
g : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Y
rw : (𝟙 (tensorUnit.{v, u} C (𝒞 := inst)) ⊗ₘ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst)))) ≫ (f ⊗ₘ g ⊗ₘ h)
| f ⊗ₘ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (g ⊗ₘ h)

Tactic:
rw [← Category.id_comp f, ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
h : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Z
f : tensorUnit.{v, u} C (𝒞 := inst) ⟶ X
g : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Y
h₁ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)) ⟶
      tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z))
    (tensorUnit.{v, u} C (𝒞 := inst) ◁ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (f ⊗ₘ g ⊗ₘ h))
    ((𝟙 (tensorUnit.{v, u} C (𝒞 := inst)) ⊗ₘ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst)))) ≫ (f ⊗ₘ g ⊗ₘ h))
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (tensorUnit.{v, u} C (𝒞 := inst)) ⟶
      tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z))
    (tensorUnit.{v, u} C (𝒞 := inst) ◁ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (f ⊗ₘ g ⊗ₘ h))
    (f ⊗ₘ Iso.inv (λ_ (tensorUnit.{v, u} C (𝒞 := inst))) ≫ (g ⊗ₘ h))

Tactic:
conv_rhs => rw [← Category.id_comp f, ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Category.id_comp