C : Type u₁
D : Type u₂
inst✝³ : Category C
inst✝² : Category D
E : Type u₃
F : Type u₄
inst✝¹ : Category E
inst✝ : Category F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ⋙ L₂ ⟶ L₁ ⋙ H
Y : D
⊢ (L₂.map (adj₂.unit.app (G.obj (R₁.obj Y))) ≫ L₂.map (R₂.map (f.app (R₁.obj Y) ≫ H.map (adj₁.counit.app Y)))) ≫
      adj₂.counit.app (H.obj Y) =
    f.app (R₁.obj Y) ≫ H.map (adj₁.counit.app Y)
C : Type u₁
D : Type u₂
inst✝³ : Category C
inst✝² : Category D
E : Type u₃
F : Type u₄
inst✝¹ : Category E
inst✝ : Category F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ⋙ L₂ ⟶ L₁ ⋙ H
Y : D
⊢ L₂.map ((↑(transferNatTrans adj₁ adj₂) f).app Y) ≫ adj₂.counit.app (H.obj Y) =
    f.app (R₁.obj Y) ≫ H.map (adj₁.counit.app Y)
erw [Functor.map_comp]
no goals
C : Type u₁
D : Type u₂
inst✝³ : Category C
inst✝² : Category D
E : Type u₃
F : Type u₄
inst✝¹ : Category E
inst✝ : Category F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ⋙ L₂ ⟶ L₁ ⋙ H
Y : D
⊢ (L₂.map (adj₂.unit.app (G.obj (R₁.obj Y))) ≫ L₂.map (R₂.map (f.app (R₁.obj Y) ≫ H.map (adj₁.counit.app Y)))) ≫
      adj₂.counit.app (H.obj Y) =
    f.app (R₁.obj Y) ≫ H.map (adj₁.counit.app Y)
simp