C : Type u
inst✝² : Category C
D : Type ?u.79385
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : RespectsIso P
X Y S : C
f : X ⟶ S
g : Y ⟶ S
h : MorphismProperty.diagonal P g
⊢ MorphismProperty.diagonal P pullback.fst
C : Type u
inst✝² : Category C
D : Type ?u.79385
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : RespectsIso P
⊢ ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S), MorphismProperty.diagonal P g → MorphismProperty.diagonal P pullback.fst
introv h
C : Type u
inst✝² : Category C
D : Type ?u.79385
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : RespectsIso P
X Y S : C
f : X ⟶ S
g : Y ⟶ S
h : MorphismProperty.diagonal P g
⊢ P ((baseChange f).map (Over.homMk (pullback.diagonal g))).left
C : Type u
inst✝² : Category C
D : Type ?u.79385
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : RespectsIso P
X Y S : C
f : X ⟶ S
g : Y ⟶ S
h : MorphismProperty.diagonal P g
⊢ MorphismProperty.diagonal P pullback.fst
rw [diagonal_iff, diagonal_pullback_fst, hP'.cancel_left_isIso, hP'.cancel_right_isIso]
no goals
C : Type u
inst✝² : Category C
D : Type ?u.79385
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : RespectsIso P
X Y S : C
f : X ⟶ S
g : Y ⟶ S
h : MorphismProperty.diagonal P g
⊢ P ((baseChange f).map (Over.homMk (pullback.diagonal g))).left
exact hP.baseChange_map f _ (by simpa)
no goals
C : Type u
inst✝² : Category C
D : Type ?u.79385
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
hP' : RespectsIso P
X Y S : C
f : X ⟶ S
g : Y ⟶ S
h : MorphismProperty.diagonal P g
⊢ P (Over.homMk (pullback.diagonal g)).left
simpa