-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
theorem isStableUnderBaseChange (hP' : Q.IsStableUnderBaseChange) :
    P.IsStableUnderBaseChange :=
  MorphismProperty.IsStableUnderBaseChange.mk'
    (fun X Y S f g _ H => by
      rw [IsLocalAtTarget.iff_of_openCover (P := P) (S.affineCover.pullbackCover f)]
      intro i
      let e : pullback (pullback.fst f g) ((S.affineCover.pullbackCover f).map i) ≅
          _

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
i : (Scheme.Cover.pullbackCover S.affineCover f).1
e : pullback (pullback.fst f g) ((Scheme.Cover.pullbackCover S.affineCover f).map i) ≅
  pullback (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g) :=
  pullbackSymmetry (pullback.fst f g) ((Scheme.Cover.pullbackCover S.affineCover f).map i) ≪≫
    pullbackRightPullbackFstIso f g ((Scheme.Cover.pullbackCover S.affineCover f).map i) ≪≫
      asIso
          (pullback.map ((Scheme.Cover.pullbackCover S.affineCover f).map i ≫ f) g
            (pullback.snd f (S.affineCover.map i) ≫ S.affineCover.map i) g
            (𝟙 ((Scheme.Cover.pullbackCover S.affineCover f).obj i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫
        (pullbackRightPullbackFstIso (S.affineCover.map i) g (pullback.snd f (S.affineCover.map i))).symm
this :
  e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g) =
    (Scheme.Cover.pullbackCover S.affineCover f).pullbackHom (pullback.fst f g) i
⊢ P (pullback.fst (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g))

Tactic:
apply HasAffineProperty.pullback_fst_of_right hP'

Result:
case H
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
i : (Scheme.Cover.pullbackCover S.affineCover f).1
e : pullback (pullback.fst f g) ((Scheme.Cover.pullbackCover S.affineCover f).map i) ≅
  pullback (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g) :=
  pullbackSymmetry (pullback.fst f g) ((Scheme.Cover.pullbackCover S.affineCover f).map i) ≪≫
    pullbackRightPullbackFstIso f g ((Scheme.Cover.pullbackCover S.affineCover f).map i) ≪≫
      asIso
          (pullback.map ((Scheme.Cover.pullbackCover S.affineCover f).map i ≫ f) g
            (pullback.snd f (S.affineCover.map i) ≫ S.affineCover.map i) g
            (𝟙 ((Scheme.Cover.pullbackCover S.affineCover f).obj i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫
        (pullbackRightPullbackFstIso (S.affineCover.map i) g (pullback.snd f (S.affineCover.map i))).symm
this :
  e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g) =
    (Scheme.Cover.pullbackCover S.affineCover f).pullbackHom (pullback.fst f g) i
⊢ Q (pullback.fst (S.affineCover.map i) g)

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
i : (Scheme.Cover.pullbackCover S.affineCover f).1
⊢ g ≫ 𝟙 S = 𝟙 Y ≫ g

Tactic:
simp

Result:
no goals

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
i : (Scheme.Cover.pullbackCover S.affineCover f).1
e : pullback (pullback.fst f g) ((Scheme.Cover.pullbackCover S.affineCover f).map i) ≅
  pullback (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g) :=
  pullbackSymmetry (pullback.fst f g) ((Scheme.Cover.pullbackCover S.affineCover f).map i) ≪≫
    pullbackRightPullbackFstIso f g ((Scheme.Cover.pullbackCover S.affineCover f).map i) ≪≫
      asIso
          (pullback.map ((Scheme.Cover.pullbackCover S.affineCover f).map i ≫ f) g
            (pullback.snd f (S.affineCover.map i) ≫ S.affineCover.map i) g
            (𝟙 ((Scheme.Cover.pullbackCover S.affineCover f).obj i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫
        (pullbackRightPullbackFstIso (S.affineCover.map i) g (pullback.snd f (S.affineCover.map i))).symm
⊢ e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g) =
    (Scheme.Cover.pullbackCover S.affineCover f).pullbackHom (pullback.fst f g) i

Tactic:
simp [e, Scheme.Cover.pullbackHom]

Result:
no goals

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
i : (Scheme.Cover.pullbackCover S.affineCover f).1
⊢ P ((Scheme.Cover.pullbackCover S.affineCover f).pullbackHom (pullback.fst f g) i)

Tactic:
let e : pullback (pullback.fst f g) ((S.affineCover.pullbackCover f).map i) ≅
    _ := by
  refine pullbackSymmetry _ _ ≪≫ pullbackRightPullbackFstIso f g _ ≪≫ ?_ ≪≫
    (pullbackRightPullbackFstIso (S.affineCover.map i) g
      (pullback.snd f (S.affineCover.map i))).symm
  exact asIso
    (pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) (by simpa using pullback.condition) (by simp))

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
i : (Scheme.Cover.pullbackCover S.affineCover f).1
e : pullback (pullback.fst f g) ((Scheme.Cover.pullbackCover S.affineCover f).map i) ≅
  pullback (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g) :=
  pullbackSymmetry (pullback.fst f g) ((Scheme.Cover.pullbackCover S.affineCover f).map i) ≪≫
    pullbackRightPullbackFstIso f g ((Scheme.Cover.pullbackCover S.affineCover f).map i) ≪≫
      asIso
          (pullback.map ((Scheme.Cover.pullbackCover S.affineCover f).map i ≫ f) g
            (pullback.snd f (S.affineCover.map i) ≫ S.affineCover.map i) g
            (𝟙 ((Scheme.Cover.pullbackCover S.affineCover f).obj i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫
        (pullbackRightPullbackFstIso (S.affineCover.map i) g (pullback.snd f (S.affineCover.map i))).symm
⊢ P ((Scheme.Cover.pullbackCover S.affineCover f).pullbackHom (pullback.fst f g) i)