C : Type u
inst✝² : Category C
D : Type ?u.24086
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left pullback.fst ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom (_ : (𝟭 C).map g.left ≫ Y.hom = X.hom) (_ : f = f)
⊢ P ((baseChange f).map g).left
C : Type u
inst✝² : Category C
D : Type ?u.24086
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
⊢ P ((baseChange f).map g).left
let e :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫
    pullback.congrHom (g.w.trans (Category.comp_id _)) rfl
C : Type u
inst✝² : Category C
D : Type ?u.24086
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left pullback.fst ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom (_ : (𝟭 C).map g.left ≫ Y.hom = X.hom) (_ : f = f)
this : e.inv ≫ pullback.snd = ((baseChange f).map g).left
⊢ P ((baseChange f).map g).left
C : Type u
inst✝² : Category C
D : Type ?u.24086
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left pullback.fst ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom (_ : (𝟭 C).map g.left ≫ Y.hom = X.hom) (_ : f = f)
⊢ P ((baseChange f).map g).left
have : e.inv ≫ pullback.snd = ((baseChange f).map g).left := by
  apply pullback.hom_ext <;> dsimp <;> simp
C : Type u
inst✝² : Category C
D : Type ?u.24086
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left pullback.fst ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom (_ : (𝟭 C).map g.left ≫ Y.hom = X.hom) (_ : f = f)
this : e.inv ≫ pullback.snd = ((baseChange f).map g).left
⊢ P pullback.snd
C : Type u
inst✝² : Category C
D : Type ?u.24086
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left pullback.fst ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom (_ : (𝟭 C).map g.left ≫ Y.hom = X.hom) (_ : f = f)
this : e.inv ≫ pullback.snd = ((baseChange f).map g).left
⊢ P ((baseChange f).map g).left
rw [← this, hP.respectsIso.cancel_left_isIso]
no goals
C : Type u
inst✝² : Category C
D : Type ?u.24086
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left pullback.fst ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom (_ : (𝟭 C).map g.left ≫ Y.hom = X.hom) (_ : f = f)
this : e.inv ≫ pullback.snd = ((baseChange f).map g).left
⊢ P pullback.snd
exact hP.snd _ _ H
no goals
C : Type u
inst✝² : Category C
D : Type ?u.24086
inst✝¹ : Category D
inst✝ : HasPullbacks C
P : MorphismProperty C
hP : StableUnderBaseChange P
S S' : C
f : S' ⟶ S
X Y : Over S
g : X ⟶ Y
H : P g.left
e : pullback g.left pullback.fst ≅ pullback X.hom f :=
  pullbackRightPullbackFstIso Y.hom f g.left ≪≫ pullback.congrHom (_ : (𝟭 C).map g.left ≫ Y.hom = X.hom) (_ : f = f)
⊢ e.inv ≫ pullback.snd = ((baseChange f).map g).left
apply pullback.hom_ext <;> dsimp <;> simp