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
W X Y Z : C
inst✝¹ : Closed W
inst✝ : Closed X
f : W ⟶ X
g : Y ⟶ Z
⊢ (pre f).app Y ≫ (ihom W).map g = (ihom X).map g ≫ (pre f).app Z
simp