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