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 : D
⊢ (↑(homEquiv adj2 (G.obj x) x).symm ((rightAdjointUniq adj1 adj2).hom.app x)).op = (adj1.counit.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 : D
⊢ ↑(homEquiv adj2 (G.obj x) x).symm ((rightAdjointUniq adj1 adj2).hom.app x) = adj1.counit.app x
apply Quiver.Hom.op_inj
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 : D
e_1✝ :
  (x.op ⟶ (F.obj (G.obj x)).op) =
    (fun x_1 => x.op ⟶ (Functor.op F).obj ((Functor.op G).obj x.op))
      ((leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom.app x.op)
⊢ (adj1.counit.app x).op = (opAdjointOpOfAdjoint G F adj1).unit.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 : D
⊢ (↑(homEquiv adj2 (G.obj x) x).symm ((rightAdjointUniq adj1 adj2).hom.app x)).op = (adj1.counit.app x).op
convert homEquiv_leftAdjointUniq_hom_app (opAdjointOpOfAdjoint _ F adj2)
  (opAdjointOpOfAdjoint _ _ adj1) (Opposite.op x)
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 : D
e_1✝ :
  (x.op ⟶ (F.obj (G.obj x)).op) =
    (fun x_1 => x.op ⟶ (Functor.op F).obj ((Functor.op G).obj x.op))
      ((leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom.app x.op)
⊢ (adj1.counit.app x).op =
    ↑(opEquiv x.op (F.toPrefunctor.1 (G.obj x)).op).symm
      (F.map (↑(opEquiv (G.obj x).op (G.obj x).op) (𝟙 (G.obj x).op)) ≫ adj1.counit.app x)
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 : D
e_1✝ :
  (x.op ⟶ (F.obj (G.obj x)).op) =
    (fun x_1 => x.op ⟶ (Functor.op F).obj ((Functor.op G).obj x.op))
      ((leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom.app x.op)
⊢ (adj1.counit.app x).op = (opAdjointOpOfAdjoint G F adj1).unit.app x.op
simp only [opAdjointOpOfAdjoint, Functor.op_obj, Opposite.unop_op, mkOfHomEquiv_unit_app,
  Equiv.trans_apply, homEquiv_counit, Functor.id_obj]
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 : D
e_1✝ :
  (x.op ⟶ (F.obj (G.obj x)).op) =
    (fun x_1 => x.op ⟶ (Functor.op F).obj ((Functor.op G).obj x.op))
      ((leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom.app x.op)
⊢ (adj1.counit.app x).op =
    ↑(opEquiv x.op (F.toPrefunctor.1 (G.obj x)).op).symm (𝟙 (F.obj (G.obj x)) ≫ adj1.counit.app x)
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 : D
e_1✝ :
  (x.op ⟶ (F.obj (G.obj x)).op) =
    (fun x_1 => x.op ⟶ (Functor.op F).obj ((Functor.op G).obj x.op))
      ((leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom.app x.op)
⊢ (adj1.counit.app x).op =
    ↑(opEquiv x.op (F.toPrefunctor.1 (G.obj x)).op).symm
      (F.map (↑(opEquiv (G.obj x).op (G.obj x).op) (𝟙 (G.obj x).op)) ≫ adj1.counit.app x)
erw [F.map_id]
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 : D
e_1✝ :
  (x.op ⟶ (F.obj (G.obj x)).op) =
    (fun x_1 => x.op ⟶ (Functor.op F).obj ((Functor.op G).obj x.op))
      ((leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom.app x.op)
⊢ (adj1.counit.app x).op = ↑(opEquiv x.op (F.toPrefunctor.1 (G.obj x)).op).symm (adj1.counit.app x)
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 : D
e_1✝ :
  (x.op ⟶ (F.obj (G.obj x)).op) =
    (fun x_1 => x.op ⟶ (Functor.op F).obj ((Functor.op G).obj x.op))
      ((leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom.app x.op)
⊢ (adj1.counit.app x).op =
    ↑(opEquiv x.op (F.toPrefunctor.1 (G.obj x)).op).symm (𝟙 (F.obj (G.obj x)) ≫ adj1.counit.app x)
rw [Category.id_comp]
no goals
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 : D
e_1✝ :
  (x.op ⟶ (F.obj (G.obj x)).op) =
    (fun x_1 => x.op ⟶ (Functor.op F).obj ((Functor.op G).obj x.op))
      ((leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom.app x.op)
⊢ (adj1.counit.app x).op = ↑(opEquiv x.op (F.toPrefunctor.1 (G.obj x)).op).symm (adj1.counit.app x)
rfl