no goals
C : Type u
inst✝¹ : Category C
D : Type ?u.16029
inst✝ : Category D
P : MorphismProperty C
hP : RespectsIso P
f g : Arrow C
e : f ≅ g
⊢ P f.hom ↔ P g.hom
rw [← Arrow.inv_left_hom_right e.hom, hP.cancel_left_isIso, hP.cancel_right_isIso]