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