[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α β : F.NatTrans G
h : α = β
X : C
⊢ NatTrans.app α X = NatTrans.app β X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.NatTrans G
X Y U V : C
f : X ⟶ Y
g : Y ⟶ U
h : U ⟶ V
⊢ app α X ≫ G.map f ≫ G.map g ≫ G.map h = F.map f ≫ F.map g ≫ F.map h ≫ app α V
[PROOFSTEP]
simp
