diff --git a/Mathlib/CategoryTheory/Functor/Currying.lean b/Mathlib/CategoryTheory/Functor/Currying.lean
index edaba6e369347..e130aedb422c8 100644
--- a/Mathlib/CategoryTheory/Functor/Currying.lean
+++ b/Mathlib/CategoryTheory/Functor/Currying.lean
@@ -3,6 +3,7 @@ Copyright (c) 2017 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+import Mathlib.CategoryTheory.EqToHom
 import Mathlib.CategoryTheory.Products.Basic
 
 /-!
diff --git a/Mathlib/CategoryTheory/Monoidal/Category.lean b/Mathlib/CategoryTheory/Monoidal/Category.lean
index c38de64d692f4..d80764aa71802 100644
--- a/Mathlib/CategoryTheory/Monoidal/Category.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Category.lean
@@ -3,6 +3,7 @@ Copyright (c) 2018 Michael Jendrusch. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Jendrusch, Kim Morrison, Bhavik Mehta, Jakob von Raumer
 -/
+import Mathlib.CategoryTheory.EqToHom
 import Mathlib.CategoryTheory.Functor.Trifunctor
 import Mathlib.CategoryTheory.Products.Basic
 
diff --git a/Mathlib/CategoryTheory/Products/Basic.lean b/Mathlib/CategoryTheory/Products/Basic.lean
index c38b430629b3b..58958ff88a2de 100644
--- a/Mathlib/CategoryTheory/Products/Basic.lean
+++ b/Mathlib/CategoryTheory/Products/Basic.lean
@@ -3,7 +3,6 @@ Copyright (c) 2017 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Stephen Morgan, Kim Morrison
 -/
-import Mathlib.CategoryTheory.EqToHom
 import Mathlib.CategoryTheory.Functor.Const
 import Mathlib.CategoryTheory.Opposites
 import Mathlib.Data.Prod.Basic
@@ -296,7 +295,18 @@ end Equivalence
 /-- `F.flip` composed with evaluation is the same as evaluating `F`. -/
 @[simps!]
 def flipCompEvaluation (F : A ⥤ B ⥤ C) (a) : F.flip ⋙ (evaluation _ _).obj a ≅ F.obj a :=
-  NatIso.ofComponents fun b => eqToIso rfl
+  NatIso.ofComponents fun b => Iso.refl _
+
+theorem flip_comp_evaluation (F : A ⥤ B ⥤ C) (a) : F.flip ⋙ (evaluation _ _).obj a = F.obj a :=
+  rfl
+
+/-- `F` composed with evaluation is the same as evaluating `F.flip`. -/
+@[simps!]
+def compEvaluation (F : A ⥤ B ⥤ C) (b) : F ⋙ (evaluation _ _).obj b ≅ F.flip.obj b :=
+  NatIso.ofComponents fun a => Iso.refl _
+
+theorem comp_evaluation (F : A ⥤ B ⥤ C) (b) : F ⋙ (evaluation _ _).obj b = F.flip.obj b :=
+  rfl
 
 variable (A B C)