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₂
⊢ ↑(transferNatTransSelf adj₃ adj₂) (↑(transferNatTransSelf adj₃ adj₂).symm g) ≫
      ↑(transferNatTransSelf adj₂ adj₁) (↑(transferNatTransSelf adj₂ adj₁).symm f) =
    g ≫ f
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₂
⊢ ↑(transferNatTransSelf adj₂ adj₁).symm f ≫ ↑(transferNatTransSelf adj₃ adj₂).symm g =
    ↑(transferNatTransSelf adj₃ adj₁).symm (g ≫ f)
rw [Equiv.eq_symm_apply, ← transferNatTransSelf_comp _ adj₂]
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₂
⊢ ↑(transferNatTransSelf adj₃ adj₂) (↑(transferNatTransSelf adj₃ adj₂).symm g) ≫
      ↑(transferNatTransSelf adj₂ adj₁) (↑(transferNatTransSelf adj₂ adj₁).symm f) =
    g ≫ f
simp