[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G H : D ⥤ E
α : G ⟶ H
X Y : C
f : X ⟶ Y
⊢ (F ⋙ G).map f ≫ (fun X => NatTrans.app α (F.obj X)) Y = (fun X => NatTrans.app α (F.obj X)) X ≫ (F ⋙ H).map f
[PROOFSTEP]
rw [Functor.comp_map, Functor.comp_map, α.naturality]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ (G ⋙ F).map f ≫ (fun X => F.map (NatTrans.app α X)) Y = (fun X => F.map (NatTrans.app α X)) X ≫ (H ⋙ F).map f
[PROOFSTEP]
rw [Functor.comp_map, Functor.comp_map, ← F.map_comp, ← F.map_comp, α.naturality]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
H : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ (((fun F => Functor.mk { obj := fun G => F ⋙ G, map := fun {X Y} α => whiskerLeft F α }) X✝).obj H).map f ≫
      (fun c => H.map (NatTrans.app τ c)) Y =
    (fun c => H.map (NatTrans.app τ c)) X ≫
      (((fun F => Functor.mk { obj := fun G => F ⋙ G, map := fun {X Y} α => whiskerLeft F α }) Y✝).obj H).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
H : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ H.map (X✝.map f) ≫ H.map (NatTrans.app τ Y) = H.map (NatTrans.app τ X) ≫ H.map (Y✝.map f)
[PROOFSTEP]
rw [← H.map_comp, ← H.map_comp, ← τ.naturality]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
X Y : D ⥤ E
f : X ⟶ Y
⊢ ((fun F => Functor.mk { obj := fun G => F ⋙ G, map := fun {X Y} α => whiskerLeft F α }) X✝).map f ≫
      (fun H => NatTrans.mk fun c => H.map (NatTrans.app τ c)) Y =
    (fun H => NatTrans.mk fun c => H.map (NatTrans.app τ c)) X ≫
      ((fun F => Functor.mk { obj := fun G => F ⋙ G, map := fun {X Y} α => whiskerLeft F α }) Y✝).map f
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
X Y : D ⥤ E
f : X ⟶ Y
x✝ : C
⊢ NatTrans.app
      (((fun F => Functor.mk { obj := fun G => F ⋙ G, map := fun {X Y} α => whiskerLeft F α }) X✝).map f ≫
        (fun H => NatTrans.mk fun c => H.map (NatTrans.app τ c)) Y)
      x✝ =
    NatTrans.app
      ((fun H => NatTrans.mk fun c => H.map (NatTrans.app τ c)) X ≫
        ((fun F => Functor.mk { obj := fun G => F ⋙ G, map := fun {X Y} α => whiskerLeft F α }) Y✝).map f)
      x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
X Y : D ⥤ E
f : X ⟶ Y
x✝ : C
⊢ NatTrans.app f (X✝.obj x✝) ≫ Y.map (NatTrans.app τ x✝) = X.map (NatTrans.app τ x✝) ≫ NatTrans.app f (Y✝.obj x✝)
[PROOFSTEP]
rw [f.naturality]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (((fun H => Functor.mk { obj := fun F => F ⋙ H, map := fun {X Y} α => whiskerRight α H }) X✝).obj F).map f ≫
      (fun c => NatTrans.app τ (F.obj c)) Y =
    (fun c => NatTrans.app τ (F.obj c)) X ≫
      (((fun H => Functor.mk { obj := fun F => F ⋙ H, map := fun {X Y} α => whiskerRight α H }) Y✝).obj F).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ X✝.map (F.map f) ≫ NatTrans.app τ (F.obj Y) = NatTrans.app τ (F.obj X) ≫ Y✝.map (F.map f)
[PROOFSTEP]
rw [τ.naturality]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
X Y : C ⥤ D
f : X ⟶ Y
⊢ ((fun H => Functor.mk { obj := fun F => F ⋙ H, map := fun {X Y} α => whiskerRight α H }) X✝).map f ≫
      (fun F => NatTrans.mk fun c => NatTrans.app τ (F.obj c)) Y =
    (fun F => NatTrans.mk fun c => NatTrans.app τ (F.obj c)) X ≫
      ((fun H => Functor.mk { obj := fun F => F ⋙ H, map := fun {X Y} α => whiskerRight α H }) Y✝).map f
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
X Y : C ⥤ D
f : X ⟶ Y
x✝ : C
⊢ NatTrans.app
      (((fun H => Functor.mk { obj := fun F => F ⋙ H, map := fun {X Y} α => whiskerRight α H }) X✝).map f ≫
        (fun F => NatTrans.mk fun c => NatTrans.app τ (F.obj c)) Y)
      x✝ =
    NatTrans.app
      ((fun F => NatTrans.mk fun c => NatTrans.app τ (F.obj c)) X ≫
        ((fun H => Functor.mk { obj := fun F => F ⋙ H, map := fun {X Y} α => whiskerRight α H }) Y✝).map f)
      x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
X Y : C ⥤ D
f : X ⟶ Y
x✝ : C
⊢ X✝.map (NatTrans.app f x✝) ≫ NatTrans.app τ (Y.obj x✝) = NatTrans.app τ (X.obj x✝) ≫ Y✝.map (NatTrans.app f x✝)
[PROOFSTEP]
rw [← NatTrans.naturality]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
inst✝ : Faithful F
X✝ Y✝ : C ⥤ D
a₁✝ a₂✝ : X✝ ⟶ Y✝
hαβ : ((whiskeringRight C D E).obj F).map a₁✝ = ((whiskeringRight C D E).obj F).map a₂✝
⊢ a₁✝ = a₂✝
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
inst✝ : Faithful F
X✝ Y✝ : C ⥤ D
a₁✝ a₂✝ : X✝ ⟶ Y✝
hαβ : ((whiskeringRight C D E).obj F).map a₁✝ = ((whiskeringRight C D E).obj F).map a₂✝
X : C
⊢ NatTrans.app a₁✝ X = NatTrans.app a₂✝ X
[PROOFSTEP]
exact (F.map_injective <| congr_fun (congr_arg NatTrans.app hαβ) X)
[GOAL]
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ B
G : B ⥤ C
⊢ (associator F (𝟭 B) G).hom ≫ whiskerLeft F (leftUnitor G).hom = whiskerRight (rightUnitor F).hom G
[PROOFSTEP]
aesop_cat
[GOAL]
A : Type u₁
inst✝⁴ : Category.{v₁, u₁} A
B : Type u₂
inst✝³ : Category.{v₂, u₂} B
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
K : D ⥤ E
⊢ whiskerRight (associator F G H).hom K ≫ (associator F (G ⋙ H) K).hom ≫ whiskerLeft F (associator G H K).hom =
    (associator (F ⋙ G) H K).hom ≫ (associator F G (H ⋙ K)).hom
[PROOFSTEP]
aesop_cat
