no goals
C : Type u
inst✝⁵ : Category C
A B X X' Y Y' Z : C
inst✝⁴ : HasFiniteProducts C
inst✝³ : Exponentiable A
A₁ A₂ A₃ : C
inst✝² : Exponentiable A₁
inst✝¹ : Exponentiable A₂
inst✝ : Exponentiable A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
⊢ pre (f ≫ g) = pre g ≫ pre f
rw [pre, pre, pre, transferNatTransSelf_comp, prod.functor.map_comp]