∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A B : G.Coalgebra}
  (h : A.A ≅ B.A)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp A.a (G.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom B.a)
      CategoryTheory.Comonad.Coalgebra.isoMk._auto_1),
  (CategoryTheory.Comonad.Coalgebra.isoMk h w).inv.f = h.inv