[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ ∀ ⦃X Y : C ⥤ D⦄ (f : X ⟶ Y),
    (𝟭 (C ⥤ D)).map f ≫
        (fun X =>
            (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv)
          Y =
      (fun X => (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv)
          X ≫
        ((whiskeringRight C D E).obj F ⋙ (whiskeringRight C E D).obj G).map f
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : C ⥤ D
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 (C ⥤ D)).map f✝ ≫
      (fun X => (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv)
        Y✝ =
    (fun X => (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv)
        X✝ ≫
      ((whiskeringRight C D E).obj F ⋙ (whiskeringRight C E D).obj G).map f✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : C ⥤ D
f✝ : X✝ ⟶ Y✝
x✝ : C
⊢ NatTrans.app
      ((𝟭 (C ⥤ D)).map f✝ ≫
        (fun X =>
            (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv)
          Y✝)
      x✝ =
    NatTrans.app
      ((fun X =>
            (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv)
          X✝ ≫
        ((whiskeringRight C D E).obj F ⋙ (whiskeringRight C E D).obj G).map f✝)
      x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : C ⥤ D
f✝ : X✝ ⟶ Y✝
x✝ : C
⊢ NatTrans.app f✝ x✝ ≫ 𝟙 (Y✝.obj x✝) ≫ NatTrans.app adj.unit (Y✝.obj x✝) ≫ 𝟙 (G.obj (F.obj (Y✝.obj x✝))) =
    (𝟙 (X✝.obj x✝) ≫ NatTrans.app adj.unit (X✝.obj x✝) ≫ 𝟙 (G.obj (F.obj (X✝.obj x✝)))) ≫
      G.map (F.map (NatTrans.app f✝ x✝))
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ ∀ ⦃X Y : C ⥤ E⦄ (f : X ⟶ Y),
    ((whiskeringRight C E D).obj G ⋙ (whiskeringRight C D E).obj F).map f ≫
        (fun X => (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom) Y =
      (fun X => (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom) X ≫
        (𝟭 (C ⥤ E)).map f
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : C ⥤ E
f✝ : X✝ ⟶ Y✝
⊢ ((whiskeringRight C E D).obj G ⋙ (whiskeringRight C D E).obj F).map f✝ ≫
      (fun X => (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom) Y✝ =
    (fun X => (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom) X✝ ≫
      (𝟭 (C ⥤ E)).map f✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : C ⥤ E
f✝ : X✝ ⟶ Y✝
x✝ : C
⊢ NatTrans.app
      (((whiskeringRight C E D).obj G ⋙ (whiskeringRight C D E).obj F).map f✝ ≫
        (fun X => (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom) Y✝)
      x✝ =
    NatTrans.app
      ((fun X => (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom) X✝ ≫
        (𝟭 (C ⥤ E)).map f✝)
      x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : C ⥤ E
f✝ : X✝ ⟶ Y✝
x✝ : C
⊢ F.map (G.map (NatTrans.app f✝ x✝)) ≫
      𝟙 (F.obj (G.obj (Y✝.obj x✝))) ≫ NatTrans.app adj.counit (Y✝.obj x✝) ≫ 𝟙 (Y✝.obj x✝) =
    (𝟙 (F.obj (G.obj (X✝.obj x✝))) ≫ NatTrans.app adj.counit (X✝.obj x✝) ≫ 𝟙 (X✝.obj x✝)) ≫ NatTrans.app f✝ x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ whiskerRight
        (NatTrans.mk fun X =>
          (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv)
        ((whiskeringRight C D E).obj F) ≫
      (Functor.associator ((whiskeringRight C D E).obj F) ((whiskeringRight C E D).obj G)
            ((whiskeringRight C D E).obj F)).hom ≫
        whiskerLeft ((whiskeringRight C D E).obj F)
          (NatTrans.mk fun X =>
            (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom) =
    NatTrans.id (𝟭 (C ⥤ D) ⋙ (whiskeringRight C D E).obj F)
[PROOFSTEP]
ext
[GOAL]
case w.h.w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
x✝¹ : C ⥤ D
x✝ : C
⊢ NatTrans.app
      (NatTrans.app
        (whiskerRight
            (NatTrans.mk fun X =>
              (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv)
            ((whiskeringRight C D E).obj F) ≫
          (Functor.associator ((whiskeringRight C D E).obj F) ((whiskeringRight C E D).obj G)
                ((whiskeringRight C D E).obj F)).hom ≫
            whiskerLeft ((whiskeringRight C D E).obj F)
              (NatTrans.mk fun X =>
                (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom))
        x✝¹)
      x✝ =
    NatTrans.app (NatTrans.app (NatTrans.id (𝟭 (C ⥤ D) ⋙ (whiskeringRight C D E).obj F)) x✝¹) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
x✝¹ : C ⥤ D
x✝ : C
⊢ F.map (𝟙 (x✝¹.obj x✝) ≫ NatTrans.app adj.unit (x✝¹.obj x✝) ≫ 𝟙 (G.obj (F.obj (x✝¹.obj x✝)))) ≫
      𝟙 (F.obj (G.obj (F.obj (x✝¹.obj x✝)))) ≫
        𝟙 (F.obj (G.obj (F.obj (x✝¹.obj x✝)))) ≫ NatTrans.app adj.counit (F.obj (x✝¹.obj x✝)) ≫ 𝟙 (F.obj (x✝¹.obj x✝)) =
    𝟙 (F.obj (x✝¹.obj x✝))
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ whiskerLeft ((whiskeringRight C E D).obj G)
        (NatTrans.mk fun X =>
          (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv) ≫
      (Functor.associator ((whiskeringRight C E D).obj G) ((whiskeringRight C D E).obj F)
            ((whiskeringRight C E D).obj G)).inv ≫
        whiskerRight
          (NatTrans.mk fun X => (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom)
          ((whiskeringRight C E D).obj G) =
    NatTrans.id ((whiskeringRight C E D).obj G ⋙ 𝟭 (C ⥤ D))
[PROOFSTEP]
ext
[GOAL]
case w.h.w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
x✝¹ : C ⥤ E
x✝ : C
⊢ NatTrans.app
      (NatTrans.app
        (whiskerLeft ((whiskeringRight C E D).obj G)
            (NatTrans.mk fun X =>
              (Functor.rightUnitor ((𝟭 (C ⥤ D)).obj X)).inv ≫ whiskerLeft X adj.unit ≫ (Functor.associator X F G).inv) ≫
          (Functor.associator ((whiskeringRight C E D).obj G) ((whiskeringRight C D E).obj F)
                ((whiskeringRight C E D).obj G)).inv ≫
            whiskerRight
              (NatTrans.mk fun X =>
                (Functor.associator X G F).hom ≫ whiskerLeft X adj.counit ≫ (Functor.rightUnitor X).hom)
              ((whiskeringRight C E D).obj G))
        x✝¹)
      x✝ =
    NatTrans.app (NatTrans.app (NatTrans.id ((whiskeringRight C E D).obj G ⋙ 𝟭 (C ⥤ D))) x✝¹) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.63, u_1} C
inst✝¹ : Category.{?u.67, u_2} D
inst✝ : Category.{?u.71, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
x✝¹ : C ⥤ E
x✝ : C
⊢ (𝟙 (G.obj (x✝¹.obj x✝)) ≫ NatTrans.app adj.unit (G.obj (x✝¹.obj x✝)) ≫ 𝟙 (G.obj (F.obj (G.obj (x✝¹.obj x✝))))) ≫
      𝟙 (G.obj (F.obj (G.obj (x✝¹.obj x✝)))) ≫
        G.map (𝟙 (F.obj (G.obj (x✝¹.obj x✝))) ≫ NatTrans.app adj.counit (x✝¹.obj x✝) ≫ 𝟙 (x✝¹.obj x✝)) =
    𝟙 (G.obj (x✝¹.obj x✝))
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ ∀ ⦃X Y : D ⥤ C⦄ (f : X ⟶ Y),
    (𝟭 (D ⥤ C)).map f ≫
        (fun X =>
            (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom)
          Y =
      (fun X => (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom)
          X ≫
        ((whiskeringLeft E D C).obj G ⋙ (whiskeringLeft D E C).obj F).map f
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : D ⥤ C
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 (D ⥤ C)).map f✝ ≫
      (fun X => (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom)
        Y✝ =
    (fun X => (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom)
        X✝ ≫
      ((whiskeringLeft E D C).obj G ⋙ (whiskeringLeft D E C).obj F).map f✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : D ⥤ C
f✝ : X✝ ⟶ Y✝
x✝ : D
⊢ NatTrans.app
      ((𝟭 (D ⥤ C)).map f✝ ≫
        (fun X =>
            (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom)
          Y✝)
      x✝ =
    NatTrans.app
      ((fun X =>
            (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom)
          X✝ ≫
        ((whiskeringLeft E D C).obj G ⋙ (whiskeringLeft D E C).obj F).map f✝)
      x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : D ⥤ C
f✝ : X✝ ⟶ Y✝
x✝ : D
⊢ NatTrans.app f✝ x✝ ≫ 𝟙 (Y✝.obj x✝) ≫ Y✝.map (NatTrans.app adj.unit x✝) ≫ 𝟙 (Y✝.obj (G.obj (F.obj x✝))) =
    (𝟙 (X✝.obj x✝) ≫ X✝.map (NatTrans.app adj.unit x✝) ≫ 𝟙 (X✝.obj (G.obj (F.obj x✝)))) ≫
      NatTrans.app f✝ (G.obj (F.obj x✝))
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ ∀ ⦃X Y : E ⥤ C⦄ (f : X ⟶ Y),
    ((whiskeringLeft D E C).obj F ⋙ (whiskeringLeft E D C).obj G).map f ≫
        (fun X => (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom) Y =
      (fun X => (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom) X ≫
        (𝟭 (E ⥤ C)).map f
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : E ⥤ C
f✝ : X✝ ⟶ Y✝
⊢ ((whiskeringLeft D E C).obj F ⋙ (whiskeringLeft E D C).obj G).map f✝ ≫
      (fun X => (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom) Y✝ =
    (fun X => (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom) X✝ ≫
      (𝟭 (E ⥤ C)).map f✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : E ⥤ C
f✝ : X✝ ⟶ Y✝
x✝ : E
⊢ NatTrans.app
      (((whiskeringLeft D E C).obj F ⋙ (whiskeringLeft E D C).obj G).map f✝ ≫
        (fun X => (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom) Y✝)
      x✝ =
    NatTrans.app
      ((fun X => (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom) X✝ ≫
        (𝟭 (E ⥤ C)).map f✝)
      x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X✝ Y✝ : E ⥤ C
f✝ : X✝ ⟶ Y✝
x✝ : E
⊢ NatTrans.app f✝ (F.obj (G.obj x✝)) ≫
      𝟙 (Y✝.obj (F.obj (G.obj x✝))) ≫ Y✝.map (NatTrans.app adj.counit x✝) ≫ 𝟙 (Y✝.obj x✝) =
    (𝟙 (X✝.obj (F.obj (G.obj x✝))) ≫ X✝.map (NatTrans.app adj.counit x✝) ≫ 𝟙 (X✝.obj x✝)) ≫ NatTrans.app f✝ x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ whiskerRight
        (NatTrans.mk fun X =>
          (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom)
        ((whiskeringLeft E D C).obj G) ≫
      (Functor.associator ((whiskeringLeft E D C).obj G) ((whiskeringLeft D E C).obj F)
            ((whiskeringLeft E D C).obj G)).hom ≫
        whiskerLeft ((whiskeringLeft E D C).obj G)
          (NatTrans.mk fun X =>
            (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom) =
    NatTrans.id (𝟭 (D ⥤ C) ⋙ (whiskeringLeft E D C).obj G)
[PROOFSTEP]
ext x
[GOAL]
case w.h.w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
x : D ⥤ C
x✝ : E
⊢ NatTrans.app
      (NatTrans.app
        (whiskerRight
            (NatTrans.mk fun X =>
              (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom)
            ((whiskeringLeft E D C).obj G) ≫
          (Functor.associator ((whiskeringLeft E D C).obj G) ((whiskeringLeft D E C).obj F)
                ((whiskeringLeft E D C).obj G)).hom ≫
            whiskerLeft ((whiskeringLeft E D C).obj G)
              (NatTrans.mk fun X =>
                (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom))
        x)
      x✝ =
    NatTrans.app (NatTrans.app (NatTrans.id (𝟭 (D ⥤ C) ⋙ (whiskeringLeft E D C).obj G)) x) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
x : D ⥤ C
x✝ : E
⊢ (𝟙 (x.obj (G.obj x✝)) ≫ x.map (NatTrans.app adj.unit (G.obj x✝)) ≫ 𝟙 (x.obj (G.obj (F.obj (G.obj x✝))))) ≫
      𝟙 (x.obj (G.obj (F.obj (G.obj x✝)))) ≫
        𝟙 (x.obj (G.obj (F.obj (G.obj x✝)))) ≫ x.map (G.map (NatTrans.app adj.counit x✝)) ≫ 𝟙 (x.obj (G.obj x✝)) =
    𝟙 (x.obj (G.obj x✝))
[PROOFSTEP]
simp [Category.id_comp, Category.comp_id, ← x.map_comp]
[GOAL]
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
⊢ whiskerLeft ((whiskeringLeft D E C).obj F)
        (NatTrans.mk fun X =>
          (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom) ≫
      (Functor.associator ((whiskeringLeft D E C).obj F) ((whiskeringLeft E D C).obj G)
            ((whiskeringLeft D E C).obj F)).inv ≫
        whiskerRight
          (NatTrans.mk fun X => (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom)
          ((whiskeringLeft D E C).obj F) =
    NatTrans.id ((whiskeringLeft D E C).obj F ⋙ 𝟭 (D ⥤ C))
[PROOFSTEP]
ext x
[GOAL]
case w.h.w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
x : E ⥤ C
x✝ : D
⊢ NatTrans.app
      (NatTrans.app
        (whiskerLeft ((whiskeringLeft D E C).obj F)
            (NatTrans.mk fun X =>
              (Functor.leftUnitor ((𝟭 (D ⥤ C)).obj X)).inv ≫ whiskerRight adj.unit X ≫ (Functor.associator F G X).hom) ≫
          (Functor.associator ((whiskeringLeft D E C).obj F) ((whiskeringLeft E D C).obj G)
                ((whiskeringLeft D E C).obj F)).inv ≫
            whiskerRight
              (NatTrans.mk fun X =>
                (Functor.associator G F X).inv ≫ whiskerRight adj.counit X ≫ (Functor.leftUnitor X).hom)
              ((whiskeringLeft D E C).obj F))
        x)
      x✝ =
    NatTrans.app (NatTrans.app (NatTrans.id ((whiskeringLeft D E C).obj F ⋙ 𝟭 (D ⥤ C))) x) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.w.h
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{?u.21134, u_1} C
inst✝¹ : Category.{?u.21138, u_2} D
inst✝ : Category.{?u.21142, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
x : E ⥤ C
x✝ : D
⊢ (𝟙 (x.obj (F.obj x✝)) ≫ x.map (F.map (NatTrans.app adj.unit x✝)) ≫ 𝟙 (x.obj (F.obj (G.obj (F.obj x✝))))) ≫
      𝟙 (x.obj (F.obj (G.obj (F.obj x✝)))) ≫
        𝟙 (x.obj (F.obj (G.obj (F.obj x✝)))) ≫ x.map (NatTrans.app adj.counit (F.obj x✝)) ≫ 𝟙 (x.obj (F.obj x✝)) =
    𝟙 (x.obj (F.obj x✝))
[PROOFSTEP]
simp [Category.id_comp, Category.comp_id, ← x.map_comp]
