no goals
J : Type u₁
inst✝³ : Category J
K✝ : Type u₂
inst✝² : Category K✝
C : Type u₃
inst✝¹ : Category C
D : Type u₄
inst✝ : Category D
F K : J ⥤ C
c d : Cocone K
f : c ⟶ d
i : IsIso f.Hom
⊢ f ≫ CoconeMorphism.mk (inv f.Hom) = 𝟙 c ∧ CoconeMorphism.mk (inv f.Hom) ≫ f = 𝟙 d
aesop_cat