no goals
C : Type u
inst✝³ : Category C
A B X✝ X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A
f : B ⟶ A
inst✝ : Exponentiable B
X : C
⊢ CartesianClosed.uncurry ((pre f).app X) = prod.map f (𝟙 (A ⟹ X)) ≫ (exp.ev A).app X
rw [uncurry_eq, prod_map_pre_app_comp_ev]