∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C],
  (CategoryTheory.coalgebraEquivOver X).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun f =>
        CategoryTheory.Over.isoMk
          (CategoryTheory.Iso.refl
            (((CategoryTheory.overToCoalgebra X).comp (CategoryTheory.coalgebraToOver X)).obj f).left)
          ⋯)
      ⋯