awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : Functor.{v₂, v₁, u₂, u₁} J C
inst_5 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasEnrichedHom C F₁ F₂
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under.{v₂, u₂} j
w :
  Functor.map (ihom (F₁.obj k.right)) (f₃.app k.right) =
    CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Iso.inv (ρ_ (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
          (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₃.obj k.right)) (F₃'.obj k.right)))
        (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right) ◁
          (eHomEquiv C : (a : F₃.obj k.right ⟶ F₃'.obj k.right) → 𝟙_ C ⟶ F₃.obj k.right ⟶[C] F₃'.obj k.right)
            (f₃.app k.right))
        (eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right)))
⊢ Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃'.obj k.right))
    (F₂.map k.hom ≫ curry (f.app k.right) ≫ Functor.map (ihom (F₁.obj k.right)) (f₃.app k.right))
    (F₂.map k.hom ≫
      curry (f.app k.right) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
            (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
          (Iso.inv (ρ_ (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))))
          (CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
              (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₃.obj k.right)) (F₃'.obj k.right)))
            (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right) ◁
              (eHomEquiv C : (a : F₃.obj k.right ⟶ F₃'.obj k.right) → 𝟙_ C ⟶ F₃.obj k.right ⟶[C] F₃'.obj k.right)
                (f₃.app k.right))
            (eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right))))

Tactic:
congr 2
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : Functor.{v₂, v₁, u₂, u₁} J C
inst_5 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasEnrichedHom C F₁ F₂
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under.{v₂, u₂} j
w :
  CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Iso.inv (ρ_ (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
          (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₃.obj k.right)) (F₃'.obj k.right)))
        (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right) ◁
          (eHomEquiv C : (a : F₃.obj k.right ⟶ F₃'.obj k.right) → 𝟙_ C ⟶ F₃.obj k.right ⟶[C] F₃'.obj k.right)
            (f₃.app k.right))
        (eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right))) =
    Functor.map (ihom (F₁.obj k.right)) (f₃.app k.right)
⊢ Functor.map (ihom (F₁.obj k.right)) (f₃.app k.right) =
    CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Iso.inv (ρ_ (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
          (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₃.obj k.right)) (F₃'.obj k.right)))
        (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right) ◁
          (eHomEquiv C : (a : F₃.obj k.right ⟶ F₃'.obj k.right) → 𝟙_ C ⟶ F₃.obj k.right ⟶[C] F₃'.obj k.right)
            (f₃.app k.right))
        (eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right)))

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : Functor.{v₂, v₁, u₂, u₁} J C
inst_5 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasEnrichedHom C F₁ F₂
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under.{v₂, u₂} j
⊢ CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Iso.inv (ρ_ (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
          (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₃.obj k.right)) (F₃'.obj k.right)))
        (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right) ◁
          (eHomEquiv C : (a : F₃.obj k.right ⟶ F₃'.obj k.right) → 𝟙_ C ⟶ F₃.obj k.right ⟶[C] F₃'.obj k.right)
            (f₃.app k.right))
        (eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right))) =
    Functor.map (ihom (F₁.obj k.right)) (f₃.app k.right)

Tactic:
apply enrichedOrdinaryCategorySelf_eHomWhiskerLeft

Premises used: CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerLeft
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete
Goal:
I : Type u₂
inst : Category.{v₂, u₂} I
C : Type u₁
inst_1 : Category.{v₁, u₁} C
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalClosed.{v₁, u₁} C
inst_4 :
  ∀ (F : Functor.{u₂, v₁, u₂, u₁} (Discrete I) C),
    HasRightKanExtension.{u₂, u₂, v₁, u₁, v₂, u₂} (Discrete.functor _root_.id) F
A B : Functor.{v₂, v₁, u₂, u₁} I C
f : A ⟶ B
h :
  IsIso (X := obj (obj (whiskeringLeft (Discrete I) I C) (incl I)) A)
    (map (obj (whiskeringLeft (Discrete I) I C) (incl I)) f)
simp :
  ∀
    (h :
      ∀ (X : Discrete I),
        IsIso (X := (obj (obj (whiskeringLeft (Discrete I) I C) (incl I)) A).obj X)
          (NatTrans.app (map (obj (whiskeringLeft (Discrete I) I C) (incl I)) f) X))
    (X : I), IsIso (f.app X)
⊢ IsIso f

Tactic:
simp only [NatTrans.isIso_iff_isIso_app] at *

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete
Goal:
I : Type u₂
inst : Category.{v₂, u₂} I
C : Type u₁
inst_1 : Category.{v₁, u₁} C
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalClosed.{v₁, u₁} C
inst_4 :
  ∀ (F : Functor.{u₂, v₁, u₂, u₁} (Discrete I) C),
    HasRightKanExtension.{u₂, u₂, v₁, u₁, v₂, u₂} (Discrete.functor _root_.id) F
A B : Functor.{v₂, v₁, u₂, u₁} I C
f : A ⟶ B
h :
  ∀ (X : Discrete I),
    IsIso (X := (obj (obj (whiskeringLeft (Discrete I) I C) (incl I)) A).obj X)
      (NatTrans.app (map (obj (whiskeringLeft (Discrete I) I C) (incl I)) f) X)
X : I
⊢ IsIso (f.app X)

Tactic:
h ⟨X⟩

Premises used: CategoryTheory.Discrete.mk
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete
Goal:
I : Type u₂
inst : Category.{v₂, u₂} I
C : Type u₁
inst_1 : Category.{v₁, u₁} C
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalClosed.{v₁, u₁} C
inst_4 :
  ∀ (F : Functor.{u₂, v₁, u₂, u₁} (Discrete I) C),
    HasRightKanExtension.{u₂, u₂, v₁, u₁, v₂, u₂} (Discrete.functor _root_.id) F
A B : Functor.{v₂, v₁, u₂, u₁} I C
f : A ⟶ B
h :
  ∀ (X : Discrete I),
    IsIso (X := (obj (obj (whiskeringLeft (Discrete I) I C) (incl I)) A).obj X)
      (NatTrans.app (map (obj (whiskeringLeft (Discrete I) I C) (incl I)) f) X)
X : I
⊢ IsIso (f.app X)

Tactic:
exact h ⟨X⟩

Premises used: CategoryTheory.Discrete.mk
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete
Goal:
I : Type u₂
inst : Category.{v₂, u₂} I
C : Type u₁
inst_1 : Category.{v₁, u₁} C
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalClosed.{v₁, u₁} C
inst_4 :
  ∀ (F : Functor.{u₂, v₁, u₂, u₁} (Discrete I) C),
    HasRightKanExtension.{u₂, u₂, v₁, u₁, v₂, u₂} (Discrete.functor _root_.id) F
inst_5 : HasLimitsOfShape.{0, 0, v₁, u₁} WalkingParallelPair C
⊢ Comonad.PreservesLimitOfIsCoreflexivePair (C := Functor.{v₂, v₁, u₂, u₁} I C)
    (obj (whiskeringLeft (Discrete I) I C) (incl I))

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair.mk
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete
Goal:
I : Type u₂
inst : Category.{v₂, u₂} I
C : Type u₁
inst_1 : Category.{v₁, u₁} C
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalClosed.{v₁, u₁} C
inst_4 :
  ∀ (F : Functor.{u₂, v₁, u₂, u₁} (Discrete I) C),
    HasRightKanExtension.{u₂, u₂, v₁, u₁, v₂, u₂} (Discrete.functor _root_.id) F
inst_5 : HasLimitsOfShape.{0, 0, v₁, u₁} WalkingParallelPair C
F : Functor.{v₂, v₁, u₂, u₁} I C
⊢ IsLeftAdjoint (tensorLeft (incl I ⋙ F))

Tactic:
(ihom.adjunction (incl I ⋙ F)).isLeftAdjoint

Premises used: _private.0.CategoryTheory.Functor.incl, CategoryTheory.Functor.comp, CategoryTheory.Adjunction.isLeftAdjoint, CategoryTheory.ihom.adjunction
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G : Functor.{v, v_1, u, u_1} D C
X Y : D
f : X ⟶ Y
dsimp :
  G.map f ≫ NatTrans.app (ihom.coev (F.obj Y)) (G.obj Y) =
    NatTrans.app (ihom.coev (F.obj X)) (G.obj X) ≫ (F.closedIhom.obj (tensorObj (𝒞 := category) F G)).map f
⊢ (obj (𝟭 (Functor.{v, v_1, u, u_1} D C)) G).map f ≫ NatTrans.app (ihom.coev (F.obj Y)) (G.obj Y) =
    NatTrans.app (ihom.coev (F.obj X)) (G.obj X) ≫ ((tensorLeft F ⋙ F.closedIhom).obj G).map f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G : Functor.{v, v_1, u, u_1} D C
X Y : D
f : X ⟶ Y
simp :
  Eq (α := G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
    (NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫ map (ihom (F.obj Y)) (F.obj Y ◁ G.map f) :
      obj.{v_1, v_1, u_1, u_1} (𝟭 C) (G.obj X) ⟶
        obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
    (CategoryStruct.comp (Y :=
        obj.{v_1, v_1, u_1, u_1} (ihom (F.obj X)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (G.obj X)))
        (NatTrans.app (ihom.coev (F.obj X)) (G.obj X))
        (NatTrans.app (pre (CategoryTheory.inv (F.map f))) ((tensorObj (𝒞 := category) F G).obj X) ≫
          map (ihom (F.obj Y)) (F.map f ⊗ₘ G.map f)) :
      G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
⊢ G.map f ≫ NatTrans.app (ihom.coev (F.obj Y)) (G.obj Y) =
    NatTrans.app (ihom.coev (F.obj X)) (G.obj X) ≫ (F.closedIhom.obj (tensorObj (𝒞 := category) F G)).map f

Tactic:
simp only [ihom.coev_naturality, closedIhom_obj_map, Monoidal.tensorObj_map]

Premises used: CategoryTheory.ihom.coev_naturality, CategoryTheory.Functor.closedIhom_obj_map, CategoryTheory.Monoidal.tensorObj_map
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G : Functor.{v, v_1, u, u_1} D C
X Y : D
f : X ⟶ Y
dsimp :
  Eq (α := G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
    (NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫ map (ihom (F.obj Y)) (F.obj Y ◁ G.map f) :
      G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
    (CategoryStruct.comp (Y :=
        obj.{v_1, v_1, u_1, u_1} (ihom (F.obj X)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (G.obj X)))
        (NatTrans.app (ihom.coev (F.obj X)) (G.obj X))
        (NatTrans.app (pre (CategoryTheory.inv (F.map f))) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (G.obj X)) ≫
          map (ihom (F.obj Y)) (F.map f ⊗ₘ G.map f)) :
      G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
⊢ Eq (α := G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
    (NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫ map (ihom (F.obj Y)) (F.obj Y ◁ G.map f) :
      obj.{v_1, v_1, u_1, u_1} (𝟭 C) (G.obj X) ⟶
        obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
    (CategoryStruct.comp (Y :=
        obj.{v_1, v_1, u_1, u_1} (ihom (F.obj X)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (G.obj X)))
        (NatTrans.app (ihom.coev (F.obj X)) (G.obj X))
        (NatTrans.app (pre (CategoryTheory.inv (F.map f))) ((tensorObj (𝒞 := category) F G).obj X) ≫
          map (ihom (F.obj Y)) (F.map f ⊗ₘ G.map f)) :
      G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G : Functor.{v, v_1, u, u_1} D C
X Y : D
f : X ⟶ Y
rw :
  Eq (α := G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
    (NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫ map (ihom (F.obj Y)) (F.obj Y ◁ G.map f) :
      G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
    (NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫
        map (ihom (F.obj Y)) (CategoryTheory.inv (F.map f) ▷ G.obj X ≫ F.map f ▷ G.obj X ≫ F.obj Y ◁ G.map f) :
      G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
⊢ Eq (α := G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
    (NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫ map (ihom (F.obj Y)) (F.obj Y ◁ G.map f) :
      G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
    (CategoryStruct.comp (Y :=
        obj.{v_1, v_1, u_1, u_1} (ihom (F.obj X)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (G.obj X)))
        (NatTrans.app (ihom.coev (F.obj X)) (G.obj X))
        (NatTrans.app (pre (CategoryTheory.inv (F.map f))) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (G.obj X)) ≫
          map (ihom (F.obj Y)) (F.map f ⊗ₘ G.map f)) :
      G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))

Tactic:
rw [coev_app_comp_pre_app_assoc, ← Functor.map_comp, tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.Functor.map_comp, CategoryTheory.MonoidalClosed.coev_app_comp_pre_app_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G : Functor.{v, v_1, u, u_1} D C
X Y : D
f : X ⟶ Y
⊢ Eq (α := G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
    (NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫ map (ihom (F.obj Y)) (F.obj Y ◁ G.map f) :
      G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))
    (NatTrans.app (ihom.coev (F.obj Y)) (G.obj X) ≫
        map (ihom (F.obj Y)) (CategoryTheory.inv (F.map f) ▷ G.obj X ≫ F.map f ▷ G.obj X ≫ F.obj Y ◁ G.map f) :
      G.obj X ⟶ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (G.obj Y)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G : Functor.{v, v_1, u, u_1} D C
X Y : D
f : X ⟶ Y
dsimp :
  (F.map f ⊗ₘ (F.closedIhom.obj G).map f) ≫ NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y) =
    NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ G.map f
⊢ ((F.closedIhom ⋙ tensorLeft F).obj G).map f ≫ NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y) =
    NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ (obj (𝟭 (Functor.{v, v_1, u, u_1} D C)) G).map f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G : Functor.{v, v_1, u, u_1} D C
X Y : D
f : X ⟶ Y
simp :
  Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (obj.{v_1, v_1, u_1, u_1} (ihom (F.obj X)) (G.obj X)) ⟶ G.obj Y)
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (G.obj Y)))
      (F.map f ⊗ₘ map (ihom (F.obj X)) (G.map f) ≫ NatTrans.app (pre (CategoryTheory.inv (F.map f))) (G.obj Y))
      (NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y)))
    (NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ G.map f)
⊢ (F.map f ⊗ₘ (F.closedIhom.obj G).map f) ≫ NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y) =
    NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ G.map f

Tactic:
simp only [closedIhom_obj_map, pre_comm_ihom_map]

Premises used: CategoryTheory.Functor.closedIhom_obj_map, CategoryTheory.MonoidalClosed.pre_comm_ihom_map
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G : Functor.{v, v_1, u, u_1} D C
X Y : D
f : X ⟶ Y
rw :
  Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (obj.{v_1, v_1, u_1, u_1} (ihom (F.obj X)) (G.obj X)) ⟶ G.obj Y)
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (G.obj Y)))
      (F.map f ▷ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj X)) (G.obj X) ≫
        F.obj Y ◁ (map (ihom (F.obj X)) (G.map f) ≫ NatTrans.app (pre (CategoryTheory.inv (F.map f))) (G.obj Y)))
      (NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y)))
    (NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ G.map f)
⊢ Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (obj.{v_1, v_1, u_1, u_1} (ihom (F.obj X)) (G.obj X)) ⟶ G.obj Y)
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (G.obj Y)))
      (F.map f ⊗ₘ map (ihom (F.obj X)) (G.map f) ≫ NatTrans.app (pre (CategoryTheory.inv (F.map f))) (G.obj Y))
      (NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y)))
    (NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ G.map f)

Tactic:
rw [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G : Functor.{v, v_1, u, u_1} D C
X Y : D
f : X ⟶ Y
⊢ Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj X) (obj.{v_1, v_1, u_1, u_1} (ihom (F.obj X)) (G.obj X)) ⟶ G.obj Y)
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (F.obj Y) (obj.{v_1, v_1, u_1, u_1} (ihom (F.obj Y)) (G.obj Y)))
      (F.map f ▷ obj.{v_1, v_1, u_1, u_1} (ihom (F.obj X)) (G.obj X) ≫
        F.obj Y ◁ (map (ihom (F.obj X)) (G.map f) ≫ NatTrans.app (pre (CategoryTheory.inv (F.map f))) (G.obj Y)))
      (NatTrans.app (ihom.ev (F.obj Y)) (G.obj Y)))
    (NatTrans.app (ihom.ev (F.obj X)) (G.obj X) ≫ G.map f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G H : Functor.{v, v_1, u, u_1} D C
f : G ⟶ H
⊢ map (ihom F) f = F.closedIhom.map f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G : Functor.{v, v_1, u, u_1} D C
⊢ Eq (α := obj (ihom F ⋙ tensorLeft F) G ⟶ obj (𝟭 (Functor.{v, v_1, u, u_1} D C)) G) (NatTrans.app (ihom.ev F) G)
    (NatTrans.app F.closedCounit G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
Goal:
D : Type u
C : Type u_1
inst : Groupoid.{v, u} D
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalClosed.{v_1, u_1} C
F G : Functor.{v, v_1, u, u_1} D C
⊢ Eq (α := obj (𝟭 (Functor.{v, v_1, u, u_1} D C)) G ⟶ obj (tensorLeft F ⋙ ihom F) G) (NatTrans.app (ihom.coev F) G)
    (NatTrans.app F.closedUnit G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F X_1 Y : C ⥤ Type (max w v u)
f : X_1 ⟶ Y
X : C
a : (F.functorHom X_1).obj X
c d : C
g : c ⟶ d
h : obj (Opposite.unop (obj (Functor.rightOp coyoneda) X)) c
this :
  F.map g ≫
      a.app d
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Opposite.unop (obj (Functor.rightOp coyoneda) X)) g) :
            (a : (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj c)) →
              (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj d))
          h) =
    a.app c h ≫ X_1.map g
change : (F.map g ≫ a.app d (h ≫ g)) ≫ f.app d = (a.app c h ≫ f.app c) ≫ Y.map g
⊢ F.map g ≫
      a.app d
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (Functor.map (Opposite.unop (obj (Functor.rightOp coyoneda) X)) g) :
              (a : (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj c)) →
                (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj d))
            h) ≫
        f.app d =
    (a.app c h ≫ f.app c) ≫ Y.map g

Tactic:
change (F.map g ≫ a.app _ (h ≫ g)) ≫ _ = _

Premises used: CategoryTheory.Functor.map, CategoryTheory.Functor.HomObj.app, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F X_1 Y : C ⥤ Type (max w v u)
f : X_1 ⟶ Y
X : C
a : (F.functorHom X_1).obj X
c d : C
g : c ⟶ d
h : obj (Opposite.unop (obj (Functor.rightOp coyoneda) X)) c
this :
  F.map g ≫
      a.app d
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Opposite.unop (obj (Functor.rightOp coyoneda) X)) g) :
            (a : (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj c)) →
              (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj d))
          h) =
    a.app c h ≫ X_1.map g
⊢ (F.map g ≫ a.app d (h ≫ g)) ≫ f.app d = (a.app c h ≫ f.app c) ≫ Y.map g

Tactic:
aesop