case a
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ ((rightAdjointUniq adj1 adj2).hom.app x ≫ (rightAdjointUniq adj2 adj3).hom.app x).op =
    ((rightAdjointUniq adj1 adj3).hom.app x).op
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ (rightAdjointUniq adj1 adj2).hom.app x ≫ (rightAdjointUniq adj2 adj3).hom.app x =
    (rightAdjointUniq adj1 adj3).hom.app x
apply Quiver.Hom.op_inj
case a
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ (leftAdjointUniq (opAdjointOpOfAdjoint G'' F adj3) (opAdjointOpOfAdjoint G' F adj2)).hom.app x.op ≫
      (leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom.app x.op =
    (leftAdjointUniq (opAdjointOpOfAdjoint G'' F adj3) (opAdjointOpOfAdjoint G F adj1)).hom.app x.op
case a
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ ((rightAdjointUniq adj1 adj2).hom.app x ≫ (rightAdjointUniq adj2 adj3).hom.app x).op =
    ((rightAdjointUniq adj1 adj3).hom.app x).op
dsimp [rightAdjointUniq]
no goals
case a
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ (leftAdjointUniq (opAdjointOpOfAdjoint G'' F adj3) (opAdjointOpOfAdjoint G' F adj2)).hom.app x.op ≫
      (leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom.app x.op =
    (leftAdjointUniq (opAdjointOpOfAdjoint G'' F adj3) (opAdjointOpOfAdjoint G F adj1)).hom.app x.op
simp