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 : C
⊢ adj₁.unit.app X ≫
      𝟙 (R₁.obj (L₁.obj X)) ≫
        (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app
            (L₁.obj X) ≫
          𝟙 (R₂.obj (L₁.obj X)) =
    adj₂.unit.app X ≫ R₂.map (f.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 : C
⊢ adj₁.unit.app X ≫ (↑(transferNatTransSelf adj₁ adj₂) f).app (L₁.obj X) = adj₂.unit.app X ≫ R₂.map (f.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 : C
⊢ adj₁.unit.app X ≫
      (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app (L₁.obj X) =
    adj₂.unit.app X ≫ R₂.map (f.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 : C
⊢ adj₁.unit.app X ≫
      𝟙 (R₁.obj (L₁.obj X)) ≫
        (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app
            (L₁.obj X) ≫
          𝟙 (R₂.obj (L₁.obj X)) =
    adj₂.unit.app X ≫ R₂.map (f.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 : C
this :
  (𝟭 C).map (adj₁.unit.app X) ≫
      (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app (L₁.obj X) =
    adj₂.unit.app ((𝟭 C).obj ((𝟭 C).obj X)) ≫
      R₂.map (((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv).app ((𝟭 C).obj X))
⊢ adj₁.unit.app X ≫
      (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app (L₁.obj X) =
    adj₂.unit.app X ≫ R₂.map (f.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 : C
⊢ adj₁.unit.app X ≫
      (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app (L₁.obj X) =
    adj₂.unit.app X ≫ R₂.map (f.app X)
have := unit_transferNatTrans 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 : C
this :
  adj₁.unit.app X ≫
      (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app (L₁.obj X) =
    adj₂.unit.app X ≫ R₂.map (𝟙 (L₂.obj X) ≫ f.app X ≫ 𝟙 (L₁.obj X))
⊢ adj₁.unit.app X ≫
      (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app (L₁.obj X) =
    adj₂.unit.app X ≫ R₂.map (f.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 : C
this :
  (𝟭 C).map (adj₁.unit.app X) ≫
      (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app (L₁.obj X) =
    adj₂.unit.app ((𝟭 C).obj ((𝟭 C).obj X)) ≫
      R₂.map (((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv).app ((𝟭 C).obj X))
⊢ adj₁.unit.app X ≫
      (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app (L₁.obj X) =
    adj₂.unit.app X ≫ R₂.map (f.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 : C
this :
  adj₁.unit.app X ≫
      (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app (L₁.obj X) =
    adj₂.unit.app X ≫ R₂.map (𝟙 (L₂.obj X) ≫ f.app X ≫ 𝟙 (L₁.obj X))
⊢ adj₂.unit.app X ≫ R₂.map (𝟙 (L₂.obj X) ≫ f.app X ≫ 𝟙 (L₁.obj X)) = adj₂.unit.app X ≫ R₂.map (f.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 : C
this :
  adj₁.unit.app X ≫
      (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app (L₁.obj X) =
    adj₂.unit.app X ≫ R₂.map (𝟙 (L₂.obj X) ≫ f.app X ≫ 𝟙 (L₁.obj X))
⊢ adj₁.unit.app X ≫
      (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app (L₁.obj X) =
    adj₂.unit.app X ≫ R₂.map (f.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 : C
this :
  adj₁.unit.app X ≫
      (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv)).app (L₁.obj X) =
    adj₂.unit.app X ≫ R₂.map (𝟙 (L₂.obj X) ≫ f.app X ≫ 𝟙 (L₁.obj X))
⊢ adj₂.unit.app X ≫ R₂.map (𝟙 (L₂.obj X) ≫ f.app X ≫ 𝟙 (L₁.obj X)) = adj₂.unit.app X ≫ R₂.map (f.app X)
simp