C : Type u
inst✝² : Category C
D : Type ?u.85650
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.universally P f
hg : MorphismProperty.universally P g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ g)
⊢ P f'
C : Type u
inst✝² : Category C
D : Type ?u.85650
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
⊢ StableUnderComposition (MorphismProperty.universally P)
intro X Y Z f g hf hg X' Z' i₁ i₂ f' H
C : Type u
inst✝² : Category C
D : Type ?u.85650
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.universally P f
hg : MorphismProperty.universally P g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ g)
this : pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g) ≫ pullback.fst = f'
⊢ P f'
C : Type u
inst✝² : Category C
D : Type ?u.85650
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.universally P f
hg : MorphismProperty.universally P g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ g)
⊢ P f'
have := pullback.lift_fst _ _ (H.w.trans (Category.assoc _ _ _).symm)
C : Type u
inst✝² : Category C
D : Type ?u.85650
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.universally P f
hg : MorphismProperty.universally P g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H✝ : IsPullback f' i₁ i₂ (f ≫ g)
H : IsPullback (pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g) ≫ pullback.fst) i₁ i₂ (f ≫ g)
this : pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g) ≫ pullback.fst = f'
⊢ P (pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g) ≫ pullback.fst)
C : Type u
inst✝² : Category C
D : Type ?u.85650
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.universally P f
hg : MorphismProperty.universally P g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (f ≫ g)
this : pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g) ≫ pullback.fst = f'
⊢ P f'
rw [← this] at H⊢
C : Type u
inst✝² : Category C
D : Type ?u.85650
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.universally P f
hg : MorphismProperty.universally P g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H✝ : IsPullback f' i₁ i₂ (f ≫ g)
H : IsPullback (pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g) ≫ pullback.fst) i₁ i₂ (f ≫ g)
this : pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g) ≫ pullback.fst = f'
⊢ P (pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g))
C : Type u
inst✝² : Category C
D : Type ?u.85650
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.universally P f
hg : MorphismProperty.universally P g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H✝ : IsPullback f' i₁ i₂ (f ≫ g)
H : IsPullback (pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g) ≫ pullback.fst) i₁ i₂ (f ≫ g)
this : pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g) ≫ pullback.fst = f'
⊢ P (pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g) ≫ pullback.fst)
apply hP _ _ _ (hg _ _ _ <| IsPullback.of_hasPullback _ _)
no goals
C : Type u
inst✝² : Category C
D : Type ?u.85650
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderComposition P
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.universally P f
hg : MorphismProperty.universally P g
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H✝ : IsPullback f' i₁ i₂ (f ≫ g)
H : IsPullback (pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g) ≫ pullback.fst) i₁ i₂ (f ≫ g)
this : pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g) ≫ pullback.fst = f'
⊢ P (pullback.lift f' (i₁ ≫ f) (_ : f' ≫ i₂ = (i₁ ≫ f) ≫ g))
exact hf _ _ _ (H.of_right (pullback.lift_snd _ _ _) (IsPullback.of_hasPullback i₂ g))