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

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.obj A ◁ (expComparison F A).natTrans.app B ≫ (exp.ev (F.obj A)).app (F.obj B) =
    inv (prodComparison F A (A ⟹ B)) ≫ F.map ((exp.ev A).app B)

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

Result:
case h.e'_3.h.h.e'_6.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 A ⊗ (exp A ⋙ F).obj B ⟶ (𝟭 D).obj (F.obj B)) =
    (((curriedTensor D).obj (F.obj A)).obj ((exp A ⋙ F).obj B) ⟶ (𝟭 D).obj (F.obj B))
e_3✝ : F.obj A ⊗ F.obj (A ⟹ B) = (F ⋙ (curriedTensor D).obj (F.obj A)).obj (A ⟹ B)
e_4✝ : F.obj (A ⊗ (A ⟹ B)) = ((curriedTensor C).obj A ⋙ F).obj (A ⟹ B)
⊢ inv (prodComparison F A (A ⟹ B)) = (prodComparisonNatIso F A).inv.app (A ⟹ B)

Proof state:
case h.e'_3.h.h.e'_6.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 A ⊗ (exp A ⋙ F).obj B ⟶ (𝟭 D).obj (F.obj B)) =
    (((curriedTensor D).obj (F.obj A)).obj ((exp A ⋙ F).obj B) ⟶ (𝟭 D).obj (F.obj B))
e_3✝ : F.obj A ⊗ F.obj (A ⟹ B) = (F ⋙ (curriedTensor D).obj (F.obj A)).obj (A ⟹ B)
e_4✝ : F.obj (A ⊗ (A ⟹ B)) = ((curriedTensor C).obj A ⋙ F).obj (A ⟹ B)
⊢ prodComparison F A (A ⟹ B) ≫ (prodComparisonNatIso F A).inv.app (A ⟹ B) = 𝟙 (F.obj (A ⊗ (A ⟹ B)))

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

Result:
no goals

Proof state:
case h.e'_3.h.h.e'_6.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 A ⊗ (exp A ⋙ F).obj B ⟶ (𝟭 D).obj (F.obj B)) =
    (((curriedTensor D).obj (F.obj A)).obj ((exp A ⋙ F).obj B) ⟶ (𝟭 D).obj (F.obj B))
e_3✝ : F.obj A ⊗ F.obj (A ⟹ B) = (F ⋙ (curriedTensor D).obj (F.obj A)).obj (A ⟹ B)
e_4✝ : F.obj (A ⊗ (A ⟹ B)) = ((curriedTensor C).obj A ⋙ F).obj (A ⟹ B)
⊢ inv (prodComparison F A (A ⟹ B)) = (prodComparisonNatIso F A).inv.app (A ⟹ B)

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Result:
case h.e'_3.h.h.e'_6.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 A ⊗ (exp A ⋙ F).obj B ⟶ (𝟭 D).obj (F.obj B)) =
    (((curriedTensor D).obj (F.obj A)).obj ((exp A ⋙ F).obj B) ⟶ (𝟭 D).obj (F.obj B))
e_3✝ : F.obj A ⊗ F.obj (A ⟹ B) = (F ⋙ (curriedTensor D).obj (F.obj A)).obj (A ⟹ B)
e_4✝ : F.obj (A ⊗ (A ⟹ B)) = ((curriedTensor C).obj A ⋙ F).obj (A ⟹ B)
⊢ prodComparison F A (A ⟹ B) ≫ (prodComparisonNatIso F A).inv.app (A ⟹ B) = 𝟙 (F.obj (A ⊗ (A ⟹ B)))