case a
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ (adj1.unit.app x ≫ (rightAdjointUniq adj1 adj2).hom.app (F.obj x)).op = (adj2.unit.app x).op
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ adj1.unit.app x ≫ (rightAdjointUniq adj1 adj2).hom.app (F.obj x) = adj2.unit.app x
apply Quiver.Hom.op_inj
case h.e'_2.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
e_1✝ : ((G'.obj (F.obj x)).op ⟶ ((𝟭 C).obj x).op) = ((Functor.op G').obj ((Functor.op F).obj x.op) ⟶ (𝟭 Cᵒᵖ).obj x.op)
⊢ (adj1.unit.app x ≫ (rightAdjointUniq adj1 adj2).hom.app (F.obj x)).op =
    (leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom.app
        ((Functor.op F).obj x.op) ≫
      (opAdjointOpOfAdjoint G F adj1).counit.app x.op

case h.e'_3.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
e_1✝ : ((G'.obj (F.obj x)).op ⟶ ((𝟭 C).obj x).op) = ((Functor.op G').obj ((Functor.op F).obj x.op) ⟶ (𝟭 Cᵒᵖ).obj x.op)
⊢ (adj2.unit.app x).op = (opAdjointOpOfAdjoint G' F adj2).counit.app x.op
case a
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ (adj1.unit.app x ≫ (rightAdjointUniq adj1 adj2).hom.app (F.obj x)).op = (adj2.unit.app x).op
convert
  leftAdjointUniq_hom_app_counit (opAdjointOpOfAdjoint _ _ adj2)
    (opAdjointOpOfAdjoint _ _ adj1) (Opposite.op x) using 1
no goals
case h.e'_2.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
e_1✝ : ((G'.obj (F.obj x)).op ⟶ ((𝟭 C).obj x).op) = ((Functor.op G').obj ((Functor.op F).obj x.op) ⟶ (𝟭 Cᵒᵖ).obj x.op)
⊢ (adj1.unit.app x ≫ (rightAdjointUniq adj1 adj2).hom.app (F.obj x)).op =
    (leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom.app
        ((Functor.op F).obj x.op) ≫
      (opAdjointOpOfAdjoint G F adj1).counit.app x.op

case h.e'_3.h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
e_1✝ : ((G'.obj (F.obj x)).op ⟶ ((𝟭 C).obj x).op) = ((Functor.op G').obj ((Functor.op F).obj x.op) ⟶ (𝟭 Cᵒᵖ).obj x.op)
⊢ (adj2.unit.app x).op = (opAdjointOpOfAdjoint G' F adj2).counit.app x.op
all_goals {
  simp only [Functor.id_obj, Functor.comp_obj, op_comp, Functor.op_obj, Opposite.unop_op,
    opAdjointOpOfAdjoint, mkOfHomEquiv_counit_app, Equiv.invFun_as_coe, Equiv.symm_trans_apply,
    Equiv.symm_symm, homEquiv_unit]
  erw [Functor.map_id]
  rw [Category.comp_id]
  rfl }