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₁
g : L₁ ⟶ L₂
gf : g ≫ f = 𝟙 L₁
⊢ ↑(transferNatTransSelf adj₁ adj₂) f ≫ ↑(transferNatTransSelf adj₂ adj₁) g = 𝟙 R₁
rw [transferNatTransSelf_comp, gf, transferNatTransSelf_id]