-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
theorem pullback_fst_of_right (hP' : Q.IsStableUnderBaseChange)
    {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [IsAffine S] (H : Q g) :
    P (pullback.fst f 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
inst✝ : IsAffine S
H : Q g
this : Q.IsLocal := isLocal_affineProperty P
i : X.affineCover.1
e : pullback (pullback.fst f g) (X.affineCover.map i) ≅ pullback (X.affineCover.map i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.map i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.map i)
⊢ e.hom ≫ pullback.fst (X.affineCover.map i ≫ f) g = Scheme.Cover.pullbackHom X.affineCover (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
inst✝ : IsAffine S
H : Q g
this✝ : Q.IsLocal := isLocal_affineProperty P
i : X.affineCover.1
e : pullback (pullback.fst f g) (X.affineCover.map i) ≅ pullback (X.affineCover.map i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.map i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.map i)
this : e.hom ≫ pullback.fst (X.affineCover.map i ≫ f) g = Scheme.Cover.pullbackHom X.affineCover (pullback.fst f g) i
⊢ Q (Scheme.Cover.pullbackHom X.affineCover (pullback.fst f g) i)

Tactic:
rw [← this, Q.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
inst✝ : IsAffine S
H : Q g
this✝ : Q.IsLocal := isLocal_affineProperty P
i : X.affineCover.1
e : pullback (pullback.fst f g) (X.affineCover.map i) ≅ pullback (X.affineCover.map i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.map i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.map i)
this : e.hom ≫ pullback.fst (X.affineCover.map i ≫ f) g = Scheme.Cover.pullbackHom X.affineCover (pullback.fst f g) i
⊢ Q (pullback.fst (X.affineCover.map i ≫ f) 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
inst✝ : IsAffine S
H : Q g
this✝ : Q.IsLocal := isLocal_affineProperty P
i : X.affineCover.1
e : pullback (pullback.fst f g) (X.affineCover.map i) ≅ pullback (X.affineCover.map i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.map i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.map i)
this : e.hom ≫ pullback.fst (X.affineCover.map i ≫ f) g = Scheme.Cover.pullbackHom X.affineCover (pullback.fst f g) i
⊢ Q (pullback.fst (X.affineCover.map i ≫ f) g)

Tactic:
apply hP' (.of_hasPullback _ _)

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : IsAffine S
H : Q g
this✝ : Q.IsLocal := isLocal_affineProperty P
i : X.affineCover.1
e : pullback (pullback.fst f g) (X.affineCover.map i) ≅ pullback (X.affineCover.map i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.map i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.map i)
this : e.hom ≫ pullback.fst (X.affineCover.map i ≫ f) g = Scheme.Cover.pullbackHom X.affineCover (pullback.fst f g) i
⊢ Q 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
inst✝ : IsAffine S
H : Q g
this : Q.IsLocal := isLocal_affineProperty P
⊢ ∀ (i : X.affineCover.1), Q (Scheme.Cover.pullbackHom X.affineCover (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
inst✝ : IsAffine S
H : Q g
this : Q.IsLocal := isLocal_affineProperty P
i : X.affineCover.1
⊢ Q (Scheme.Cover.pullbackHom X.affineCover (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
inst✝ : IsAffine S
H : Q g
⊢ P (pullback.fst f g)

Tactic:
letI := isLocal_affineProperty P

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : IsAffine S
H : Q g
this : Q.IsLocal := isLocal_affineProperty P
⊢ P (pullback.fst f 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
inst✝ : IsAffine S
H : Q g
this : Q.IsLocal := isLocal_affineProperty P
i : X.affineCover.1
⊢ Q (Scheme.Cover.pullbackHom X.affineCover (pullback.fst f g) i)

Tactic:
let e := pullbackSymmetry _ _ ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.map i)

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : IsAffine S
H : Q g
this : Q.IsLocal := isLocal_affineProperty P
i : X.affineCover.1
e : pullback (pullback.fst f g) (X.affineCover.map i) ≅ pullback (X.affineCover.map i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.map i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.map i)
⊢ Q (Scheme.Cover.pullbackHom X.affineCover (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
inst✝ : IsAffine S
H : Q g
this : Q.IsLocal := isLocal_affineProperty P
i : X.affineCover.1
e : pullback (pullback.fst f g) (X.affineCover.map i) ≅ pullback (X.affineCover.map i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.map i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.map i)
⊢ Q (Scheme.Cover.pullbackHom X.affineCover (pullback.fst f g) i)

Tactic:
have : e.hom ≫ pullback.fst _ _ = X.affineCover.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
inst✝ : IsAffine S
H : Q g
this✝ : Q.IsLocal := isLocal_affineProperty P
i : X.affineCover.1
e : pullback (pullback.fst f g) (X.affineCover.map i) ≅ pullback (X.affineCover.map i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.map i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.map i)
this : e.hom ≫ pullback.fst (X.affineCover.map i ≫ f) g = Scheme.Cover.pullbackHom X.affineCover (pullback.fst f g) i
⊢ Q (Scheme.Cover.pullbackHom X.affineCover (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
inst✝ : IsAffine S
H : Q g
this✝ : Q.IsLocal := isLocal_affineProperty P
i : X.affineCover.1
e : pullback (pullback.fst f g) (X.affineCover.map i) ≅ pullback (X.affineCover.map i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.map i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.map i)
this : e.hom ≫ pullback.fst (X.affineCover.map i ≫ f) g = Scheme.Cover.pullbackHom X.affineCover (pullback.fst f g) i
⊢ Q g

Tactic:
exact H

Result:
no goals