-- Mathlib/CategoryTheory/Closed/Functor.lean
theorem coev_expComparison (A B : C) :
    F.map ((exp.coev A).app B) ≫ (expComparison F A).natTrans.app (A ⊗ B) =
      (exp.coev _).app (F.obj B) ≫ (exp (F.obj A)).map (inv (prodComparison F A B))

Proof state:
case h.e'_3.h.h.e'_7.h.h.e'_8.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
e_1✝ :
  (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (A ⊗ B)) =
    (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (((curriedTensor C).obj A).obj B))
e_4✝ :
  (tensorLeft (F.obj A) ⋙ exp (F.obj A)).obj (F.obj B) =
    ((curriedTensor D).obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_5✝ : (F.obj A ⟹ F.obj (A ⊗ B)) = (F.obj A ⟹ ((curriedTensor C).obj A ⋙ F).obj ((𝟭 C).obj B))
e_6✝ : (tensorLeft (F.obj A)).obj (F.obj B) = ((curriedTensor D).obj (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_7✝ : F.obj (A ⊗ B) = ((curriedTensor C).obj A ⋙ F).obj ((𝟭 C).obj B)
⊢ inv (prodComparison F A B) = (prodComparisonNatIso F A).inv.app ((𝟭 C).obj B)

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Result:
case h.e'_3.h.h.e'_7.h.h.e'_8.h.hom_inv_id
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
e_1✝ :
  (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (A ⊗ B)) =
    (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (((curriedTensor C).obj A).obj B))
e_4✝ :
  (tensorLeft (F.obj A) ⋙ exp (F.obj A)).obj (F.obj B) =
    ((curriedTensor D).obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_5✝ : (F.obj A ⟹ F.obj (A ⊗ B)) = (F.obj A ⟹ ((curriedTensor C).obj A ⋙ F).obj ((𝟭 C).obj B))
e_6✝ : (tensorLeft (F.obj A)).obj (F.obj B) = ((curriedTensor D).obj (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_7✝ : F.obj (A ⊗ B) = ((curriedTensor C).obj A ⋙ F).obj ((𝟭 C).obj B)
⊢ prodComparison F A B ≫ (prodComparisonNatIso F A).inv.app ((𝟭 C).obj B) = 𝟙 (F.obj (A ⊗ B))

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
⊢ F.map ((exp.coev A).app B) ≫ (expComparison F A).natTrans.app (A ⊗ B) =
    (exp.coev (F.obj A)).app (F.obj B) ≫ (exp (F.obj A)).map (inv (prodComparison F A B))

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

Result:
case h.e'_3.h.h.e'_7.h.h.e'_8.h
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
e_1✝ :
  (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (A ⊗ B)) =
    (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (((curriedTensor C).obj A).obj B))
e_4✝ :
  (tensorLeft (F.obj A) ⋙ exp (F.obj A)).obj (F.obj B) =
    ((curriedTensor D).obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_5✝ : (F.obj A ⟹ F.obj (A ⊗ B)) = (F.obj A ⟹ ((curriedTensor C).obj A ⋙ F).obj ((𝟭 C).obj B))
e_6✝ : (tensorLeft (F.obj A)).obj (F.obj B) = ((curriedTensor D).obj (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_7✝ : F.obj (A ⊗ B) = ((curriedTensor C).obj A ⋙ F).obj ((𝟭 C).obj B)
⊢ inv (prodComparison F A B) = (prodComparisonNatIso F A).inv.app ((𝟭 C).obj B)

Proof state:
case h.e'_3.h.h.e'_7.h.h.e'_8.h.hom_inv_id
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
e_1✝ :
  (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (A ⊗ B)) =
    (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (((curriedTensor C).obj A).obj B))
e_4✝ :
  (tensorLeft (F.obj A) ⋙ exp (F.obj A)).obj (F.obj B) =
    ((curriedTensor D).obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_5✝ : (F.obj A ⟹ F.obj (A ⊗ B)) = (F.obj A ⟹ ((curriedTensor C).obj A ⋙ F).obj ((𝟭 C).obj B))
e_6✝ : (tensorLeft (F.obj A)).obj (F.obj B) = ((curriedTensor D).obj (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_7✝ : F.obj (A ⊗ B) = ((curriedTensor C).obj A ⋙ F).obj ((𝟭 C).obj B)
⊢ prodComparison F A B ≫ (prodComparisonNatIso F A).inv.app ((𝟭 C).obj B) = 𝟙 (F.obj (A ⊗ B))

Tactic:
dsimp

Result:
case h.e'_3.h.h.e'_7.h.h.e'_8.h.hom_inv_id
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
e_1✝ :
  (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (A ⊗ B)) =
    (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (((curriedTensor C).obj A).obj B))
e_4✝ :
  (tensorLeft (F.obj A) ⋙ exp (F.obj A)).obj (F.obj B) =
    ((curriedTensor D).obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_5✝ : (F.obj A ⟹ F.obj (A ⊗ B)) = (F.obj A ⟹ ((curriedTensor C).obj A ⋙ F).obj ((𝟭 C).obj B))
e_6✝ : (tensorLeft (F.obj A)).obj (F.obj B) = ((curriedTensor D).obj (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_7✝ : F.obj (A ⊗ B) = ((curriedTensor C).obj A ⋙ F).obj ((𝟭 C).obj B)
⊢ prodComparison F A B ≫ (inv (prodComparisonNatTrans F A)).app B = 𝟙 (F.obj (A ⊗ B))

Proof state:
case h.e'_3.h.h.e'_7.h.h.e'_8.h.hom_inv_id
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
e_1✝ :
  (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (A ⊗ B)) =
    (F.obj ((𝟭 C).obj B) ⟶ (F ⋙ exp (F.obj A)).obj (((curriedTensor C).obj A).obj B))
e_4✝ :
  (tensorLeft (F.obj A) ⋙ exp (F.obj A)).obj (F.obj B) =
    ((curriedTensor D).obj (F.obj A) ⋙ exp (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_5✝ : (F.obj A ⟹ F.obj (A ⊗ B)) = (F.obj A ⟹ ((curriedTensor C).obj A ⋙ F).obj ((𝟭 C).obj B))
e_6✝ : (tensorLeft (F.obj A)).obj (F.obj B) = ((curriedTensor D).obj (F.obj A)).obj (F.obj ((𝟭 C).obj B))
e_7✝ : F.obj (A ⊗ B) = ((curriedTensor C).obj A ⋙ F).obj ((𝟭 C).obj B)
⊢ prodComparison F A B ≫ (inv (prodComparisonNatTrans F A)).app B = 𝟙 (F.obj (A ⊗ B))

Tactic:
simp

Result:
no goals