C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x : C
⊢ (leftAdjointUniq adj1 adj2).hom.app x ≫ (leftAdjointUniq adj2 adj3).hom.app x =
    ((leftAdjointUniq adj1 adj2).hom ≫ (leftAdjointUniq adj2 adj3).hom).app x
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x : C
⊢ (leftAdjointUniq adj1 adj2).hom.app x ≫ (leftAdjointUniq adj2 adj3).hom.app x = (leftAdjointUniq adj1 adj3).hom.app x
rw [← leftAdjointUniq_trans adj1 adj2 adj3]
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x : C
⊢ (leftAdjointUniq adj1 adj2).hom.app x ≫ (leftAdjointUniq adj2 adj3).hom.app x =
    ((leftAdjointUniq adj1 adj2).hom ≫ (leftAdjointUniq adj2 adj3).hom).app x
rfl