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
A₁ A₂ A₃ : C
inst✝² : Closed A₁
inst✝¹ : Closed A₂
inst✝ : Closed A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
⊢ pre (f ≫ g) = pre g ≫ pre f
rw [pre, pre, pre, transferNatTransSelf_comp, (tensoringLeft C).map_comp]