case hP
C : Type u
inst✝¹ : Category C
D : Type ?u.20586
inst✝ : Category D
P : MorphismProperty C
hP : StableUnderBaseChange P
⊢ ∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
C : Type u
inst✝¹ : Category C
D : Type ?u.20586
inst✝ : Category D
P : MorphismProperty C
hP : StableUnderBaseChange P
⊢ RespectsIso P
apply RespectsIso.of_respects_arrow_iso
case hP
C : Type u
inst✝¹ : Category C
D : Type ?u.20586
inst✝ : Category D
P : MorphismProperty C
hP : StableUnderBaseChange P
f g : Arrow C
e : f ≅ g
⊢ P f.hom → P g.hom
case hP
C : Type u
inst✝¹ : Category C
D : Type ?u.20586
inst✝ : Category D
P : MorphismProperty C
hP : StableUnderBaseChange P
⊢ ∀ (f g : Arrow C), (f ≅ g) → P f.hom → P g.hom
intro f g e
no goals
case hP
C : Type u
inst✝¹ : Category C
D : Type ?u.20586
inst✝ : Category D
P : MorphismProperty C
hP : StableUnderBaseChange P
f g : Arrow C
e : f ≅ g
⊢ P f.hom → P g.hom
exact hP (IsPullback.of_horiz_isIso (CommSq.mk e.inv.w))