no goals
C : Type u₁
inst✝³ : Category C
C' : Type u₂
inst✝² : Category C'
D : GlueData C
F : C ⥤ C'
H : (i j k : D.J) → PreservesLimit (cospan (f D i j) (f D i k)) F
inst✝¹ : HasMulticoequalizer (diagram D)
inst✝ : PreservesColimit (MultispanIndex.multispan (diagram D)) F
i : D.J
⊢ ι (mapGlueData D F) i ≫ (gluedIso D F).inv = F.map (ι D i)
rw [Iso.comp_inv_eq, ι_gluedIso_hom]