∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (X : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProducts C] {X_1 Y : (CategoryTheory.prodComonad X).Coalgebra} (f : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp f.f
      (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp Y.a CategoryTheory.Limits.prod.fst)).hom =
    (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp X_1.a CategoryTheory.Limits.prod.fst)).hom