Theorem: CategoryTheory.Functor.triangle (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
F : A ⥤ B
G : B ⥤ C
⊢ (associator F (𝟭 B) G).hom ≫ whiskerLeft F (leftUnitor G).hom = whiskerRight (rightUnitor F).hom G
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
F : A ⥤ B
G : B ⥤ C
x✝ : A
⊢ NatTrans.app ((associator F (𝟭 B) G).hom ≫ whiskerLeft F (leftUnitor G).hom) x✝ =
    NatTrans.app (whiskerRight (rightUnitor F).hom G) 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
F : A ⥤ B
G : B ⥤ C
x✝ : A
⊢ NatTrans.app ((associator F (𝟭 B) G).hom ≫ whiskerLeft F (leftUnitor G).hom) x✝ =
    NatTrans.app (whiskerRight (rightUnitor F).hom G) 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
F : A ⥤ B
G : B ⥤ C
x✝ : A
⊢ 𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)) ≫
      𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)) =
    Prefunctor.map 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
F : A ⥤ B
G : B ⥤ C
x✝ : A
⊢ 𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)) ≫
      𝟙 (Prefunctor.obj G.toPrefunctor (Prefunctor.obj F.toPrefunctor x✝)) =
    Prefunctor.map G.toPrefunctor (𝟙 (Prefunctor.obj F.toPrefunctor x✝))
Tactic:
simp
State after:
no goals