Theorem: CategoryTheory.Functor.pentagon (Moncalc/CategoryTheory/Whiskering.lean)

State before:
A : Type u₁
inst✝⁴ : Category A
B : Type u₂
inst✝³ : Category B
C : Type u₃
inst✝² : Category C
D : Type u₄
inst✝¹ : Category D
E : Type u₅
inst✝ : Category 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
Tactic:
ext
State after:
case w.h
A : Type u₁
inst✝⁴ : Category A
B : Type u₂
inst✝³ : Category B
C : Type u₃
inst✝² : Category C
D : Type u₄
inst✝¹ : Category D
E : Type u₅
inst✝ : Category E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
K : D ⥤ E
x✝ : A
⊢ NatTrans.app
      (whiskerRight (associator F G H).hom K ≫ (associator F (G ⋙ H) K).hom ≫ whiskerLeft F (associator G H K).hom) x✝ =
    NatTrans.app ((associator (F ⋙ G) H K).hom ≫ (associator F G (H ⋙ K)).hom) x✝

State before:
case w.h
A : Type u₁
inst✝⁴ : Category A
B : Type u₂
inst✝³ : Category B
C : Type u₃
inst✝² : Category C
D : Type u₄
inst✝¹ : Category D
E : Type u₅
inst✝ : Category E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
K : D ⥤ E
x✝ : A
⊢ NatTrans.app
      (whiskerRight (associator F G H).hom K ≫ (associator F (G ⋙ H) K).hom ≫ whiskerLeft F (associator G H K).hom) x✝ =
    NatTrans.app ((associator (F ⋙ G) H K).hom ≫ (associator F G (H ⋙ K)).hom) x✝
Tactic:
dsimp
State after:
case w.h
A : Type u₁
inst✝⁴ : Category A
B : Type u₂
inst✝³ : Category B
C : Type u₃
inst✝² : Category C
D : Type u₄
inst✝¹ : Category D
E : Type u₅
inst✝ : Category E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
K : D ⥤ E
x✝ : A
⊢ Prefunctor.map K.toPrefunctor
        (𝟙 (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) ≫
      𝟙
          (Prefunctor.obj K.toPrefunctor
            (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) ≫
        𝟙
          (Prefunctor.obj K.toPrefunctor
            (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) =
    𝟙
        (Prefunctor.obj K.toPrefunctor
          (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) ≫
      𝟙
        (Prefunctor.obj K.toPrefunctor
          (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝))))

State before:
case w.h
A : Type u₁
inst✝⁴ : Category A
B : Type u₂
inst✝³ : Category B
C : Type u₃
inst✝² : Category C
D : Type u₄
inst✝¹ : Category D
E : Type u₅
inst✝ : Category E
F : A ⥤ B
G : B ⥤ C
H : C ⥤ D
K : D ⥤ E
x✝ : A
⊢ Prefunctor.map K.toPrefunctor
        (𝟙 (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) ≫
      𝟙
          (Prefunctor.obj K.toPrefunctor
            (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) ≫
        𝟙
          (Prefunctor.obj K.toPrefunctor
            (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) =
    𝟙
        (Prefunctor.obj K.toPrefunctor
          (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)))) ≫
      𝟙
        (Prefunctor.obj K.toPrefunctor
          (Prefunctor.obj H.toPrefunctor (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝))))
Tactic:
simp
State after:
no goals