∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J : C} (f : I ⟶ J)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ExponentiableMorphism f],
  CategoryTheory.ExponentiableMorphism.ev f = (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj f).counit