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

Tactic:
rw [← this, P.cancel_left_of_respectsIso]

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 (pullback.fst (pullback.snd f (S.affineCover.map i)) (pullback.fst (S.affineCover.map i) g))

Proof state:
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
this : Q.IsLocal := isLocal_affineProperty P
⊢ Q (pullback.fst (S.affineCover.map i) g)

Tactic:
rw [← pullbackSymmetry_hom_comp_snd, Q.cancel_left_of_respectsIso]

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
this : Q.IsLocal := isLocal_affineProperty P
⊢ Q (pullback.snd g (S.affineCover.map i))

Proof state:
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
this : Q.IsLocal := isLocal_affineProperty P
⊢ Q (pullback.snd g (S.affineCover.map i))

Tactic:
apply of_isPullback (.of_hasPullback _ _) H

Result:
no goals