C : Type u
inst✝² : Category C
D : Type ?u.19471
inst✝¹ : Category D
P : MorphismProperty C
inst✝ : HasPullbacks C
hP₁ : RespectsIso P
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S), P g → P pullback.fst
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
e : Y' ≅ pullback f g := IsPullback.isoPullback (_ : IsPullback g' f' f g)
⊢ P g'
C : Type u
inst✝² : Category C
D : Type ?u.19471
inst✝¹ : Category D
P : MorphismProperty C
inst✝ : HasPullbacks C
hP₁ : RespectsIso P
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S), P g → P pullback.fst
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
⊢ P g'
let e := sq.flip.isoPullback
C : Type u
inst✝² : Category C
D : Type ?u.19471
inst✝¹ : Category D
P : MorphismProperty C
inst✝ : HasPullbacks C
hP₁ : RespectsIso P
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S), P g → P pullback.fst
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
e : Y' ≅ pullback f g := IsPullback.isoPullback (_ : IsPullback g' f' f g)
⊢ P pullback.fst
C : Type u
inst✝² : Category C
D : Type ?u.19471
inst✝¹ : Category D
P : MorphismProperty C
inst✝ : HasPullbacks C
hP₁ : RespectsIso P
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S), P g → P pullback.fst
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
e : Y' ≅ pullback f g := IsPullback.isoPullback (_ : IsPullback g' f' f g)
⊢ P g'
rw [← hP₁.cancel_left_isIso e.inv, sq.flip.isoPullback_inv_fst]
no goals
C : Type u
inst✝² : Category C
D : Type ?u.19471
inst✝¹ : Category D
P : MorphismProperty C
inst✝ : HasPullbacks C
hP₁ : RespectsIso P
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S), P g → P pullback.fst
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
e : Y' ≅ pullback f g := IsPullback.isoPullback (_ : IsPullback g' f' f g)
⊢ P pullback.fst
exact hP₂ _ _ _ f g hg