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
X : C
⊢ G.map (adj₁.unit.app X) ≫
      adj₂.unit.app (G.obj (R₁.obj (L₁.obj X))) ≫
        R₂.map (f.app (R₁.obj (L₁.obj X)) ≫ H.map (adj₁.counit.app (L₁.obj X))) =
    adj₂.unit.app (G.obj X) ≫ R₂.map (f.app X)
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
X : C
⊢ G.map (adj₁.unit.app X) ≫ (↑(transferNatTrans adj₁ adj₂) f).app (L₁.obj X) =
    adj₂.unit.app (G.obj ((𝟭 C).obj X)) ≫ R₂.map (f.app ((𝟭 C).obj X))
dsimp [transferNatTrans]
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
X : C
⊢ adj₂.unit.app (G.obj X) ≫ R₂.map (f.app X ≫ H.map (L₁.map (adj₁.unit.app X) ≫ adj₁.counit.app (L₁.obj X))) =
    adj₂.unit.app (G.obj X) ≫ R₂.map (f.app X)
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
X : C
⊢ G.map (adj₁.unit.app X) ≫
      adj₂.unit.app (G.obj (R₁.obj (L₁.obj X))) ≫
        R₂.map (f.app (R₁.obj (L₁.obj X)) ≫ H.map (adj₁.counit.app (L₁.obj X))) =
    adj₂.unit.app (G.obj X) ≫ R₂.map (f.app X)
rw [← adj₂.unit_naturality_assoc, ← R₂.map_comp, ← Functor.comp_map G L₂, f.naturality_assoc,
  Functor.comp_map, ← H.map_comp]
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
X : C
⊢ adj₂.unit.app (G.obj X) ≫ R₂.map (f.app X ≫ H.map (L₁.map (adj₁.unit.app X) ≫ adj₁.counit.app (L₁.obj X))) =
    adj₂.unit.app (G.obj X) ≫ R₂.map (f.app X)
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
X : C
⊢ adj₂.unit.app (G.obj X) ≫ R₂.map (f.app X ≫ H.map (L₁.map (adj₁.unit.app X) ≫ adj₁.counit.app (L₁.obj X))) =
    adj₂.unit.app (G.obj X) ≫ R₂.map (f.app X)
dsimp
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
X : C
⊢ adj₂.unit.app (G.obj X) ≫ R₂.map (f.app X ≫ H.map (L₁.map (adj₁.unit.app X) ≫ adj₁.counit.app (L₁.obj X))) =
    adj₂.unit.app (G.obj X) ≫ R₂.map (f.app X)
simp