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₃
L R : C ⥤ C
adj : L ⊣ R
g : R ⟶ 𝟭 C
X : C
⊢ 𝟙 X ≫ ((adj.unit.app X ≫ 𝟙 (R.obj (L.obj X)) ≫ g.app (L.obj X) ≫ 𝟙 (L.obj X)) ≫ 𝟙 (L.obj X)) ≫ 𝟙 (L.obj X) =
    adj.unit.app X ≫ g.app (L.obj 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₃
L R : C ⥤ C
adj : L ⊣ R
g : R ⟶ 𝟭 C
X : C
⊢ (↑(transferNatTransSelf adj Adjunction.id).symm g).app X = adj.unit.app X ≫ g.app (L.obj X)
dsimp [transferNatTransSelf, transferNatTrans, Adjunction.id]
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₃
L R : C ⥤ C
adj : L ⊣ R
g : R ⟶ 𝟭 C
X : C
⊢ 𝟙 X ≫ ((adj.unit.app X ≫ 𝟙 (R.obj (L.obj X)) ≫ g.app (L.obj X) ≫ 𝟙 (L.obj X)) ≫ 𝟙 (L.obj X)) ≫ 𝟙 (L.obj X) =
    adj.unit.app X ≫ g.app (L.obj X)
simp only [comp_id, id_comp]