no goals
T : Type u
inst✝ : Category T
i : Arrow T
X Y : T
p : X ≅ Y
sq : i ⟶ mk p.hom
⊢ i.hom ≫ sq.right ≫ p.inv = sq.left
simpa only [Category.assoc] using (Iso.comp_inv_eq p).mpr (Arrow.w_mk_right sq).symm