awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
I B : C
t : IsInitial.{v, u} I
inst_2 : MonoidalClosed.{v, u} C
Z : C
g h : Z ⟶ I
h_1 : g ≫ t.to B = h ≫ t.to B
⊢ IsIso g

Tactic:
haveI := strict_initial t g
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
I B : C
t : IsInitial.{v, u} I
inst_2 : MonoidalClosed.{v, u} C
Z : C
g h : Z ⟶ I
h_1 : g ≫ t.to B = h ≫ t.to B
this : IsIso g
⊢ IsIso h

Tactic:
haveI := strict_initial t h
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
I B : C
t : IsInitial.{v, u} I
inst_2 : MonoidalClosed.{v, u} C
Z : C
g h : Z ⟶ I
h_1 : g ≫ t.to B = h ≫ t.to B
this_1 : IsIso g
this : IsIso h
⊢ g = h

Tactic:
eq_of_inv_eq_inv (t.hom_ext _ _)

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.eq_of_inv_eq_inv
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
I B : C
t : IsInitial.{v, u} I
inst_2 : MonoidalClosed.{v, u} C
Z : C
g h : Z ⟶ I
h_1 : g ≫ t.to B = h ≫ t.to B
this_1 : IsIso g
this : IsIso h
⊢ g = h

Tactic:
exact eq_of_inv_eq_inv (t.hom_ext _ _)

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.eq_of_inv_eq_inv
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X X' Y Y' Z A B_1 : C
inst_2 : Closed.{v, u} A
inst_3 : HasInitial.{v, u} C
B : C
inst_4 : MonoidalClosed.{v, u} C
⊢ Mono.{v, u} (X := initial.{v, u} C) (initial.to B)

Tactic:
initial_mono B initialIsInitial

Premises used: CategoryTheory.initial_mono, CategoryTheory.Limits.initialIsInitial, CategoryTheory.Limits.IsInitial.to, CategoryTheory.Limits.colimit.desc
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
X Y : C
⊢ @EnrichedCategory.Hom.{v, u, u} _ inst inst_1 _ _ X Y = Functor.obj.{v, v, u, u} (ihom X) Y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
X : C
⊢ Eq.{v + 1} (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v, u, u} _ inst inst_1 _ _ X X) (eId C X)
    (id X)

Tactic:
rfl

Premises used: CategoryTheory.MonoidalClosed.id, CategoryTheory.MonoidalClosed.curry, rfl, CategoryTheory.eId
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    Quiver.Hom (V := C)
      (tensorObj.{v, u} (𝒞 := inst) (@EnrichedCategory.Hom.{v, u, u} _ inst inst_1 _ _ X Y)
        (@EnrichedCategory.Hom.{v, u, u} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{v, u, u} _ inst inst_1 _ _ X Z))
    (eComp C X Y Z) (comp X Y Z)

Tactic:
rfl

Premises used: CategoryTheory.MonoidalClosed.comp, CategoryTheory.MonoidalClosed.curry, CategoryTheory.eComp, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
X Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
change :
  Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y₁)) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom X) Y₁) (Functor.obj.{v, v, u, u} (ihom Y₁) Y₂))
        (Functor.obj.{v, v, u, u} (ihom X) Y₁ ◁ curry' g) (comp X Y₁ Y₂) =
    Functor.map (ihom X) g
⊢ Eq (α :=
    Quiver.Hom (V := C) (@EnrichedCategory.Hom.{v, u, u} _ inst inst_1 _ _ X Y₁)
      (@EnrichedCategory.Hom.{v, u, u} _ inst inst_1 _ _ X Y₂))
    (eHomWhiskerLeft C X g) (Functor.map (ihom X) g)

Tactic:
change (ρ_ _).inv ≫ _ ◁ curry' g ≫ comp X Y₁ Y₂ = _

Premises used: CategoryTheory.MonoidalClosed.comp, CategoryTheory.MonoidalCategoryStruct.rightUnitor, CategoryTheory.MonoidalClosed.curry', CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
X Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
rw :
  CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom X) Y₁) (tensorUnit.{v, u} C (𝒞 := inst)))
      (Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y₁)))
      (Iso.hom (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y₁)) ≫ Functor.map (ihom X) g) =
    Functor.map (ihom X) g
rw₁ rw₂ :
  Eq (α := Functor.obj.{v, v, u, u} (ihom X) Y₁ ⟶ Functor.obj.{v, v, u, u} (ihom X) Y₂) (Functor.map (ihom X) g)
    (Functor.map (ihom X) g)
⊢ Iso.inv (ρ_ (Functor.obj.{v, v, u, u} (ihom X) Y₁)) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (ihom X) Y₁) (Functor.obj.{v, v, u, u} (ihom Y₁) Y₂))
        (Functor.obj.{v, v, u, u} (ihom X) Y₁ ◁ curry' g) (comp X Y₁ Y₂) =
    Functor.map (ihom X) g

Tactic:
rw [whiskerLeft_curry'_comp, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.MonoidalClosed.whiskerLeft_curry'_comp, CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
X₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
change :
  Eq (α := Functor.obj.{v, v, u, u} (ihom X₂) Y ⟶ Functor.obj.{v, v, u, u} (ihom X₁) Y)
    (Iso.inv (λ_ (Functor.obj.{v, v, u, u} (ihom X₂) Y)) ≫
      curry' f ▷ Functor.obj.{v, v, u, u} (ihom X₂) Y ≫ comp X₁ X₂ Y)
    (NatTrans.app (pre f) Y)
⊢ Eq (α :=
    Quiver.Hom (V := C) (@EnrichedCategory.Hom.{v, u, u} _ inst inst_1 _ _ X₂ Y)
      (@EnrichedCategory.Hom.{v, u, u} _ inst inst_1 _ _ X₁ Y))
    (eHomWhiskerRight C f Y) (NatTrans.app (pre f) Y)

Tactic:
change (λ_ _).inv ≫ curry' f ▷ _ ≫ comp X₁ X₂ Y = _

Premises used: CategoryTheory.MonoidalClosed.comp, CategoryTheory.MonoidalCategoryStruct.leftUnitor, CategoryTheory.MonoidalClosed.curry', CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
X₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
rw :
  Eq (α := Functor.obj.{v, v, u, u} (ihom X₂) Y ⟶ Functor.obj.{v, v, u, u} (ihom X₁) Y)
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) (Functor.obj.{v, v, u, u} (ihom X₂) Y))
      (Iso.inv (λ_ (Functor.obj.{v, v, u, u} (ihom X₂) Y)))
      (Iso.hom (λ_ (Functor.obj.{v, v, u, u} (ihom X₂) Y)) ≫ NatTrans.app (pre f) Y))
    (NatTrans.app (pre f) Y)
rw₁ rw₂ :
  Eq (α := Functor.obj.{v, v, u, u} (ihom X₂) Y ⟶ Functor.obj.{v, v, u, u} (ihom X₁) Y) (NatTrans.app (pre f) Y)
    (NatTrans.app (pre f) Y)
⊢ Eq (α := Functor.obj.{v, v, u, u} (ihom X₂) Y ⟶ Functor.obj.{v, v, u, u} (ihom X₁) Y)
    (Iso.inv (λ_ (Functor.obj.{v, v, u, u} (ihom X₂) Y)) ≫
      curry' f ▷ Functor.obj.{v, v, u, u} (ihom X₂) Y ≫ comp X₁ X₂ Y)
    (NatTrans.app (pre f) Y)

Tactic:
rw [curry'_whiskerRight_comp, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.MonoidalClosed.curry'_whiskerRight_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Eq (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v, u, u} _ inst inst_1 _ _ X Y)
    ((eHomEquiv C : (a : X ⟶ Y) → 𝟙_ C ⟶ X ⟶[C] Y) f :
      tensorUnit.{v, u} C (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v, u, u} _ inst inst_1 _ _ X Y)
    (curry' f : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom X) Y)

Tactic:
rfl

Premises used: CategoryTheory.MonoidalClosed.curry', CategoryTheory.MonoidalClosed.curry, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : MonoidalClosed.{v, u} C
X Y : C
g : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Functor.obj.{v, v, u, u} (ihom X) Y
⊢ (Equiv.symm (eHomEquiv C) : (a : 𝟙_ C ⟶ X ⟶[C] Y) → X ⟶ Y) g = uncurry' g

Tactic:
rfl

Premises used: CategoryTheory.MonoidalClosed.uncurry', rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
h : L ⊣ F
A : C
inst_4 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) L
inst_5 : F.Full
inst_6 : F.Faithful
B : D
dsimp :
  IsIso (X := L.obj (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) B)) (Y := tensorObj.{v, u} (𝒞 := inst) A (L.obj B))
    (prodComparison L (F.obj A) B ≫ h.counit.app A ▷ L.obj B)
⊢ IsIso (X := (tensorLeft (F.obj A) ⋙ L).obj B) (Y := (L ⋙ tensorLeft A).obj B)
    (NatTrans.app (natTrans (frobeniusMorphism F h A)) B)

Tactic:
dsimp [frobeniusMorphism]

Premises used: CategoryTheory.frobeniusMorphism
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
h : L ⊣ F
A : C
inst_4 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) L
inst_5 : F.Full
inst_6 : F.Faithful
B : D
⊢ IsIso (X := L.obj (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) B)) (Y := tensorObj.{v, u} (𝒞 := inst) A (L.obj B))
    (prodComparison L (F.obj A) B ≫ h.counit.app A ▷ L.obj B)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u', u'} (Functor.obj (curriedTensor D) (F.obj A)) ((ihom A ⋙ F).obj B) ⟶
      Functor.obj.{v, v, u', u'} (𝟭 D) (F.obj B))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v, v, u', u'} (Functor.obj (curriedTensor D) (F.obj A)) ((F ⋙ ihom (F.obj A)).obj B))
        (Functor.map (Functor.obj (curriedTensor D) (F.obj A))
          (NatTrans.app
            ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)) :
                (a : TwoSquare F ((curriedTensor C).obj A) ((curriedTensor D).obj (F.obj A)) F) →
                  TwoSquare (ihom A) F F (ihom (F.obj A)))
              (Iso.inv (prodComparisonNatIso F A)))
            B))
        (NatTrans.app (Adjunction.counit (ihom.adjunction (F.obj A))) (F.obj B)) :
      Functor.obj.{v, v, u', u'} (Functor.obj (curriedTensor D) (F.obj A)) ((ihom A ⋙ F).obj B) ⟶
        Functor.obj.{v, v, u', u'} (𝟭 D) (F.obj B))
    (NatTrans.app (Iso.inv (prodComparisonNatIso F A)) (Functor.obj.{v, v, u, u} (ihom A) B) ≫
        F.map (NatTrans.app (Adjunction.counit (ihom.adjunction A)) B) :
      (F ⋙ Functor.obj (curriedTensor D) (F.obj A)).obj (Functor.obj.{v, v, u, u} (ihom A) B) ⟶
        F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B))

Tactic:
mateEquiv_counit _ _ (prodComparisonNatIso F A).inv B

Premises used: CategoryTheory.mateEquiv_counit, CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
h :
  (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) ((ihom A ⋙ F).obj B) ⟶ Functor.obj.{v, v, u', u'} (𝟭 D) (F.obj B)) =
      (Functor.obj.{v, v, u', u'} (Functor.obj (curriedTensor D) (F.obj A)) ((ihom A ⋙ F).obj B) ⟶
        Functor.obj.{v, v, u', u'} (𝟭 D) (F.obj B)) →
    tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj (Functor.obj.{v, v, u, u} (ihom A) B)) =
        (F ⋙ Functor.obj (curriedTensor D) (F.obj A)).obj (Functor.obj.{v, v, u, u} (ihom A) B) →
      F.obj (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (ihom A) B)) =
          (Functor.obj (curriedTensor C) A ⋙ F).obj (Functor.obj.{v, v, u, u} (ihom A) B) →
        Eq (α :=
          tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj (Functor.obj.{v, v, u, u} (ihom A) B)) ⟶
            F.obj (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (ihom A) B)))
          (inv (prodComparison F A (Functor.obj.{v, v, u, u} (ihom A) B)))
          (NatTrans.app (Iso.inv (prodComparisonNatIso F A)) (Functor.obj.{v, v, u, u} (ihom A) B))
⊢ Eq (α := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) ((ihom A ⋙ F).obj B) ⟶ Functor.obj.{v, v, u', u'} (𝟭 D) (F.obj B))
    (CategoryStruct.comp (Y := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) ((F ⋙ ihom (F.obj A)).obj B))
      (F.obj A ◁ NatTrans.app (natTrans (expComparison F A)) B) (NatTrans.app (ihom.ev (F.obj A)) (F.obj B)))
    (inv (prodComparison F A (Functor.obj.{v, v, u, u} (ihom A) B)) ≫ F.map (NatTrans.app (ihom.ev A) B))

Tactic:
convert! mateEquiv_counit _ _ (prodComparisonNatIso F A).inv B using 2

Premises used: CategoryTheory.mateEquiv_counit, CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
e_1 :
  (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) ((ihom A ⋙ F).obj B) ⟶ Functor.obj.{v, v, u', u'} (𝟭 D) (F.obj B)) =
    (Functor.obj.{v, v, u', u'} (Functor.obj (curriedTensor D) (F.obj A)) ((ihom A ⋙ F).obj B) ⟶
      Functor.obj.{v, v, u', u'} (𝟭 D) (F.obj B))
e_3 :
  tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj (Functor.obj.{v, v, u, u} (ihom A) B)) =
    (F ⋙ Functor.obj (curriedTensor D) (F.obj A)).obj (Functor.obj.{v, v, u, u} (ihom A) B)
e_4 :
  F.obj (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (ihom A) B)) =
    (Functor.obj (curriedTensor C) A ⋙ F).obj (Functor.obj.{v, v, u, u} (ihom A) B)
h :
  CategoryStruct.comp (Y := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj (Functor.obj.{v, v, u, u} (ihom A) B)))
      (prodComparison F A (Functor.obj.{v, v, u, u} (ihom A) B))
      (NatTrans.app (Iso.inv (prodComparisonNatIso F A)) (Functor.obj.{v, v, u, u} (ihom A) B)) =
    𝟙 (F.obj (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (ihom A) B)))
⊢ Eq (α :=
    tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj (Functor.obj.{v, v, u, u} (ihom A) B)) ⟶
      F.obj (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (ihom A) B)))
    (inv (prodComparison F A (Functor.obj.{v, v, u, u} (ihom A) B)))
    (NatTrans.app (Iso.inv (prodComparisonNatIso F A)) (Functor.obj.{v, v, u, u} (ihom A) B))

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Premises used: CategoryTheory.IsIso.inv_eq_of_hom_inv_id
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
e_1 :
  (tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) ((ihom A ⋙ F).obj B) ⟶ Functor.obj.{v, v, u', u'} (𝟭 D) (F.obj B)) =
    (Functor.obj.{v, v, u', u'} (Functor.obj (curriedTensor D) (F.obj A)) ((ihom A ⋙ F).obj B) ⟶
      Functor.obj.{v, v, u', u'} (𝟭 D) (F.obj B))
e_3 :
  tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj (Functor.obj.{v, v, u, u} (ihom A) B)) =
    (F ⋙ Functor.obj (curriedTensor D) (F.obj A)).obj (Functor.obj.{v, v, u, u} (ihom A) B)
e_4 :
  F.obj (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (ihom A) B)) =
    (Functor.obj (curriedTensor C) A ⋙ F).obj (Functor.obj.{v, v, u, u} (ihom A) B)
⊢ CategoryStruct.comp (Y := tensorObj.{v, u'} (𝒞 := inst_1) (F.obj A) (F.obj (Functor.obj.{v, v, u, u} (ihom A) B)))
      (prodComparison F A (Functor.obj.{v, v, u, u} (ihom A) B))
      (NatTrans.app (Iso.inv (prodComparisonNatIso F A)) (Functor.obj.{v, v, u, u} (ihom A) B)) =
    𝟙 (F.obj (tensorObj.{v, u} (𝒞 := inst) A (Functor.obj.{v, v, u, u} (ihom A) B)))

Tactic:
simp only [prodComparisonNatTrans_app, prodComparisonNatIso_inv, NatIso.isIso_inv_app,
    IsIso.hom_inv_id]

Premises used: CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso_inv, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.NatIso.isIso_inv_app, CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans_app
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
⊢ Eq (α :=
    F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B) ⟶
      (F ⋙ ihom (F.obj A)).obj (Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) A) B))
    (CategoryStruct.comp (Y := F.obj (Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) A ⋙ ihom A) B))
      (F.map (NatTrans.app (Adjunction.unit (ihom.adjunction A)) B))
      (NatTrans.app
        ((mateEquiv (ihom.adjunction A) (ihom.adjunction (F.obj A)) :
            (a : TwoSquare F ((curriedTensor C).obj A) ((curriedTensor D).obj (F.obj A)) F) →
              TwoSquare (ihom A) F F (ihom (F.obj A)))
          (Iso.inv (prodComparisonNatIso F A)))
        (Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) A) B)))
    (NatTrans.app (Adjunction.unit (ihom.adjunction (F.obj A))) (F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B)) ≫
      Functor.map (ihom (F.obj A))
        (NatTrans.app (Iso.inv (prodComparisonNatIso F A)) (Functor.obj.{v, v, u, u} (𝟭 C) B)))

Tactic:
unit_mateEquiv _ _ (prodComparisonNatIso F A).inv B

Premises used: CategoryTheory.unit_mateEquiv, CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
h :
  (F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B) ⟶ (F ⋙ ihom (F.obj A)).obj (tensorObj.{v, u} (𝒞 := inst) A B)) =
      (F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B) ⟶
        (F ⋙ ihom (F.obj A)).obj (Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) A) B)) →
    Functor.obj.{v, v, u', u'} (tensorLeft (F.obj A) ⋙ ihom (F.obj A)) (F.obj B) =
        Functor.obj.{v, v, u', u'} (Functor.obj (curriedTensor D) (F.obj A) ⋙ ihom (F.obj A))
          (F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B)) →
      Functor.obj.{v, v, u', u'} (ihom (F.obj A)) (F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) =
          Functor.obj.{v, v, u', u'} (ihom (F.obj A))
            ((Functor.obj (curriedTensor C) A ⋙ F).obj (Functor.obj.{v, v, u, u} (𝟭 C) B)) →
        Functor.obj.{v, v, u', u'} (tensorLeft (F.obj A)) (F.obj B) =
            Functor.obj.{v, v, u', u'} (Functor.obj (curriedTensor D) (F.obj A))
              (F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B)) →
          F.obj (tensorObj.{v, u} (𝒞 := inst) A B) =
              (Functor.obj (curriedTensor C) A ⋙ F).obj (Functor.obj.{v, v, u, u} (𝟭 C) B) →
            Eq (α :=
              Functor.obj.{v, v, u', u'} (tensorLeft (F.obj A)) (F.obj B) ⟶ F.obj (tensorObj.{v, u} (𝒞 := inst) A B))
              (inv (prodComparison F A B))
              (NatTrans.app (Iso.inv (prodComparisonNatIso F A)) (Functor.obj.{v, v, u, u} (𝟭 C) B))
⊢ Eq (α := F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B) ⟶ (F ⋙ ihom (F.obj A)).obj (tensorObj.{v, u} (𝒞 := inst) A B))
    (CategoryStruct.comp (Y := F.obj (Functor.obj.{v, v, u, u} (tensorLeft A ⋙ ihom A) B))
      (F.map (NatTrans.app (ihom.coev A) B))
      (NatTrans.app (natTrans (expComparison F A)) (tensorObj.{v, u} (𝒞 := inst) A B)))
    (NatTrans.app (ihom.coev (F.obj A)) (F.obj B) ≫ Functor.map (ihom (F.obj A)) (inv (prodComparison F A B)))

Tactic:
convert! unit_mateEquiv _ _ (prodComparisonNatIso F A).inv B using 3

Premises used: CategoryTheory.unit_mateEquiv, CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
e_1 :
  (F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B) ⟶ (F ⋙ ihom (F.obj A)).obj (tensorObj.{v, u} (𝒞 := inst) A B)) =
    (F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B) ⟶
      (F ⋙ ihom (F.obj A)).obj (Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) A) B))
e_4 :
  Functor.obj.{v, v, u', u'} (tensorLeft (F.obj A) ⋙ ihom (F.obj A)) (F.obj B) =
    Functor.obj.{v, v, u', u'} (Functor.obj (curriedTensor D) (F.obj A) ⋙ ihom (F.obj A))
      (F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B))
e_5 :
  Functor.obj.{v, v, u', u'} (ihom (F.obj A)) (F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) =
    Functor.obj.{v, v, u', u'} (ihom (F.obj A))
      ((Functor.obj (curriedTensor C) A ⋙ F).obj (Functor.obj.{v, v, u, u} (𝟭 C) B))
e_6 :
  Functor.obj.{v, v, u', u'} (tensorLeft (F.obj A)) (F.obj B) =
    Functor.obj.{v, v, u', u'} (Functor.obj (curriedTensor D) (F.obj A)) (F.obj (Functor.obj.{v, v, u, u} (𝟭 C) B))
e_7 :
  F.obj (tensorObj.{v, u} (𝒞 := inst) A B) =
    (Functor.obj (curriedTensor C) A ⋙ F).obj (Functor.obj.{v, v, u, u} (𝟭 C) B)
h :
  CategoryStruct.comp (Y := Functor.obj.{v, v, u', u'} (tensorLeft (F.obj A)) (F.obj B)) (prodComparison F A B)
      (NatTrans.app (Iso.inv (prodComparisonNatIso F A)) (Functor.obj.{v, v, u, u} (𝟭 C) B)) =
    𝟙 (F.obj (tensorObj.{v, u} (𝒞 := inst) A B))
⊢ Eq (α := Functor.obj.{v, v, u', u'} (tensorLeft (F.obj A)) (F.obj B) ⟶ F.obj (tensorObj.{v, u} (𝒞 := inst) A B))
    (inv (prodComparison F A B)) (NatTrans.app (Iso.inv (prodComparisonNatIso F A)) (Functor.obj.{v, v, u, u} (𝟭 C) B))

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Premises used: CategoryTheory.IsIso.inv_eq_of_hom_inv_id