no goals
C : Type u
inst✝² : Category C
D : Type ?u.13555
inst✝¹ : Category D
P : MorphismProperty C
hP : RespectsIso P
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : P (f ≫ g)
⊢ P g
simpa using hP.1 (asIso f).symm (f ≫ g) h