∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor A B}
  {H K : CategoryTheory.Functor A C} (α : F ⟶ G) (β : H ⟶ K) (X : A),
  ((CategoryTheory.NatTrans.prod' α β).app X).2 = β.app X