[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
h : G.op ⊣ F.op
⊢ ∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y),
    ↑(fun {X} {Y} =>
              ((homEquiv h (Opposite.op Y) (Opposite.op X)).trans
                      (opEquiv (Opposite.op Y) (F.op.obj (Opposite.op X)))).symm.trans
                (opEquiv (G.op.obj (Opposite.op Y)) (Opposite.op X))).symm
        (f ≫ g) =
      F.map f ≫
        ↑(fun {X} {Y} =>
                ((homEquiv h (Opposite.op Y) (Opposite.op X)).trans
                        (opEquiv (Opposite.op Y) (F.op.obj (Opposite.op X)))).symm.trans
                  (opEquiv (G.op.obj (Opposite.op Y)) (Opposite.op X))).symm
          g
[PROOFSTEP]
intros X' X Y f g
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
h : G.op ⊣ F.op
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
⊢ ↑(fun {X} {Y} =>
            ((homEquiv h (Opposite.op Y) (Opposite.op X)).trans
                    (opEquiv (Opposite.op Y) (F.op.obj (Opposite.op X)))).symm.trans
              (opEquiv (G.op.obj (Opposite.op Y)) (Opposite.op X))).symm
      (f ≫ g) =
    F.map f ≫
      ↑(fun {X} {Y} =>
              ((homEquiv h (Opposite.op Y) (Opposite.op X)).trans
                      (opEquiv (Opposite.op Y) (F.op.obj (Opposite.op X)))).symm.trans
                (opEquiv (G.op.obj (Opposite.op Y)) (Opposite.op X))).symm
        g
[PROOFSTEP]
dsimp [opEquiv]
  -- Porting note: Why is `erw` needed here?
        -- https://github.com/leanprover-community/mathlib4/issues/5164
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
h : G.op ⊣ F.op
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
⊢ (↑(homEquiv h (Opposite.op Y) (Opposite.op X')) (g.op ≫ f.op)).unop =
    F.map f ≫ (↑(homEquiv h (Opposite.op Y) (Opposite.op X)) g.op).unop
[PROOFSTEP]
erw [homEquiv_unit, homEquiv_unit]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
h : G.op ⊣ F.op
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
⊢ (NatTrans.app h.unit (Opposite.op Y) ≫ F.op.map (g.op ≫ f.op)).unop =
    F.map f ≫ (NatTrans.app h.unit (Opposite.op Y) ≫ F.op.map g.op).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
h : G.op ⊣ F.op
⊢ ∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'),
    (↑fun {X} {Y} =>
          ((homEquiv h (Opposite.op Y) (Opposite.op X)).trans
                  (opEquiv (Opposite.op Y) (F.op.obj (Opposite.op X)))).symm.trans
            (opEquiv (G.op.obj (Opposite.op Y)) (Opposite.op X)))
        (f ≫ g) =
      (↑fun {X} {Y} =>
            ((homEquiv h (Opposite.op Y) (Opposite.op X)).trans
                    (opEquiv (Opposite.op Y) (F.op.obj (Opposite.op X)))).symm.trans
              (opEquiv (G.op.obj (Opposite.op Y)) (Opposite.op X)))
          f ≫
        G.map g
[PROOFSTEP]
intros X Y Y' f g
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
h : G.op ⊣ F.op
X : C
Y Y' : D
f : F.obj X ⟶ Y
g : Y ⟶ Y'
⊢ (↑fun {X} {Y} =>
        ((homEquiv h (Opposite.op Y) (Opposite.op X)).trans
                (opEquiv (Opposite.op Y) (F.op.obj (Opposite.op X)))).symm.trans
          (opEquiv (G.op.obj (Opposite.op Y)) (Opposite.op X)))
      (f ≫ g) =
    (↑fun {X} {Y} =>
          ((homEquiv h (Opposite.op Y) (Opposite.op X)).trans
                  (opEquiv (Opposite.op Y) (F.op.obj (Opposite.op X)))).symm.trans
            (opEquiv (G.op.obj (Opposite.op Y)) (Opposite.op X)))
        f ≫
      G.map g
[PROOFSTEP]
dsimp [opEquiv]
  -- Porting note: Why is `erw` needed here?
        -- https://github.com/leanprover-community/mathlib4/issues/5164
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
h : G.op ⊣ F.op
X : C
Y Y' : D
f : F.obj X ⟶ Y
g : Y ⟶ Y'
⊢ (↑(homEquiv h (Opposite.op Y') (Opposite.op X)).symm (g.op ≫ f.op)).unop =
    (↑(homEquiv h (Opposite.op Y) (Opposite.op X)).symm f.op).unop ≫ G.map g
[PROOFSTEP]
erw [homEquiv_counit, homEquiv_counit]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
h : G.op ⊣ F.op
X : C
Y Y' : D
f : F.obj X ⟶ Y
g : Y ⟶ Y'
⊢ (G.op.map (g.op ≫ f.op) ≫ NatTrans.app h.counit (Opposite.op X)).unop =
    (G.op.map f.op ≫ NatTrans.app h.counit (Opposite.op X)).unop ≫ G.map g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
h : G ⊣ F
⊢ ∀ {X' X : Cᵒᵖ} {Y : Dᵒᵖ} (f : X' ⟶ X) (g : X ⟶ G.op.obj Y),
    ↑((fun X Y =>
                (opEquiv (F.op.obj X) Y).trans
                  ((homEquiv h Y.unop X.unop).symm.trans (opEquiv X (Opposite.op (G.toPrefunctor.1 Y.unop))).symm))
              X' Y).symm
        (f ≫ g) =
      F.op.map f ≫
        ↑((fun X Y =>
                  (opEquiv (F.op.obj X) Y).trans
                    ((homEquiv h Y.unop X.unop).symm.trans (opEquiv X (Opposite.op (G.toPrefunctor.1 Y.unop))).symm))
                X Y).symm
          g
[PROOFSTEP]
intros X' X Y f g
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
h : G ⊣ F
X' X : Cᵒᵖ
Y : Dᵒᵖ
f : X' ⟶ X
g : X ⟶ G.op.obj Y
⊢ ↑((fun X Y =>
              (opEquiv (F.op.obj X) Y).trans
                ((homEquiv h Y.unop X.unop).symm.trans (opEquiv X (Opposite.op (G.toPrefunctor.1 Y.unop))).symm))
            X' Y).symm
      (f ≫ g) =
    F.op.map f ≫
      ↑((fun X Y =>
                (opEquiv (F.op.obj X) Y).trans
                  ((homEquiv h Y.unop X.unop).symm.trans (opEquiv X (Opposite.op (G.toPrefunctor.1 Y.unop))).symm))
              X Y).symm
        g
[PROOFSTEP]
dsimp [opEquiv]
  -- Porting note: Why is `erw` needed here?
        -- https://github.com/leanprover-community/mathlib4/issues/5164
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
h : G ⊣ F
X' X : Cᵒᵖ
Y : Dᵒᵖ
f : X' ⟶ X
g : X ⟶ G.op.obj Y
⊢ (↑(homEquiv h Y.unop X'.unop) (g.unop ≫ f.unop)).op = (F.map f.unop).op ≫ (↑(homEquiv h Y.unop X.unop) g.unop).op
[PROOFSTEP]
erw [homEquiv_unit, homEquiv_unit]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
h : G ⊣ F
X' X : Cᵒᵖ
Y : Dᵒᵖ
f : X' ⟶ X
g : X ⟶ G.op.obj Y
⊢ (NatTrans.app h.unit Y.unop ≫ F.map (g.unop ≫ f.unop)).op =
    (F.map f.unop).op ≫ (NatTrans.app h.unit Y.unop ≫ F.map g.unop).op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
h : G ⊣ F
⊢ ∀ {X : Cᵒᵖ} {Y Y' : Dᵒᵖ} (f : F.op.obj X ⟶ Y) (g : Y ⟶ Y'),
    ↑((fun X Y =>
              (opEquiv (F.op.obj X) Y).trans
                ((homEquiv h Y.unop X.unop).symm.trans (opEquiv X (Opposite.op (G.toPrefunctor.1 Y.unop))).symm))
            X Y')
        (f ≫ g) =
      ↑((fun X Y =>
                (opEquiv (F.op.obj X) Y).trans
                  ((homEquiv h Y.unop X.unop).symm.trans (opEquiv X (Opposite.op (G.toPrefunctor.1 Y.unop))).symm))
              X Y)
          f ≫
        G.op.map g
[PROOFSTEP]
intros X' X Y f g
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
h : G ⊣ F
X' : Cᵒᵖ
X Y : Dᵒᵖ
f : F.op.obj X' ⟶ X
g : X ⟶ Y
⊢ ↑((fun X Y =>
            (opEquiv (F.op.obj X) Y).trans
              ((homEquiv h Y.unop X.unop).symm.trans (opEquiv X (Opposite.op (G.toPrefunctor.1 Y.unop))).symm))
          X' Y)
      (f ≫ g) =
    ↑((fun X Y =>
              (opEquiv (F.op.obj X) Y).trans
                ((homEquiv h Y.unop X.unop).symm.trans (opEquiv X (Opposite.op (G.toPrefunctor.1 Y.unop))).symm))
            X' X)
        f ≫
      G.op.map g
[PROOFSTEP]
dsimp [opEquiv]
  -- Porting note: Why is `erw` needed here?
        -- https://github.com/leanprover-community/mathlib4/issues/5164
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
h : G ⊣ F
X' : Cᵒᵖ
X Y : Dᵒᵖ
f : F.op.obj X' ⟶ X
g : X ⟶ Y
⊢ (↑(homEquiv h Y.unop X'.unop).symm (g.unop ≫ f.unop)).op =
    (↑(homEquiv h X.unop X'.unop).symm f.unop).op ≫ (G.map g.unop).op
[PROOFSTEP]
erw [homEquiv_counit, homEquiv_counit]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
h : G ⊣ F
X' : Cᵒᵖ
X Y : Dᵒᵖ
f : F.op.obj X' ⟶ X
g : X ⟶ Y
⊢ (G.map (g.unop ≫ f.unop) ≫ NatTrans.app h.counit X'.unop).op =
    (G.map f.unop ≫ NatTrans.app h.counit X'.unop).op ≫ (G.map g.unop).op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ ↑(homEquiv adj1 x (F'.obj x)) (NatTrans.app (leftAdjointUniq adj1 adj2).hom x) = NatTrans.app adj2.unit x
[PROOFSTEP]
apply (adj1.homEquiv _ _).symm.injective
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ ↑(homEquiv adj1 x (F'.obj x)).symm (↑(homEquiv adj1 x (F'.obj x)) (NatTrans.app (leftAdjointUniq adj1 adj2).hom x)) =
    ↑(homEquiv adj1 x (F'.obj x)).symm (NatTrans.app adj2.unit x)
[PROOFSTEP]
apply Quiver.Hom.op_inj
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ (↑(homEquiv adj1 x (F'.obj x)).symm
        (↑(homEquiv adj1 x (F'.obj x)) (NatTrans.app (leftAdjointUniq adj1 adj2).hom x))).op =
    (↑(homEquiv adj1 x (F'.obj x)).symm (NatTrans.app adj2.unit x)).op
[PROOFSTEP]
apply coyoneda.map_injective
[GOAL]
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ coyoneda.map
      (↑(homEquiv adj1 x (F'.obj x)).symm
          (↑(homEquiv adj1 x (F'.obj x)) (NatTrans.app (leftAdjointUniq adj1 adj2).hom x))).op =
    coyoneda.map (↑(homEquiv adj1 x (F'.obj x)).symm (NatTrans.app adj2.unit x)).op
[PROOFSTEP]
ext
  -- Porting note: Why do I need this with the `ext` from the previous line?
[GOAL]
case a.a.a.w.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
x✝ : D
a✝ : (coyoneda.obj (Opposite.op (F'.obj x))).obj x✝
⊢ NatTrans.app
      (coyoneda.map
        (↑(homEquiv adj1 x (F'.obj x)).symm
            (↑(homEquiv adj1 x (F'.obj x)) (NatTrans.app (leftAdjointUniq adj1 adj2).hom x))).op)
      x✝ a✝ =
    NatTrans.app (coyoneda.map (↑(homEquiv adj1 x (F'.obj x)).symm (NatTrans.app adj2.unit x)).op) x✝ a✝
[PROOFSTEP]
funext
[GOAL]
case a.a.a.w.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
x✝ : D
a✝ : (coyoneda.obj (Opposite.op (F'.obj x))).obj x✝
⊢ NatTrans.app
      (coyoneda.map
        (↑(homEquiv adj1 x (F'.obj x)).symm
            (↑(homEquiv adj1 x (F'.obj x)) (NatTrans.app (leftAdjointUniq adj1 adj2).hom x))).op)
      x✝ a✝ =
    NatTrans.app (coyoneda.map (↑(homEquiv adj1 x (F'.obj x)).symm (NatTrans.app adj2.unit x)).op) x✝ a✝
[PROOFSTEP]
simp [leftAdjointUniq, leftAdjointsCoyonedaEquiv]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
⊢ adj1.unit ≫ whiskerRight (leftAdjointUniq adj1 adj2).hom G = adj2.unit
[PROOFSTEP]
ext x
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ NatTrans.app (adj1.unit ≫ whiskerRight (leftAdjointUniq adj1 adj2).hom G) x = NatTrans.app adj2.unit x
[PROOFSTEP]
rw [NatTrans.comp_app, ← homEquiv_leftAdjointUniq_hom_app adj1 adj2]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ NatTrans.app adj1.unit x ≫ NatTrans.app (whiskerRight (leftAdjointUniq adj1 adj2).hom G) x =
    ↑(homEquiv adj1 x (F'.obj x)) (NatTrans.app (leftAdjointUniq adj1 adj2).hom x)
[PROOFSTEP]
simp [← G.map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ NatTrans.app adj1.unit x ≫ G.map (NatTrans.app (leftAdjointUniq adj1 adj2).hom x) = NatTrans.app adj2.unit x
[PROOFSTEP]
rw [← unit_leftAdjointUniq_hom adj1 adj2]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ NatTrans.app adj1.unit x ≫ G.map (NatTrans.app (leftAdjointUniq adj1 adj2).hom x) =
    NatTrans.app (adj1.unit ≫ whiskerRight (leftAdjointUniq adj1 adj2).hom G) x
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
⊢ whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit = adj1.counit
[PROOFSTEP]
ext x
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ NatTrans.app (whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit) x = NatTrans.app adj1.counit x
[PROOFSTEP]
apply Quiver.Hom.op_inj
[GOAL]
case w.h.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ (NatTrans.app (whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit) x).op = (NatTrans.app adj1.counit x).op
[PROOFSTEP]
apply coyoneda.map_injective
[GOAL]
case w.h.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ coyoneda.map (NatTrans.app (whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit) x).op =
    coyoneda.map (NatTrans.app adj1.counit x).op
[PROOFSTEP]
ext
[GOAL]
case w.h.a.a.w.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x x✝ : D
a✝ : (coyoneda.obj (Opposite.op ((𝟭 D).obj x))).obj x✝
⊢ NatTrans.app (coyoneda.map (NatTrans.app (whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit) x).op) x✝ a✝ =
    NatTrans.app (coyoneda.map (NatTrans.app adj1.counit x).op) x✝ a✝
[PROOFSTEP]
funext
[GOAL]
case w.h.a.a.w.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x x✝ : D
a✝ : (coyoneda.obj (Opposite.op ((𝟭 D).obj x))).obj x✝
⊢ NatTrans.app (coyoneda.map (NatTrans.app (whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit) x).op) x✝ a✝ =
    NatTrans.app (coyoneda.map (NatTrans.app adj1.counit x).op) x✝ a✝
[PROOFSTEP]
simp [leftAdjointUniq, leftAdjointsCoyonedaEquiv]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ NatTrans.app (leftAdjointUniq adj1 adj2).hom (G.obj x) ≫ NatTrans.app adj2.counit x = NatTrans.app adj1.counit x
[PROOFSTEP]
rw [← leftAdjointUniq_hom_counit adj1 adj2]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ NatTrans.app (leftAdjointUniq adj1 adj2).hom (G.obj x) ≫ NatTrans.app adj2.counit x =
    NatTrans.app (whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit) x
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
⊢ (leftAdjointUniq adj1 adj2).hom ≫ (leftAdjointUniq adj2 adj3).hom = (leftAdjointUniq adj1 adj3).hom
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x✝ : C
⊢ NatTrans.app ((leftAdjointUniq adj1 adj2).hom ≫ (leftAdjointUniq adj2 adj3).hom) x✝ =
    NatTrans.app (leftAdjointUniq adj1 adj3).hom x✝
[PROOFSTEP]
apply Quiver.Hom.op_inj
[GOAL]
case w.h.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x✝ : C
⊢ (NatTrans.app ((leftAdjointUniq adj1 adj2).hom ≫ (leftAdjointUniq adj2 adj3).hom) x✝).op =
    (NatTrans.app (leftAdjointUniq adj1 adj3).hom x✝).op
[PROOFSTEP]
apply coyoneda.map_injective
[GOAL]
case w.h.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x✝ : C
⊢ coyoneda.map (NatTrans.app ((leftAdjointUniq adj1 adj2).hom ≫ (leftAdjointUniq adj2 adj3).hom) x✝).op =
    coyoneda.map (NatTrans.app (leftAdjointUniq adj1 adj3).hom x✝).op
[PROOFSTEP]
ext
[GOAL]
case w.h.a.a.w.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x✝¹ : C
x✝ : D
a✝ : (coyoneda.obj (Opposite.op (F''.obj x✝¹))).obj x✝
⊢ NatTrans.app (coyoneda.map (NatTrans.app ((leftAdjointUniq adj1 adj2).hom ≫ (leftAdjointUniq adj2 adj3).hom) x✝¹).op)
      x✝ a✝ =
    NatTrans.app (coyoneda.map (NatTrans.app (leftAdjointUniq adj1 adj3).hom x✝¹).op) x✝ a✝
[PROOFSTEP]
funext
[GOAL]
case w.h.a.a.w.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x✝¹ : C
x✝ : D
a✝ : (coyoneda.obj (Opposite.op (F''.obj x✝¹))).obj x✝
⊢ NatTrans.app (coyoneda.map (NatTrans.app ((leftAdjointUniq adj1 adj2).hom ≫ (leftAdjointUniq adj2 adj3).hom) x✝¹).op)
      x✝ a✝ =
    NatTrans.app (coyoneda.map (NatTrans.app (leftAdjointUniq adj1 adj3).hom x✝¹).op) x✝ a✝
[PROOFSTEP]
simp [leftAdjointsCoyonedaEquiv, leftAdjointUniq]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x : C
⊢ NatTrans.app (leftAdjointUniq adj1 adj2).hom x ≫ NatTrans.app (leftAdjointUniq adj2 adj3).hom x =
    NatTrans.app (leftAdjointUniq adj1 adj3).hom x
[PROOFSTEP]
rw [← leftAdjointUniq_trans adj1 adj2 adj3]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
x : C
⊢ NatTrans.app (leftAdjointUniq adj1 adj2).hom x ≫ NatTrans.app (leftAdjointUniq adj2 adj3).hom x =
    NatTrans.app ((leftAdjointUniq adj1 adj2).hom ≫ (leftAdjointUniq adj2 adj3).hom) x
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
⊢ (leftAdjointUniq adj1 adj1).hom = 𝟙 F
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
x✝ : C
⊢ NatTrans.app (leftAdjointUniq adj1 adj1).hom x✝ = NatTrans.app (𝟙 F) x✝
[PROOFSTEP]
apply Quiver.Hom.op_inj
[GOAL]
case w.h.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
x✝ : C
⊢ (NatTrans.app (leftAdjointUniq adj1 adj1).hom x✝).op = (NatTrans.app (𝟙 F) x✝).op
[PROOFSTEP]
apply coyoneda.map_injective
[GOAL]
case w.h.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
x✝ : C
⊢ coyoneda.map (NatTrans.app (leftAdjointUniq adj1 adj1).hom x✝).op = coyoneda.map (NatTrans.app (𝟙 F) x✝).op
[PROOFSTEP]
ext
[GOAL]
case w.h.a.a.w.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
x✝¹ : C
x✝ : D
a✝ : (coyoneda.obj (Opposite.op (F.obj x✝¹))).obj x✝
⊢ NatTrans.app (coyoneda.map (NatTrans.app (leftAdjointUniq adj1 adj1).hom x✝¹).op) x✝ a✝ =
    NatTrans.app (coyoneda.map (NatTrans.app (𝟙 F) x✝¹).op) x✝ a✝
[PROOFSTEP]
funext
[GOAL]
case w.h.a.a.w.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
x✝¹ : C
x✝ : D
a✝ : (coyoneda.obj (Opposite.op (F.obj x✝¹))).obj x✝
⊢ NatTrans.app (coyoneda.map (NatTrans.app (leftAdjointUniq adj1 adj1).hom x✝¹).op) x✝ a✝ =
    NatTrans.app (coyoneda.map (NatTrans.app (𝟙 F) x✝¹).op) x✝ a✝
[PROOFSTEP]
simp [leftAdjointsCoyonedaEquiv, leftAdjointUniq]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
⊢ ↑(homEquiv adj2 (G.obj x) x).symm (NatTrans.app (rightAdjointUniq adj1 adj2).hom x) = NatTrans.app adj1.counit x
[PROOFSTEP]
apply Quiver.Hom.op_inj
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
⊢ (↑(homEquiv adj2 (G.obj x) x).symm (NatTrans.app (rightAdjointUniq adj1 adj2).hom x)).op =
    (NatTrans.app adj1.counit x).op
[PROOFSTEP]
convert
  homEquiv_leftAdjointUniq_hom_app (opAdjointOpOfAdjoint _ F adj2) (opAdjointOpOfAdjoint _ _ adj1)
    (Opposite.op x)
      -- Porting note: was `simpa`
[GOAL]
case h.e'_3.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
e_1✝ :
  (Opposite.op x ⟶ Opposite.op (F.obj (G.obj x))) =
    (fun x_1 => Opposite.op x ⟶ F.op.obj (G.op.obj (Opposite.op x)))
      (NatTrans.app (leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom
        (Opposite.op x))
⊢ (NatTrans.app adj1.counit x).op = NatTrans.app (opAdjointOpOfAdjoint G F adj1).unit (Opposite.op x)
[PROOFSTEP]
simp only [opAdjointOpOfAdjoint, Functor.op_obj, Opposite.unop_op, mkOfHomEquiv_unit_app, Equiv.trans_apply,
  homEquiv_counit, Functor.id_obj]
  -- Porting note: Yet another `erw`...
    -- https://github.com/leanprover-community/mathlib4/issues/5164
[GOAL]
case h.e'_3.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
e_1✝ :
  (Opposite.op x ⟶ Opposite.op (F.obj (G.obj x))) =
    (fun x_1 => Opposite.op x ⟶ F.op.obj (G.op.obj (Opposite.op x)))
      (NatTrans.app (leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom
        (Opposite.op x))
⊢ (NatTrans.app adj1.counit x).op =
    ↑(opEquiv (Opposite.op x) (Opposite.op (F.toPrefunctor.1 (G.obj x)))).symm
      (F.map (↑(opEquiv (Opposite.op (G.obj x)) (Opposite.op (G.obj x))) (𝟙 (Opposite.op (G.obj x)))) ≫
        NatTrans.app adj1.counit x)
[PROOFSTEP]
erw [F.map_id]
[GOAL]
case h.e'_3.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
e_1✝ :
  (Opposite.op x ⟶ Opposite.op (F.obj (G.obj x))) =
    (fun x_1 => Opposite.op x ⟶ F.op.obj (G.op.obj (Opposite.op x)))
      (NatTrans.app (leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom
        (Opposite.op x))
⊢ (NatTrans.app adj1.counit x).op =
    ↑(opEquiv (Opposite.op x) (Opposite.op (F.toPrefunctor.1 (G.obj x)))).symm
      (𝟙 (F.obj (G.obj x)) ≫ NatTrans.app adj1.counit x)
[PROOFSTEP]
rw [Category.id_comp]
[GOAL]
case h.e'_3.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
e_1✝ :
  (Opposite.op x ⟶ Opposite.op (F.obj (G.obj x))) =
    (fun x_1 => Opposite.op x ⟶ F.op.obj (G.op.obj (Opposite.op x)))
      (NatTrans.app (leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom
        (Opposite.op x))
⊢ (NatTrans.app adj1.counit x).op =
    ↑(opEquiv (Opposite.op x) (Opposite.op (F.toPrefunctor.1 (G.obj x)))).symm (NatTrans.app adj1.counit x)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ NatTrans.app adj1.unit x ≫ NatTrans.app (rightAdjointUniq adj1 adj2).hom (F.obj x) = NatTrans.app adj2.unit x
[PROOFSTEP]
apply Quiver.Hom.op_inj
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ (NatTrans.app adj1.unit x ≫ NatTrans.app (rightAdjointUniq adj1 adj2).hom (F.obj x)).op =
    (NatTrans.app adj2.unit x).op
[PROOFSTEP]
convert
  leftAdjointUniq_hom_app_counit (opAdjointOpOfAdjoint _ _ adj2) (opAdjointOpOfAdjoint _ _ adj1) (Opposite.op x) using 1
  --all_goals simp
[GOAL]
case h.e'_2.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
e_1✝ :
  (Opposite.op (G'.obj (F.obj x)) ⟶ Opposite.op ((𝟭 C).obj x)) =
    (G'.op.obj (F.op.obj (Opposite.op x)) ⟶ (𝟭 Cᵒᵖ).obj (Opposite.op x))
⊢ (NatTrans.app adj1.unit x ≫ NatTrans.app (rightAdjointUniq adj1 adj2).hom (F.obj x)).op =
    NatTrans.app (leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom
        (F.op.obj (Opposite.op x)) ≫
      NatTrans.app (opAdjointOpOfAdjoint G F adj1).counit (Opposite.op x)
case h.e'_3.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
e_1✝ :
  (Opposite.op (G'.obj (F.obj x)) ⟶ Opposite.op ((𝟭 C).obj x)) =
    (G'.op.obj (F.op.obj (Opposite.op x)) ⟶ (𝟭 Cᵒᵖ).obj (Opposite.op x))
⊢ (NatTrans.app adj2.unit x).op = NatTrans.app (opAdjointOpOfAdjoint G' F adj2).counit (Opposite.op x)
[PROOFSTEP]
all_goals {
  -- Porting note: Again, something seems wrong here... Some `simp` lemmas are not firing!
  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
}
[GOAL]
case h.e'_2.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
e_1✝ :
  (Opposite.op (G'.obj (F.obj x)) ⟶ Opposite.op ((𝟭 C).obj x)) =
    (G'.op.obj (F.op.obj (Opposite.op x)) ⟶ (𝟭 Cᵒᵖ).obj (Opposite.op x))
⊢ (NatTrans.app adj1.unit x ≫ NatTrans.app (rightAdjointUniq adj1 adj2).hom (F.obj x)).op =
    NatTrans.app (leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom
        (F.op.obj (Opposite.op x)) ≫
      NatTrans.app (opAdjointOpOfAdjoint G F adj1).counit (Opposite.op x)
[PROOFSTEP]
{
  -- Porting note: Again, something seems wrong here... Some `simp` lemmas are not firing!
  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
}
[GOAL]
case h.e'_2.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
e_1✝ :
  (Opposite.op (G'.obj (F.obj x)) ⟶ Opposite.op ((𝟭 C).obj x)) =
    (G'.op.obj (F.op.obj (Opposite.op x)) ⟶ (𝟭 Cᵒᵖ).obj (Opposite.op x))
⊢ (NatTrans.app adj1.unit x ≫ NatTrans.app (rightAdjointUniq adj1 adj2).hom (F.obj x)).op =
    NatTrans.app (leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom
        (F.op.obj (Opposite.op x)) ≫
      NatTrans.app (opAdjointOpOfAdjoint G F adj1).counit (Opposite.op x)
[PROOFSTEP]
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]
[GOAL]
case h.e'_2.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
e_1✝ :
  (Opposite.op (G'.obj (F.obj x)) ⟶ Opposite.op ((𝟭 C).obj x)) =
    (G'.op.obj (F.op.obj (Opposite.op x)) ⟶ (𝟭 Cᵒᵖ).obj (Opposite.op x))
⊢ (NatTrans.app (rightAdjointUniq adj1 adj2).hom (F.obj x)).op ≫ (NatTrans.app adj1.unit x).op =
    NatTrans.app
        (leftAdjointUniq
            (mkOfHomEquiv
              (CoreHomEquiv.mk fun X Y =>
                (opEquiv (Opposite.op (G'.obj X.unop)) Y).trans
                  ((homEquiv adj2 Y.unop X.unop).symm.trans (opEquiv X (Opposite.op (F.toPrefunctor.1 Y.unop))).symm)))
            (mkOfHomEquiv
              (CoreHomEquiv.mk fun X Y =>
                (opEquiv (Opposite.op (G.obj X.unop)) Y).trans
                  ((homEquiv adj1 Y.unop X.unop).symm.trans
                    (opEquiv X (Opposite.op (F.toPrefunctor.1 Y.unop))).symm)))).hom
        (Opposite.op (F.obj x)) ≫
      ↑(opEquiv (Opposite.op (G.obj (F.obj x))) (Opposite.op x)).symm
        (NatTrans.app adj1.unit x ≫
          G.map (↑(opEquiv (Opposite.op (F.obj x)) (Opposite.op (F.toPrefunctor.1 x))) (𝟙 (Opposite.op (F.obj x)))))
[PROOFSTEP]
erw [Functor.map_id]
[GOAL]
case h.e'_2.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
e_1✝ :
  (Opposite.op (G'.obj (F.obj x)) ⟶ Opposite.op ((𝟭 C).obj x)) =
    (G'.op.obj (F.op.obj (Opposite.op x)) ⟶ (𝟭 Cᵒᵖ).obj (Opposite.op x))
⊢ (NatTrans.app (rightAdjointUniq adj1 adj2).hom (F.obj x)).op ≫ (NatTrans.app adj1.unit x).op =
    NatTrans.app
        (leftAdjointUniq
            (mkOfHomEquiv
              (CoreHomEquiv.mk fun X Y =>
                (opEquiv (Opposite.op (G'.obj X.unop)) Y).trans
                  ((homEquiv adj2 Y.unop X.unop).symm.trans (opEquiv X (Opposite.op (F.toPrefunctor.1 Y.unop))).symm)))
            (mkOfHomEquiv
              (CoreHomEquiv.mk fun X Y =>
                (opEquiv (Opposite.op (G.obj X.unop)) Y).trans
                  ((homEquiv adj1 Y.unop X.unop).symm.trans
                    (opEquiv X (Opposite.op (F.toPrefunctor.1 Y.unop))).symm)))).hom
        (Opposite.op (F.obj x)) ≫
      ↑(opEquiv (Opposite.op (G.obj (F.obj x))) (Opposite.op x)).symm (NatTrans.app adj1.unit x ≫ 𝟙 (G.obj (F.obj x)))
[PROOFSTEP]
rw [Category.comp_id]
[GOAL]
case h.e'_2.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
e_1✝ :
  (Opposite.op (G'.obj (F.obj x)) ⟶ Opposite.op ((𝟭 C).obj x)) =
    (G'.op.obj (F.op.obj (Opposite.op x)) ⟶ (𝟭 Cᵒᵖ).obj (Opposite.op x))
⊢ (NatTrans.app (rightAdjointUniq adj1 adj2).hom (F.obj x)).op ≫ (NatTrans.app adj1.unit x).op =
    NatTrans.app
        (leftAdjointUniq
            (mkOfHomEquiv
              (CoreHomEquiv.mk fun X Y =>
                (opEquiv (Opposite.op (G'.obj X.unop)) Y).trans
                  ((homEquiv adj2 Y.unop X.unop).symm.trans (opEquiv X (Opposite.op (F.toPrefunctor.1 Y.unop))).symm)))
            (mkOfHomEquiv
              (CoreHomEquiv.mk fun X Y =>
                (opEquiv (Opposite.op (G.obj X.unop)) Y).trans
                  ((homEquiv adj1 Y.unop X.unop).symm.trans
                    (opEquiv X (Opposite.op (F.toPrefunctor.1 Y.unop))).symm)))).hom
        (Opposite.op (F.obj x)) ≫
      ↑(opEquiv (Opposite.op (G.obj (F.obj x))) (Opposite.op x)).symm (NatTrans.app adj1.unit x)
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
e_1✝ :
  (Opposite.op (G'.obj (F.obj x)) ⟶ Opposite.op ((𝟭 C).obj x)) =
    (G'.op.obj (F.op.obj (Opposite.op x)) ⟶ (𝟭 Cᵒᵖ).obj (Opposite.op x))
⊢ (NatTrans.app adj2.unit x).op = NatTrans.app (opAdjointOpOfAdjoint G' F adj2).counit (Opposite.op x)
[PROOFSTEP]
{
  -- Porting note: Again, something seems wrong here... Some `simp` lemmas are not firing!
  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
}
[GOAL]
case h.e'_3.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
e_1✝ :
  (Opposite.op (G'.obj (F.obj x)) ⟶ Opposite.op ((𝟭 C).obj x)) =
    (G'.op.obj (F.op.obj (Opposite.op x)) ⟶ (𝟭 Cᵒᵖ).obj (Opposite.op x))
⊢ (NatTrans.app adj2.unit x).op = NatTrans.app (opAdjointOpOfAdjoint G' F adj2).counit (Opposite.op x)
[PROOFSTEP]
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]
[GOAL]
case h.e'_3.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
e_1✝ :
  (Opposite.op (G'.obj (F.obj x)) ⟶ Opposite.op ((𝟭 C).obj x)) =
    (G'.op.obj (F.op.obj (Opposite.op x)) ⟶ (𝟭 Cᵒᵖ).obj (Opposite.op x))
⊢ (NatTrans.app adj2.unit x).op =
    ↑(opEquiv (Opposite.op (G'.obj (F.obj x))) (Opposite.op x)).symm
      (NatTrans.app adj2.unit x ≫
        G'.map (↑(opEquiv (Opposite.op (F.obj x)) (Opposite.op (F.toPrefunctor.1 x))) (𝟙 (Opposite.op (F.obj x)))))
[PROOFSTEP]
erw [Functor.map_id]
[GOAL]
case h.e'_3.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
e_1✝ :
  (Opposite.op (G'.obj (F.obj x)) ⟶ Opposite.op ((𝟭 C).obj x)) =
    (G'.op.obj (F.op.obj (Opposite.op x)) ⟶ (𝟭 Cᵒᵖ).obj (Opposite.op x))
⊢ (NatTrans.app adj2.unit x).op =
    ↑(opEquiv (Opposite.op (G'.obj (F.obj x))) (Opposite.op x)).symm (NatTrans.app adj2.unit x ≫ 𝟙 (G'.obj (F.obj x)))
[PROOFSTEP]
rw [Category.comp_id]
[GOAL]
case h.e'_3.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
e_1✝ :
  (Opposite.op (G'.obj (F.obj x)) ⟶ Opposite.op ((𝟭 C).obj x)) =
    (G'.op.obj (F.op.obj (Opposite.op x)) ⟶ (𝟭 Cᵒᵖ).obj (Opposite.op x))
⊢ (NatTrans.app adj2.unit x).op =
    ↑(opEquiv (Opposite.op (G'.obj (F.obj x))) (Opposite.op x)).symm (NatTrans.app adj2.unit x)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
⊢ adj1.unit ≫ whiskerLeft F (rightAdjointUniq adj1 adj2).hom = adj2.unit
[PROOFSTEP]
ext x
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : C
⊢ NatTrans.app (adj1.unit ≫ whiskerLeft F (rightAdjointUniq adj1 adj2).hom) x = NatTrans.app adj2.unit x
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
⊢ F.map (NatTrans.app (rightAdjointUniq adj1 adj2).hom x) ≫ NatTrans.app adj2.counit x = NatTrans.app adj1.counit x
[PROOFSTEP]
apply Quiver.Hom.op_inj
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
⊢ (F.map (NatTrans.app (rightAdjointUniq adj1 adj2).hom x) ≫ NatTrans.app adj2.counit x).op =
    (NatTrans.app adj1.counit x).op
[PROOFSTEP]
convert
  unit_leftAdjointUniq_hom_app (opAdjointOpOfAdjoint _ _ adj2) (opAdjointOpOfAdjoint _ _ adj1) (Opposite.op x) using 1
[GOAL]
case h.e'_2.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
e_1✝ :
  (Opposite.op ((𝟭 D).obj x) ⟶ Opposite.op (F.obj (G.obj x))) =
    ((𝟭 Dᵒᵖ).obj (Opposite.op x) ⟶ F.op.obj (G.op.obj (Opposite.op x)))
⊢ (F.map (NatTrans.app (rightAdjointUniq adj1 adj2).hom x) ≫ NatTrans.app adj2.counit x).op =
    NatTrans.app (opAdjointOpOfAdjoint G' F adj2).unit (Opposite.op x) ≫
      F.op.map
        (NatTrans.app (leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom
          (Opposite.op x))
[PROOFSTEP]
simp only [Functor.id_obj, op_comp, Functor.comp_obj, Functor.op_obj, Opposite.unop_op, opAdjointOpOfAdjoint_unit_app,
  Functor.op_map]
[GOAL]
case h.e'_2.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
e_1✝ :
  (Opposite.op ((𝟭 D).obj x) ⟶ Opposite.op (F.obj (G.obj x))) =
    ((𝟭 Dᵒᵖ).obj (Opposite.op x) ⟶ F.op.obj (G.op.obj (Opposite.op x)))
⊢ (NatTrans.app adj2.counit x).op ≫ (F.map (NatTrans.app (rightAdjointUniq adj1 adj2).hom x)).op =
    ↑(opEquiv (Opposite.op x) (Opposite.op (F.toPrefunctor.1 (G'.obj x)))).symm
        (F.map (↑(opEquiv (Opposite.op (G'.obj x)) (Opposite.op (G'.obj x))) (𝟙 (Opposite.op (G'.obj x)))) ≫
          NatTrans.app adj2.counit x) ≫
      (F.map
          (NatTrans.app (leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom
              (Opposite.op x)).unop).op
[PROOFSTEP]
dsimp [opEquiv]
[GOAL]
case h.e'_2.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
e_1✝ :
  (Opposite.op ((𝟭 D).obj x) ⟶ Opposite.op (F.obj (G.obj x))) =
    ((𝟭 Dᵒᵖ).obj (Opposite.op x) ⟶ F.op.obj (G.op.obj (Opposite.op x)))
⊢ (NatTrans.app adj2.counit x).op ≫ (F.map (NatTrans.app (rightAdjointUniq adj1 adj2).hom x)).op =
    ((NatTrans.app adj2.counit x).op ≫ (F.map (𝟙 (G'.obj x))).op) ≫
      (F.map
          (NatTrans.app (leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom
              (Opposite.op x)).unop).op
[PROOFSTEP]
simp only [← op_comp]
[GOAL]
case h.e'_2.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
e_1✝ :
  (Opposite.op ((𝟭 D).obj x) ⟶ Opposite.op (F.obj (G.obj x))) =
    ((𝟭 Dᵒᵖ).obj (Opposite.op x) ⟶ F.op.obj (G.op.obj (Opposite.op x)))
⊢ (F.map (NatTrans.app (rightAdjointUniq adj1 adj2).hom x) ≫ NatTrans.app adj2.counit x).op =
    (F.map
          (NatTrans.app (leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom
              (Opposite.op x)).unop ≫
        F.map (𝟙 (G'.obj x)) ≫ NatTrans.app adj2.counit x).op
[PROOFSTEP]
congr 2
[GOAL]
case h.e'_2.h.e_f.e_a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
e_1✝ :
  (Opposite.op ((𝟭 D).obj x) ⟶ Opposite.op (F.obj (G.obj x))) =
    ((𝟭 Dᵒᵖ).obj (Opposite.op x) ⟶ F.op.obj (G.op.obj (Opposite.op x)))
⊢ NatTrans.app adj2.counit x = F.map (𝟙 (G'.obj x)) ≫ NatTrans.app adj2.counit x
[PROOFSTEP]
simp
[GOAL]
case h.e'_3.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
e_1✝ :
  (Opposite.op ((𝟭 D).obj x) ⟶ Opposite.op (F.obj (G.obj x))) =
    ((𝟭 Dᵒᵖ).obj (Opposite.op x) ⟶ F.op.obj (G.op.obj (Opposite.op x)))
⊢ (NatTrans.app adj1.counit x).op = NatTrans.app (opAdjointOpOfAdjoint G F adj1).unit (Opposite.op x)
[PROOFSTEP]
simp only [Functor.id_obj, opAdjointOpOfAdjoint_unit_app, Opposite.unop_op]
[GOAL]
case h.e'_3.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
e_1✝ :
  (Opposite.op ((𝟭 D).obj x) ⟶ Opposite.op (F.obj (G.obj x))) =
    ((𝟭 Dᵒᵖ).obj (Opposite.op x) ⟶ F.op.obj (G.op.obj (Opposite.op x)))
⊢ (NatTrans.app adj1.counit x).op =
    ↑(opEquiv (Opposite.op x) (Opposite.op (F.toPrefunctor.1 (G.obj x)))).symm
      (F.map (↑(opEquiv (Opposite.op (G.obj x)) (Opposite.op (G.obj x))) (𝟙 (Opposite.op (G.obj x)))) ≫
        NatTrans.app adj1.counit x)
[PROOFSTEP]
erw [Functor.map_id, Category.id_comp]
[GOAL]
case h.e'_3.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x : D
e_1✝ :
  (Opposite.op ((𝟭 D).obj x) ⟶ Opposite.op (F.obj (G.obj x))) =
    ((𝟭 Dᵒᵖ).obj (Opposite.op x) ⟶ F.op.obj (G.op.obj (Opposite.op x)))
⊢ (NatTrans.app adj1.counit x).op =
    ↑(opEquiv (Opposite.op x) (Opposite.op (F.toPrefunctor.1 (G.obj x)))).symm (NatTrans.app adj1.counit x)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
⊢ whiskerRight (rightAdjointUniq adj1 adj2).hom F ≫ adj2.counit = adj1.counit
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
x✝ : D
⊢ NatTrans.app (whiskerRight (rightAdjointUniq adj1 adj2).hom F ≫ adj2.counit) x✝ = NatTrans.app adj1.counit x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ NatTrans.app (rightAdjointUniq adj1 adj2).hom x ≫ NatTrans.app (rightAdjointUniq adj2 adj3).hom x =
    NatTrans.app (rightAdjointUniq adj1 adj3).hom x
[PROOFSTEP]
apply Quiver.Hom.op_inj
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ (NatTrans.app (rightAdjointUniq adj1 adj2).hom x ≫ NatTrans.app (rightAdjointUniq adj2 adj3).hom x).op =
    (NatTrans.app (rightAdjointUniq adj1 adj3).hom x).op
[PROOFSTEP]
dsimp [rightAdjointUniq]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ NatTrans.app (leftAdjointUniq (opAdjointOpOfAdjoint G'' F adj3) (opAdjointOpOfAdjoint G' F adj2)).hom
        (Opposite.op x) ≫
      NatTrans.app (leftAdjointUniq (opAdjointOpOfAdjoint G' F adj2) (opAdjointOpOfAdjoint G F adj1)).hom
        (Opposite.op x) =
    NatTrans.app (leftAdjointUniq (opAdjointOpOfAdjoint G'' F adj3) (opAdjointOpOfAdjoint G F adj1)).hom (Opposite.op x)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
⊢ (rightAdjointUniq adj1 adj2).hom ≫ (rightAdjointUniq adj2 adj3).hom = (rightAdjointUniq adj1 adj3).hom
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x✝ : D
⊢ NatTrans.app ((rightAdjointUniq adj1 adj2).hom ≫ (rightAdjointUniq adj2 adj3).hom) x✝ =
    NatTrans.app (rightAdjointUniq adj1 adj3).hom x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
⊢ (rightAdjointUniq adj1 adj1).hom = 𝟙 G
[PROOFSTEP]
delta rightAdjointUniq
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
⊢ (NatIso.removeOp (leftAdjointUniq (opAdjointOpOfAdjoint G F adj1) (opAdjointOpOfAdjoint G F adj1))).hom = 𝟙 G
[PROOFSTEP]
simp
