C : Type u₁
D : Type u₂
inst✝¹ : Category C
inst✝ : Category D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
⊢ L₂.map
        (𝟙 (R₁.obj X) ≫
          (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app X ≫
            𝟙 (R₂.obj X)) ≫
      adj₂.counit.app X =
    f.app (R₁.obj X) ≫ adj₁.counit.app X
C : Type u₁
D : Type u₂
inst✝¹ : Category C
inst✝ : Category D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
⊢ L₂.map ((↑(transferNatTransSelf adj₁ adj₂) f).app X) ≫ adj₂.counit.app X = f.app (R₁.obj X) ≫ adj₁.counit.app X
dsimp [transferNatTransSelf]
C : Type u₁
D : Type u₂
inst✝¹ : Category C
inst✝ : Category D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
⊢ L₂.map ((↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app X) ≫
      adj₂.counit.app X =
    f.app (R₁.obj X) ≫ adj₁.counit.app X
C : Type u₁
D : Type u₂
inst✝¹ : Category C
inst✝ : Category D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
⊢ L₂.map
        (𝟙 (R₁.obj X) ≫
          (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app X ≫
            𝟙 (R₂.obj X)) ≫
      adj₂.counit.app X =
    f.app (R₁.obj X) ≫ adj₁.counit.app X
rw [id_comp, comp_id]
C : Type u₁
D : Type u₂
inst✝¹ : Category C
inst✝ : Category D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
this :
  L₂.map ((↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app X) ≫
      adj₂.counit.app ((𝟭 D).obj X) =
    ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv).app (R₁.obj X) ≫ (𝟭 D).map (adj₁.counit.app X)
⊢ L₂.map ((↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app X) ≫
      adj₂.counit.app X =
    f.app (R₁.obj X) ≫ adj₁.counit.app X
C : Type u₁
D : Type u₂
inst✝¹ : Category C
inst✝ : Category D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
⊢ L₂.map ((↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app X) ≫
      adj₂.counit.app X =
    f.app (R₁.obj X) ≫ adj₁.counit.app X
have := transferNatTrans_counit adj₁ adj₂ (L₂.leftUnitor.hom ≫ f ≫ L₁.rightUnitor.inv) X
C : Type u₁
D : Type u₂
inst✝¹ : Category C
inst✝ : Category D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
this :
  L₂.map ((↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app X) ≫
      adj₂.counit.app X =
    (𝟙 (L₂.obj (R₁.obj X)) ≫ f.app (R₁.obj X) ≫ 𝟙 (L₁.obj (R₁.obj X))) ≫ adj₁.counit.app X
⊢ L₂.map ((↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app X) ≫
      adj₂.counit.app X =
    f.app (R₁.obj X) ≫ adj₁.counit.app X
C : Type u₁
D : Type u₂
inst✝¹ : Category C
inst✝ : Category D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
this :
  L₂.map ((↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app X) ≫
      adj₂.counit.app ((𝟭 D).obj X) =
    ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv).app (R₁.obj X) ≫ (𝟭 D).map (adj₁.counit.app X)
⊢ L₂.map ((↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app X) ≫
      adj₂.counit.app X =
    f.app (R₁.obj X) ≫ adj₁.counit.app X
dsimp at this
C : Type u₁
D : Type u₂
inst✝¹ : Category C
inst✝ : Category D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
this :
  L₂.map ((↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app X) ≫
      adj₂.counit.app X =
    (𝟙 (L₂.obj (R₁.obj X)) ≫ f.app (R₁.obj X) ≫ 𝟙 (L₁.obj (R₁.obj X))) ≫ adj₁.counit.app X
⊢ (𝟙 (L₂.obj (R₁.obj X)) ≫ f.app (R₁.obj X) ≫ 𝟙 (L₁.obj (R₁.obj X))) ≫ adj₁.counit.app X =
    f.app (R₁.obj X) ≫ adj₁.counit.app X
C : Type u₁
D : Type u₂
inst✝¹ : Category C
inst✝ : Category D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
this :
  L₂.map ((↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app X) ≫
      adj₂.counit.app X =
    (𝟙 (L₂.obj (R₁.obj X)) ≫ f.app (R₁.obj X) ≫ 𝟙 (L₁.obj (R₁.obj X))) ≫ adj₁.counit.app X
⊢ L₂.map ((↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app X) ≫
      adj₂.counit.app X =
    f.app (R₁.obj X) ≫ adj₁.counit.app X
rw [this]
no goals
C : Type u₁
D : Type u₂
inst✝¹ : Category C
inst✝ : Category D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
this :
  L₂.map ((↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app X) ≫
      adj₂.counit.app X =
    (𝟙 (L₂.obj (R₁.obj X)) ≫ f.app (R₁.obj X) ≫ 𝟙 (L₁.obj (R₁.obj X))) ≫ adj₁.counit.app X
⊢ (𝟙 (L₂.obj (R₁.obj X)) ≫ f.app (R₁.obj X) ≫ 𝟙 (L₁.obj (R₁.obj X))) ≫ adj₁.counit.app X =
    f.app (R₁.obj X) ≫ adj₁.counit.app X
simp