C : Type u
inst✝² : Category C
D : Type ?u.40576
inst✝¹ : Category D
P : MorphismProperty C
inst✝ : HasPushouts C
hP₁ : RespectsIso P
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B), P f → P pushout.inr
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
e : B' ≅ pushout f g := IsPushout.isoPushout (_ : IsPushout f g g' f')
⊢ P f'
C : Type u
inst✝² : Category C
D : Type ?u.40576
inst✝¹ : Category D
P : MorphismProperty C
inst✝ : HasPushouts C
hP₁ : RespectsIso P
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B), P f → P pushout.inr
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
⊢ P f'
let e := sq.flip.isoPushout
C : Type u
inst✝² : Category C
D : Type ?u.40576
inst✝¹ : Category D
P : MorphismProperty C
inst✝ : HasPushouts C
hP₁ : RespectsIso P
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B), P f → P pushout.inr
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
e : B' ≅ pushout f g := IsPushout.isoPushout (_ : IsPushout f g g' f')
⊢ P pushout.inr
C : Type u
inst✝² : Category C
D : Type ?u.40576
inst✝¹ : Category D
P : MorphismProperty C
inst✝ : HasPushouts C
hP₁ : RespectsIso P
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B), P f → P pushout.inr
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
e : B' ≅ pushout f g := IsPushout.isoPushout (_ : IsPushout f g g' f')
⊢ P f'
rw [← hP₁.cancel_right_isIso _ e.hom, sq.flip.inr_isoPushout_hom]
no goals
C : Type u
inst✝² : Category C
D : Type ?u.40576
inst✝¹ : Category D
P : MorphismProperty C
inst✝ : HasPushouts C
hP₁ : RespectsIso P
hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B), P f → P pushout.inr
A A' B B' : C
f : A ⟶ A'
g : A ⟶ B
f' : B ⟶ B'
g' : A' ⟶ B'
sq : IsPushout g f f' g'
hf : P f
e : B' ≅ pushout f g := IsPushout.isoPushout (_ : IsPushout f g g' f')
⊢ P pushout.inr
exact hP₂ _ _ _ f g hf