[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


[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X Y : D
f : X ⟶ Y
⊢ (R₁ ⋙ G).map f ≫
      (fun X =>
          NatTrans.app adj₂.unit (G.obj (R₁.obj X)) ≫
            R₂.map (NatTrans.app h (R₁.obj X) ≫ H.map (NatTrans.app adj₁.counit X)))
        Y =
    (fun X =>
          NatTrans.app adj₂.unit (G.obj (R₁.obj X)) ≫
            R₂.map (NatTrans.app h (R₁.obj X) ≫ H.map (NatTrans.app adj₁.counit X)))
        X ≫
      (H ⋙ R₂).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X Y : D
f : X ⟶ Y
⊢ G.map (R₁.map f) ≫
      NatTrans.app adj₂.unit (G.obj (R₁.obj Y)) ≫
        R₂.map (NatTrans.app h (R₁.obj Y) ≫ H.map (NatTrans.app adj₁.counit Y)) =
    (NatTrans.app adj₂.unit (G.obj (R₁.obj X)) ≫
        R₂.map (NatTrans.app h (R₁.obj X) ≫ H.map (NatTrans.app adj₁.counit X))) ≫
      R₂.map (H.map f)
[PROOFSTEP]
rw [assoc, ← R₂.map_comp, assoc, ← H.map_comp, ← adj₁.counit_naturality, H.map_comp, ← Functor.comp_map L₁, ←
  h.naturality_assoc]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X Y : D
f : X ⟶ Y
⊢ G.map (R₁.map f) ≫
      NatTrans.app adj₂.unit (G.obj (R₁.obj Y)) ≫
        R₂.map (NatTrans.app h (R₁.obj Y) ≫ H.map (NatTrans.app adj₁.counit Y)) =
    NatTrans.app adj₂.unit (G.obj (R₁.obj X)) ≫
      R₂.map ((G ⋙ L₂).map (R₁.map f) ≫ NatTrans.app h (R₁.obj Y) ≫ H.map (NatTrans.app adj₁.counit Y))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : R₁ ⋙ G ⟶ H ⋙ R₂
X Y : C
f : X ⟶ Y
⊢ (G ⋙ L₂).map f ≫
      (fun X =>
          L₂.map (G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app h (L₁.obj X)) ≫
            NatTrans.app adj₂.counit (H.obj (L₁.obj X)))
        Y =
    (fun X =>
          L₂.map (G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app h (L₁.obj X)) ≫
            NatTrans.app adj₂.counit (H.obj (L₁.obj X)))
        X ≫
      (L₁ ⋙ H).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : R₁ ⋙ G ⟶ H ⋙ R₂
X Y : C
f : X ⟶ Y
⊢ L₂.map (G.map f) ≫
      L₂.map (G.map (NatTrans.app adj₁.unit Y) ≫ NatTrans.app h (L₁.obj Y)) ≫
        NatTrans.app adj₂.counit (H.obj (L₁.obj Y)) =
    (L₂.map (G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app h (L₁.obj X)) ≫
        NatTrans.app adj₂.counit (H.obj (L₁.obj X))) ≫
      H.map (L₁.map f)
[PROOFSTEP]
rw [← L₂.map_comp_assoc, ← G.map_comp_assoc, ← adj₁.unit_naturality, G.map_comp_assoc, ← Functor.comp_map, h.naturality]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : R₁ ⋙ G ⟶ H ⋙ R₂
X Y : C
f : X ⟶ Y
⊢ L₂.map (G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app h (L₁.obj X) ≫ (H ⋙ R₂).map (L₁.map f)) ≫
      NatTrans.app adj₂.counit (H.obj (L₁.obj Y)) =
    (L₂.map (G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app h (L₁.obj X)) ≫
        NatTrans.app adj₂.counit (H.obj (L₁.obj X))) ≫
      H.map (L₁.map f)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
⊢ (fun h =>
        NatTrans.mk fun X =>
          L₂.map (G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app h (L₁.obj X)) ≫
            NatTrans.app adj₂.counit (H.obj (L₁.obj X)))
      ((fun h =>
          NatTrans.mk fun X =>
            NatTrans.app adj₂.unit (G.obj (R₁.obj X)) ≫
              R₂.map (NatTrans.app h (R₁.obj X) ≫ H.map (NatTrans.app adj₁.counit X)))
        h) =
    h
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ NatTrans.app
      ((fun h =>
          NatTrans.mk fun X =>
            L₂.map (G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app h (L₁.obj X)) ≫
              NatTrans.app adj₂.counit (H.obj (L₁.obj X)))
        ((fun h =>
            NatTrans.mk fun X =>
              NatTrans.app adj₂.unit (G.obj (R₁.obj X)) ≫
                R₂.map (NatTrans.app h (R₁.obj X) ≫ H.map (NatTrans.app adj₁.counit X)))
          h))
      X =
    NatTrans.app h X
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ L₂.map
        (G.map (NatTrans.app adj₁.unit X) ≫
          NatTrans.app adj₂.unit (G.obj (R₁.obj (L₁.obj X))) ≫
            R₂.map (NatTrans.app h (R₁.obj (L₁.obj X)) ≫ H.map (NatTrans.app adj₁.counit (L₁.obj X)))) ≫
      NatTrans.app adj₂.counit (H.obj (L₁.obj X)) =
    NatTrans.app h X
[PROOFSTEP]
simp only [L₂.map_comp, assoc, adj₂.counit_naturality, adj₂.left_triangle_components_assoc, ← Functor.comp_map G L₂,
  h.naturality_assoc, Functor.comp_map L₁, ← H.map_comp, adj₁.left_triangle_components]
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ NatTrans.app h X ≫ H.map (𝟙 (L₁.obj X)) = NatTrans.app h X
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ NatTrans.app h X ≫ H.map (𝟙 (L₁.obj X)) = NatTrans.app h X
[PROOFSTEP]
simp only [id_comp, ← Functor.comp_map, ← Functor.comp_obj, NatTrans.naturality_assoc]
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ NatTrans.app h X ≫ H.map (𝟙 (L₁.obj X)) = NatTrans.app h X
[PROOFSTEP]
simp only [Functor.comp_obj, Functor.comp_map, ← Functor.map_comp]
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ NatTrans.app h X ≫ H.map (𝟙 (L₁.obj X)) = NatTrans.app h X
[PROOFSTEP]
have :
  Prefunctor.map L₁.toPrefunctor (NatTrans.app adj₁.unit X) ≫
      NatTrans.app adj₁.counit (Prefunctor.obj L₁.toPrefunctor X) =
    𝟙 _ :=
  by simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ L₁.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app adj₁.counit (L₁.obj X) = 𝟙 (L₁.obj ((𝟭 C).obj X))
[PROOFSTEP]
simp
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
this : L₁.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app adj₁.counit (L₁.obj X) = 𝟙 (L₁.obj ((𝟭 C).obj X))
⊢ NatTrans.app h X ≫ H.map (𝟙 (L₁.obj X)) = NatTrans.app h X
[PROOFSTEP]
simp [this]
  -- See library note [dsimp, simp].
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : R₁ ⋙ G ⟶ H ⋙ R₂
⊢ (fun h =>
        NatTrans.mk fun X =>
          NatTrans.app adj₂.unit (G.obj (R₁.obj X)) ≫
            R₂.map (NatTrans.app h (R₁.obj X) ≫ H.map (NatTrans.app adj₁.counit X)))
      ((fun h =>
          NatTrans.mk fun X =>
            L₂.map (G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app h (L₁.obj X)) ≫
              NatTrans.app adj₂.counit (H.obj (L₁.obj X)))
        h) =
    h
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : R₁ ⋙ G ⟶ H ⋙ R₂
X : D
⊢ NatTrans.app
      ((fun h =>
          NatTrans.mk fun X =>
            NatTrans.app adj₂.unit (G.obj (R₁.obj X)) ≫
              R₂.map (NatTrans.app h (R₁.obj X) ≫ H.map (NatTrans.app adj₁.counit X)))
        ((fun h =>
            NatTrans.mk fun X =>
              L₂.map (G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app h (L₁.obj X)) ≫
                NatTrans.app adj₂.counit (H.obj (L₁.obj X)))
          h))
      X =
    NatTrans.app h X
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : R₁ ⋙ G ⟶ H ⋙ R₂
X : D
⊢ NatTrans.app adj₂.unit (G.obj (R₁.obj X)) ≫
      R₂.map
        ((L₂.map (G.map (NatTrans.app adj₁.unit (R₁.obj X)) ≫ NatTrans.app h (L₁.obj (R₁.obj X))) ≫
            NatTrans.app adj₂.counit (H.obj (L₁.obj (R₁.obj X)))) ≫
          H.map (NatTrans.app adj₁.counit X)) =
    NatTrans.app h X
[PROOFSTEP]
simp [-Functor.comp_map, ← Functor.comp_map H, Functor.comp_map R₁, -NatTrans.naturality, ← h.naturality,
  -Functor.map_comp, ← Functor.map_comp_assoc G, R₂.map_comp]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ⋙ L₂ ⟶ L₁ ⋙ H
Y : D
⊢ L₂.map (NatTrans.app (↑(transferNatTrans adj₁ adj₂) f) Y) ≫ NatTrans.app adj₂.counit (H.obj Y) =
    NatTrans.app f (R₁.obj Y) ≫ H.map (NatTrans.app adj₁.counit Y)
[PROOFSTEP]
erw [Functor.map_comp]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ⋙ L₂ ⟶ L₁ ⋙ H
Y : D
⊢ (L₂.map (NatTrans.app adj₂.unit (G.obj (R₁.obj Y))) ≫
        L₂.map (R₂.map (NatTrans.app f (R₁.obj Y) ≫ H.map (NatTrans.app adj₁.counit Y)))) ≫
      NatTrans.app adj₂.counit (H.obj Y) =
    NatTrans.app f (R₁.obj Y) ≫ H.map (NatTrans.app adj₁.counit Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app (↑(transferNatTrans adj₁ adj₂) f) (L₁.obj X) =
    NatTrans.app adj₂.unit (G.obj ((𝟭 C).obj X)) ≫ R₂.map (NatTrans.app f ((𝟭 C).obj X))
[PROOFSTEP]
dsimp [transferNatTrans]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ G.map (NatTrans.app adj₁.unit X) ≫
      NatTrans.app adj₂.unit (G.obj (R₁.obj (L₁.obj X))) ≫
        R₂.map (NatTrans.app f (R₁.obj (L₁.obj X)) ≫ H.map (NatTrans.app adj₁.counit (L₁.obj X))) =
    NatTrans.app adj₂.unit (G.obj X) ≫ R₂.map (NatTrans.app f X)
[PROOFSTEP]
rw [← adj₂.unit_naturality_assoc, ← R₂.map_comp, ← Functor.comp_map G L₂, f.naturality_assoc, Functor.comp_map, ←
  H.map_comp]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ NatTrans.app adj₂.unit (G.obj X) ≫
      R₂.map (NatTrans.app f X ≫ H.map (L₁.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app adj₁.counit (L₁.obj X))) =
    NatTrans.app adj₂.unit (G.obj X) ≫ R₂.map (NatTrans.app f X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ NatTrans.app adj₂.unit (G.obj X) ≫
      R₂.map (NatTrans.app f X ≫ H.map (L₁.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app adj₁.counit (L₁.obj X))) =
    NatTrans.app adj₂.unit (G.obj X) ≫ R₂.map (NatTrans.app f X)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
⊢ L₂.map (NatTrans.app (↑(transferNatTransSelf adj₁ adj₂) f) X) ≫ NatTrans.app adj₂.counit X =
    NatTrans.app f (R₁.obj X) ≫ NatTrans.app adj₁.counit X
[PROOFSTEP]
dsimp [transferNatTransSelf]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
⊢ L₂.map
        (𝟙 (R₁.obj X) ≫
          NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
              X ≫
            𝟙 (R₂.obj X)) ≫
      NatTrans.app adj₂.counit X =
    NatTrans.app f (R₁.obj X) ≫ NatTrans.app adj₁.counit X
[PROOFSTEP]
rw [id_comp, comp_id]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
⊢ L₂.map
        (NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
          X) ≫
      NatTrans.app adj₂.counit X =
    NatTrans.app f (R₁.obj X) ≫ NatTrans.app adj₁.counit X
[PROOFSTEP]
have := transferNatTrans_counit adj₁ adj₂ (L₂.leftUnitor.hom ≫ f ≫ L₁.rightUnitor.inv) X
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
this :
  L₂.map
        (NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
          X) ≫
      NatTrans.app adj₂.counit ((𝟭 D).obj X) =
    NatTrans.app ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv) (R₁.obj X) ≫
      (𝟭 D).map (NatTrans.app adj₁.counit X)
⊢ L₂.map
        (NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
          X) ≫
      NatTrans.app adj₂.counit X =
    NatTrans.app f (R₁.obj X) ≫ NatTrans.app adj₁.counit X
[PROOFSTEP]
dsimp at this
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
this :
  L₂.map
        (NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
          X) ≫
      NatTrans.app adj₂.counit X =
    (𝟙 (L₂.obj (R₁.obj X)) ≫ NatTrans.app f (R₁.obj X) ≫ 𝟙 (L₁.obj (R₁.obj X))) ≫ NatTrans.app adj₁.counit X
⊢ L₂.map
        (NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
          X) ≫
      NatTrans.app adj₂.counit X =
    NatTrans.app f (R₁.obj X) ≫ NatTrans.app adj₁.counit X
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
this :
  L₂.map
        (NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
          X) ≫
      NatTrans.app adj₂.counit X =
    (𝟙 (L₂.obj (R₁.obj X)) ≫ NatTrans.app f (R₁.obj X) ≫ 𝟙 (L₁.obj (R₁.obj X))) ≫ NatTrans.app adj₁.counit X
⊢ (𝟙 (L₂.obj (R₁.obj X)) ≫ NatTrans.app f (R₁.obj X) ≫ 𝟙 (L₁.obj (R₁.obj X))) ≫ NatTrans.app adj₁.counit X =
    NatTrans.app f (R₁.obj X) ≫ NatTrans.app adj₁.counit X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : C
⊢ NatTrans.app adj₁.unit X ≫ NatTrans.app (↑(transferNatTransSelf adj₁ adj₂) f) (L₁.obj X) =
    NatTrans.app adj₂.unit X ≫ R₂.map (NatTrans.app f X)
[PROOFSTEP]
dsimp [transferNatTransSelf]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : C
⊢ NatTrans.app adj₁.unit X ≫
      𝟙 (R₁.obj (L₁.obj X)) ≫
        NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
            (L₁.obj X) ≫
          𝟙 (R₂.obj (L₁.obj X)) =
    NatTrans.app adj₂.unit X ≫ R₂.map (NatTrans.app f X)
[PROOFSTEP]
rw [id_comp, comp_id]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : C
⊢ NatTrans.app adj₁.unit X ≫
      NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
        (L₁.obj X) =
    NatTrans.app adj₂.unit X ≫ R₂.map (NatTrans.app f X)
[PROOFSTEP]
have := unit_transferNatTrans adj₁ adj₂ (L₂.leftUnitor.hom ≫ f ≫ L₁.rightUnitor.inv) X
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : C
this :
  (𝟭 C).map (NatTrans.app adj₁.unit X) ≫
      NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
        (L₁.obj X) =
    NatTrans.app adj₂.unit ((𝟭 C).obj ((𝟭 C).obj X)) ≫
      R₂.map (NatTrans.app ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv) ((𝟭 C).obj X))
⊢ NatTrans.app adj₁.unit X ≫
      NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
        (L₁.obj X) =
    NatTrans.app adj₂.unit X ≫ R₂.map (NatTrans.app f X)
[PROOFSTEP]
dsimp at this
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : C
this :
  NatTrans.app adj₁.unit X ≫
      NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
        (L₁.obj X) =
    NatTrans.app adj₂.unit X ≫ R₂.map (𝟙 (L₂.obj X) ≫ NatTrans.app f X ≫ 𝟙 (L₁.obj X))
⊢ NatTrans.app adj₁.unit X ≫
      NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
        (L₁.obj X) =
    NatTrans.app adj₂.unit X ≫ R₂.map (NatTrans.app f X)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : C
this :
  NatTrans.app adj₁.unit X ≫
      NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
        (L₁.obj X) =
    NatTrans.app adj₂.unit X ≫ R₂.map (𝟙 (L₂.obj X) ≫ NatTrans.app f X ≫ 𝟙 (L₁.obj X))
⊢ NatTrans.app adj₂.unit X ≫ R₂.map (𝟙 (L₂.obj X) ≫ NatTrans.app f X ≫ 𝟙 (L₁.obj X)) =
    NatTrans.app adj₂.unit X ≫ R₂.map (NatTrans.app f X)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
⊢ ↑(transferNatTransSelf adj₁ adj₁) (𝟙 L₁) = 𝟙 R₁
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
x✝ : D
⊢ NatTrans.app (↑(transferNatTransSelf adj₁ adj₁) (𝟙 L₁)) x✝ = NatTrans.app (𝟙 R₁) x✝
[PROOFSTEP]
dsimp [transferNatTransSelf, transferNatTrans]
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
x✝ : D
⊢ 𝟙 (R₁.obj x✝) ≫
      (NatTrans.app adj₁.unit (R₁.obj x✝) ≫
          R₁.map
            ((𝟙 (L₁.obj (R₁.obj x✝)) ≫ 𝟙 (L₁.obj (R₁.obj x✝)) ≫ 𝟙 (L₁.obj (R₁.obj x✝))) ≫
              NatTrans.app adj₁.counit x✝)) ≫
        𝟙 (R₁.obj x✝) =
    𝟙 (R₁.obj x✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
⊢ ↑(transferNatTransSelf adj₁ adj₁).symm (𝟙 R₁) = 𝟙 L₁
[PROOFSTEP]
rw [Equiv.symm_apply_eq]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
⊢ 𝟙 R₁ = ↑(transferNatTransSelf adj₁ adj₁) (𝟙 L₁)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
g : L₃ ⟶ L₂
⊢ ↑(transferNatTransSelf adj₁ adj₂) f ≫ ↑(transferNatTransSelf adj₂ adj₃) g = ↑(transferNatTransSelf adj₁ adj₃) (g ≫ f)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
g : L₃ ⟶ L₂
x✝ : D
⊢ NatTrans.app (↑(transferNatTransSelf adj₁ adj₂) f ≫ ↑(transferNatTransSelf adj₂ adj₃) g) x✝ =
    NatTrans.app (↑(transferNatTransSelf adj₁ adj₃) (g ≫ f)) x✝
[PROOFSTEP]
dsimp [transferNatTransSelf, transferNatTrans]
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
g : L₃ ⟶ L₂
x✝ : D
⊢ (𝟙 (R₁.obj x✝) ≫
        (NatTrans.app adj₂.unit (R₁.obj x✝) ≫
            R₂.map
              ((𝟙 (L₂.obj (R₁.obj x✝)) ≫ NatTrans.app f (R₁.obj x✝) ≫ 𝟙 (L₁.obj (R₁.obj x✝))) ≫
                NatTrans.app adj₁.counit x✝)) ≫
          𝟙 (R₂.obj x✝)) ≫
      𝟙 (R₂.obj x✝) ≫
        (NatTrans.app adj₃.unit (R₂.obj x✝) ≫
            R₃.map
              ((𝟙 (L₃.obj (R₂.obj x✝)) ≫ NatTrans.app g (R₂.obj x✝) ≫ 𝟙 (L₂.obj (R₂.obj x✝))) ≫
                NatTrans.app adj₂.counit x✝)) ≫
          𝟙 (R₃.obj x✝) =
    𝟙 (R₁.obj x✝) ≫
      (NatTrans.app adj₃.unit (R₁.obj x✝) ≫
          R₃.map
            ((𝟙 (L₃.obj (R₁.obj x✝)) ≫
                (NatTrans.app g (R₁.obj x✝) ≫ NatTrans.app f (R₁.obj x✝)) ≫ 𝟙 (L₁.obj (R₁.obj x✝))) ≫
              NatTrans.app adj₁.counit x✝)) ≫
        𝟙 (R₃.obj x✝)
[PROOFSTEP]
simp only [id_comp, comp_id]
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
g : L₃ ⟶ L₂
x✝ : D
⊢ (NatTrans.app adj₂.unit (R₁.obj x✝) ≫ R₂.map (NatTrans.app f (R₁.obj x✝) ≫ NatTrans.app adj₁.counit x✝)) ≫
      NatTrans.app adj₃.unit (R₂.obj x✝) ≫ R₃.map (NatTrans.app g (R₂.obj x✝) ≫ NatTrans.app adj₂.counit x✝) =
    NatTrans.app adj₃.unit (R₁.obj x✝) ≫
      R₃.map ((NatTrans.app g (R₁.obj x✝) ≫ NatTrans.app f (R₁.obj x✝)) ≫ NatTrans.app adj₁.counit x✝)
[PROOFSTEP]
rw [← adj₃.unit_naturality_assoc, ← R₃.map_comp, g.naturality_assoc, L₂.map_comp, assoc, adj₂.counit_naturality,
  adj₂.left_triangle_components_assoc, assoc]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
L R : C ⥤ C
adj : L ⊣ R
f : 𝟭 C ⟶ L
X : C
⊢ NatTrans.app (↑(transferNatTransSelf adj Adjunction.id) f) X = NatTrans.app f (R.obj X) ≫ NatTrans.app adj.counit X
[PROOFSTEP]
dsimp [transferNatTransSelf, transferNatTrans, Adjunction.id]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
L R : C ⥤ C
adj : L ⊣ R
f : 𝟭 C ⟶ L
X : C
⊢ 𝟙 (R.obj X) ≫
      (𝟙 (R.obj X) ≫ (𝟙 (R.obj X) ≫ NatTrans.app f (R.obj X) ≫ 𝟙 (L.obj (R.obj X))) ≫ NatTrans.app adj.counit X) ≫ 𝟙 X =
    NatTrans.app f (R.obj X) ≫ NatTrans.app adj.counit X
[PROOFSTEP]
simp only [comp_id, id_comp]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
L R : C ⥤ C
adj : L ⊣ R
g : R ⟶ 𝟭 C
X : C
⊢ NatTrans.app (↑(transferNatTransSelf adj Adjunction.id).symm g) X = NatTrans.app adj.unit X ≫ NatTrans.app g (L.obj X)
[PROOFSTEP]
dsimp [transferNatTransSelf, transferNatTrans, Adjunction.id]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
L R : C ⥤ C
adj : L ⊣ R
g : R ⟶ 𝟭 C
X : C
⊢ 𝟙 X ≫
      ((NatTrans.app adj.unit X ≫ 𝟙 (R.obj (L.obj X)) ≫ NatTrans.app g (L.obj X) ≫ 𝟙 (L.obj X)) ≫ 𝟙 (L.obj X)) ≫
        𝟙 (L.obj X) =
    NatTrans.app adj.unit X ≫ NatTrans.app g (L.obj X)
[PROOFSTEP]
simp only [comp_id, id_comp]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₂ ⟶ R₁
g : R₃ ⟶ R₂
⊢ ↑(transferNatTransSelf adj₂ adj₁).symm f ≫ ↑(transferNatTransSelf adj₃ adj₂).symm g =
    ↑(transferNatTransSelf adj₃ adj₁).symm (g ≫ f)
[PROOFSTEP]
rw [Equiv.eq_symm_apply, ← transferNatTransSelf_comp _ adj₂]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₂ ⟶ R₁
g : R₃ ⟶ R₂
⊢ ↑(transferNatTransSelf adj₃ adj₂) (↑(transferNatTransSelf adj₃ adj₂).symm g) ≫
      ↑(transferNatTransSelf adj₂ adj₁) (↑(transferNatTransSelf adj₂ adj₁).symm f) =
    g ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
g : L₁ ⟶ L₂
gf : g ≫ f = 𝟙 L₁
⊢ ↑(transferNatTransSelf adj₁ adj₂) f ≫ ↑(transferNatTransSelf adj₂ adj₁) g = 𝟙 R₁
[PROOFSTEP]
rw [transferNatTransSelf_comp, gf, transferNatTransSelf_id]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₁ ⟶ R₂
g : R₂ ⟶ R₁
gf : g ≫ f = 𝟙 R₂
⊢ ↑(transferNatTransSelf adj₁ adj₂).symm f ≫ ↑(transferNatTransSelf adj₂ adj₁).symm g = 𝟙 L₂
[PROOFSTEP]
rw [transferNatTransSelf_symm_comp, gf, transferNatTransSelf_symm_id]
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
inst✝ : IsIso f
⊢ inv f ≫ f = 𝟙 L₁
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
inst✝ : IsIso f
⊢ f ≫ inv f = 𝟙 L₂
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₁ ⟶ R₂
inst✝ : IsIso f
⊢ inv f ≫ f = 𝟙 R₂
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₁ ⟶ R₂
inst✝ : IsIso f
⊢ f ≫ inv f = 𝟙 R₁
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
inst✝ : IsIso (↑(transferNatTransSelf adj₁ adj₂) f)
⊢ IsIso f
[PROOFSTEP]
suffices IsIso ((transferNatTransSelf adj₁ adj₂).symm (transferNatTransSelf adj₁ adj₂ f)) by simpa using this
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
inst✝ : IsIso (↑(transferNatTransSelf adj₁ adj₂) f)
this : IsIso (↑(transferNatTransSelf adj₁ adj₂).symm (↑(transferNatTransSelf adj₁ adj₂) f))
⊢ IsIso f
[PROOFSTEP]
simpa using this
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
inst✝ : IsIso (↑(transferNatTransSelf adj₁ adj₂) f)
⊢ IsIso (↑(transferNatTransSelf adj₁ adj₂).symm (↑(transferNatTransSelf adj₁ adj₂) f))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₁ ⟶ R₂
inst✝ : IsIso (↑(transferNatTransSelf adj₁ adj₂).symm f)
⊢ IsIso f
[PROOFSTEP]
suffices IsIso ((transferNatTransSelf adj₁ adj₂) ((transferNatTransSelf adj₁ adj₂).symm f)) by simpa using this
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₁ ⟶ R₂
inst✝ : IsIso (↑(transferNatTransSelf adj₁ adj₂).symm f)
this : IsIso (↑(transferNatTransSelf adj₁ adj₂) (↑(transferNatTransSelf adj₁ adj₂).symm f))
⊢ IsIso f
[PROOFSTEP]
simpa using this
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₁ ⟶ R₂
inst✝ : IsIso (↑(transferNatTransSelf adj₁ adj₂).symm f)
⊢ IsIso (↑(transferNatTransSelf adj₁ adj₂) (↑(transferNatTransSelf adj₁ adj₂).symm f))
[PROOFSTEP]
infer_instance