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 : X' ⟶ X
g : X ⟶ G.obj Y
⊢ ↑(homEquiv adj X' Y).symm (f ≫ g) = F.map f ≫ ↑(homEquiv adj X Y).symm g
rw [homEquiv_counit, F.map_comp, assoc, adj.homEquiv_counit.symm]