-- 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
⊢ P ((Scheme.Cover.pullbackCover S.affineCover f).pullbackHom (pullback.fst f g) i)

Tactic:
have : e.hom ≫ pullback.fst _ _ =
    (S.affineCover.pullbackCover f).pullbackHom (pullback.fst _ _) i := by
  simp [e, Scheme.Cover.pullbackHom]

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
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 ((Scheme.Cover.pullbackCover S.affineCover f).pullbackHom (pullback.fst f g) 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
⊢ ((Scheme.Cover.pullbackCover S.affineCover f).map i ≫ f) ≫ 𝟙 S =
    𝟙 ((Scheme.Cover.pullbackCover S.affineCover f).obj i) ≫ pullback.snd f (S.affineCover.map i) ≫ S.affineCover.map i

Tactic:
simpa using pullback.condition

Result:
no goals