no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
f : F.obj X ⟶ Y
g : Y ⟶ Y'
⊢ ↑(homEquiv adj X Y') (f ≫ g) = ↑(homEquiv adj X Y) f ≫ G.map g
rw [homEquiv_unit, G.map_comp, ← assoc, ← homEquiv_unit]