no goals
C : Type u
inst✝³ : Category C
inst✝² : MonoidalCategory C
A B X✝ X' Y Y' Z : C
inst✝¹ : Closed A
inst✝ : Closed B
f : B ⟶ A
X : C
⊢ uncurry ((pre f).app X) = (f ⊗ 𝟙 ((ihom A).obj X)) ≫ (ihom.ev A).app X
rw [uncurry_eq, id_tensor_pre_app_comp_ev]