-- 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
⊢ pullback (pullback.fst f g) ((Scheme.Cover.pullbackCover S.affineCover f).map i) ≅ ?m.107585

Tactic:
refine pullbackSymmetry _ _ ≪≫ pullbackRightPullbackFstIso f g _ ≪≫ ?_ ≪≫
  (pullbackRightPullbackFstIso (S.affineCover.map i) g
    (pullback.snd f (S.affineCover.map i))).symm

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

Tactic:
letI := isLocal_affineProperty P

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.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
⊢ P (pullback.fst f g)

Tactic:
rw [IsLocalAtTarget.iff_of_openCover (P := P) (S.affineCover.pullbackCover f)]

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

Tactic:
intro i

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

Tactic:
exact asIso
  (pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) (by simpa using pullback.condition) (by simp))

Result:
no goals