C : Type u_4
D : Type u_1
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ G.map u ≫ adj.counit.app X ≫ p = G.map (u ≫ F.map p) ≫ adj.counit.app Y
C : Type u_4
D : Type u_1
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ ↑(Adjunction.homEquiv adj A X).symm u ≫ p = G.map i ≫ ↑(Adjunction.homEquiv adj B Y).symm v
simp only [Adjunction.homEquiv_counit, assoc, ← G.map_comp_assoc, ← sq.w]
no goals
C : Type u_4
D : Type u_1
inst✝¹ : Category C
inst✝ : Category D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : A ⟶ F.obj X
v : B ⟶ F.obj Y
sq : CommSq u i (F.map p) v
adj : G ⊣ F
⊢ G.map u ≫ adj.counit.app X ≫ p = G.map (u ≫ F.map p) ≫ adj.counit.app Y
rw [G.map_comp, assoc, Adjunction.counit_naturality]