awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this : Q.IsLocal := ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : iSup U = ⊤
H : ∀ (i : ι), P (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover U hU
i : 𝒰.I₀
j :
  PreZeroHypercover.I₀ (C := Scheme) (S := 𝒰.X i)
    ((fun (i : 𝒰.I₀) ↦
        (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
            ((fun (j : 𝒰.I₀) ↦ ((𝒰.X j).affineCover : (𝒰.X j).OpenCover)) i) :
          PreZeroHypercover (𝒰.X i)))
      i)
⊢ U i = Scheme.Hom.opensRange (𝒰.f i)

Tactic:
exact (Scheme.Opens.opensRange_ι _).symm

Premises used: AlgebraicGeometry.Scheme.Opens.opensRange_ι, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
⊢ HasAffineProperty P Q ↔ IsZariskiLocalAtTarget P ∧ Q = of P

Tactic:
⟨fun _ ↦ ⟨inferInstance, ext fun _ _ _ ↦ iff_of_isAffine.symm⟩,
    fun ⟨_, e⟩ ↦ e ▸ of_isZariskiLocalAtTarget P⟩

Premises used: Eq.rec, inferInstance, AlgebraicGeometry.AffineTargetMorphismProperty.ext, And.intro, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine, Iff.intro, AlgebraicGeometry.HasAffineProperty, AlgebraicGeometry.HasAffineProperty.of_isZariskiLocalAtTarget, Eq.symm, Iff.symm, _private.0.AlgebraicGeometry.HasAffineProperty.iff.match_1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : IsAffine S
H : Q g
letI : P (X := pullback f g) (pullback.fst f g)
⊢ P (X := pullback f g) (pullback.fst f g)

Tactic:
letI := isLocal_affineProperty P
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : IsAffine S
H : Q g
this : Q.IsLocal := ⋯
rw :
  ∀ (i : X.affineCover.toPreZeroHypercover.1),
    Q (X :=
      PreZeroHypercover.X (S := pullback f g)
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Precoverage.ZeroHypercover.pullback₁ (pullback.fst f g) X.affineCover))
        i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover (pullback.fst f g) i :
        PreZeroHypercover.X (S := pullback f g)
            (Precoverage.ZeroHypercover.toPreZeroHypercover
              (Precoverage.ZeroHypercover.pullback₁ (pullback.fst f g) X.affineCover))
            i ⟶
          X.affineCover.X i)
⊢ P (X := pullback f g) (pullback.fst f g)

Tactic:
rw [iff_of_openCover (P := P) X.affineCover]

Premises used: AlgebraicGeometry.HasAffineProperty.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : IsAffine S
H : Q g
this : Q.IsLocal := ⋯
i : X.affineCover.toPreZeroHypercover.1
let :
  Q (X :=
    PreZeroHypercover.X (S := pullback f g)
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁ (pullback.fst f g) X.affineCover))
      i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover (pullback.fst f g) i :
      PreZeroHypercover.X (S := pullback f g)
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ (pullback.fst f g) X.affineCover))
          i ⟶
        X.affineCover.X i)
⊢ Q (X :=
    PreZeroHypercover.X (S := pullback f g)
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁ (pullback.fst f g) X.affineCover))
      i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover (pullback.fst f g) i :
      PreZeroHypercover.X (S := pullback f g)
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ (pullback.fst f g) X.affineCover))
          i ⟶
        X.affineCover.X i)

Tactic:
let e := pullbackSymmetry _ _ ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.f i)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : IsAffine S
H : Q g
this : Q.IsLocal := ⋯
i : X.affineCover.toPreZeroHypercover.1
e : pullback (X := pullback f g) (pullback.fst f g) (X.affineCover.f i) ≅ pullback (X.affineCover.f i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.f i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.f i)
⊢ e.hom ≫ pullback.fst (X.affineCover.f i ≫ f) g =
    Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover (pullback.fst f g) i

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

Premises used: AlgebraicGeometry.Scheme.Cover.pullbackHom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : IsAffine S
H : Q g
this : Q.IsLocal := ⋯
i : X.affineCover.toPreZeroHypercover.1
e : pullback (X := pullback f g) (pullback.fst f g) (X.affineCover.f i) ≅ pullback (X.affineCover.f i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.f i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.f i)
⊢ e.hom ≫ pullback.fst (X.affineCover.f i ≫ f) g =
    Scheme.Cover.pullbackHom (P := IsOpenImmersion) 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]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : IsAffine S
H : Q g
this_1 : Q.IsLocal := ⋯
i : X.affineCover.toPreZeroHypercover.1
e : pullback (X := pullback f g) (pullback.fst f g) (X.affineCover.f i) ≅ pullback (X.affineCover.f i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.f i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.f i)
this :
  e.hom ≫ pullback.fst (X.affineCover.f i ≫ f) g =
    Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover (pullback.fst f g) i
rw : Q (X := pullback (X.affineCover.f i ≫ f) g) (pullback.fst (X.affineCover.f i ≫ f) g)
⊢ Q (X :=
    PreZeroHypercover.X (S := pullback f g)
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁ (pullback.fst f g) X.affineCover))
      i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover (pullback.fst f g) i :
      PreZeroHypercover.X (S := pullback f g)
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ (pullback.fst f g) X.affineCover))
          i ⟶
        X.affineCover.X i)

Tactic:
rw [← this, Q.cancel_left_of_respectsIso]

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : IsAffine S
H : Q g
this_1 : Q.IsLocal := ⋯
i : X.affineCover.toPreZeroHypercover.1
e : pullback (X := pullback f g) (pullback.fst f g) (X.affineCover.f i) ≅ pullback (X.affineCover.f i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.f i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.f i)
this :
  e.hom ≫ pullback.fst (X.affineCover.f i ≫ f) g =
    Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover (pullback.fst f g) i
apply : Q g
⊢ Q (X := pullback (X.affineCover.f i ≫ f) g) (pullback.fst (X.affineCover.f i ≫ f) g)

Tactic:
apply hP' (.of_hasPullback _ _)

Premises used: CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : IsAffine S
H : Q g
this_1 : Q.IsLocal := ⋯
i : X.affineCover.toPreZeroHypercover.1
e : pullback (X := pullback f g) (pullback.fst f g) (X.affineCover.f i) ≅ pullback (X.affineCover.f i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.f i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.f i)
this :
  e.hom ≫ pullback.fst (X.affineCover.f i ≫ f) g =
    Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover (pullback.fst f g) i
⊢ Q g

Tactic:
H
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_1 : IsAffine S
H : Q g
this_1 : Q.IsLocal := ⋯
i : X.affineCover.toPreZeroHypercover.1
e : pullback (X := pullback f g) (pullback.fst f g) (X.affineCover.f i) ≅ pullback (X.affineCover.f i ≫ f) g :=
  pullbackSymmetry (pullback.fst f g) (X.affineCover.f i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.f i)
this :
  e.hom ≫ pullback.fst (X.affineCover.f i ≫ f) g =
    Scheme.Cover.pullbackHom (P := IsOpenImmersion) X.affineCover (pullback.fst f g) i
⊢ Q g

Tactic:
exact H
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h : HasPullback f g
H : P g
rw :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀),
    P (X :=
      pullback (X := pullback f g) (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))
      (pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))
⊢ P (X := pullback f g) (pullback.fst f g)

Tactic:
rw [P.iff_of_zeroHypercover_target (S.affineCover.pullback₁ f)]

Premises used: CategoryTheory.MorphismProperty.iff_of_zeroHypercover_target, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
refine :
  pullback ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) g ≅
    pullback (X := pullback f (S.affineCover.f i)) (pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i) g
⊢ pullback (X := pullback f g) (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≅
    pullback (X := pullback f (S.affineCover.f i)) (Y := pullback (S.affineCover.f i) g)
      (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g)

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

Premises used: CategoryTheory.Limits.pullbackSymmetry, CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.pullback.snd, CategoryTheory.Limits.pullbackRightPullbackFstIso, CategoryTheory.Iso.symm, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
⊢ ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) ≫ 𝟙 S =
    𝟙 ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i) ≫
      pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i

Tactic:
simpa using pullback.condition

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
⊢ g ≫ 𝟙 S = 𝟙 Y ≫ g

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
⊢ pullback ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) g ≅
    pullback (X := pullback f (S.affineCover.f i)) (pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i) g

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

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.pullback.map, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
let :
  P (X := pullback (X := pullback f g) (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))
    (pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))
⊢ P (X := pullback (X := pullback f g) (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))
    (pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))

Tactic:
let e : pullback (pullback.fst f g) ((S.affineCover.pullback₁ f).f i) ≅
          _ := by
        refine pullbackSymmetry _ _ ≪≫ pullbackRightPullbackFstIso f g _ ≪≫ ?_ ≪≫
          (pullbackRightPullbackFstIso (S.affineCover.f i) g
            (pullback.snd f (S.affineCover.f i))).symm
        exact asIso
          (pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) (by simpa using pullback.condition) (by simp))
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
e : pullback (X := pullback f g) (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≅
  pullback (X := pullback f (S.affineCover.f i)) (Y := pullback (S.affineCover.f i) g)
    (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) :=
  pullbackSymmetry (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
    pullbackRightPullbackFstIso f g ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
      asIso
          (pullback.map ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) g
            (pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i) g
            (𝟙 ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫
        Iso.symm (pullbackRightPullbackFstIso (S.affineCover.f i) g (pullback.snd f (S.affineCover.f i)))
⊢ e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) =
    pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i)

Tactic:
simp [e]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
e : pullback (X := pullback f g) (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≅
  pullback (X := pullback f (S.affineCover.f i)) (Y := pullback (S.affineCover.f i) g)
    (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) :=
  pullbackSymmetry (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
    pullbackRightPullbackFstIso f g ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
      asIso
          (pullback.map ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) g
            (pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i) g
            (𝟙 ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫
        Iso.symm (pullbackRightPullbackFstIso (S.affineCover.f i) g (pullback.snd f (S.affineCover.f i)))
⊢ e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) =
    pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i)

Tactic:
have : e.hom ≫ pullback.fst _ _ =
          pullback.snd (pullback.fst f g) ((S.affineCover.pullback₁ f).f i) := by
        simp [e]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
e : pullback (X := pullback f g) (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≅
  pullback (X := pullback f (S.affineCover.f i)) (Y := pullback (S.affineCover.f i) g)
    (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) :=
  pullbackSymmetry (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
    pullbackRightPullbackFstIso f g ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
      asIso
          (pullback.map ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) g
            (pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i) g
            (𝟙 ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫
        Iso.symm (pullbackRightPullbackFstIso (S.affineCover.f i) g (pullback.snd f (S.affineCover.f i)))
this :
  e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) =
    pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i)
rw :
  P (X :=
    pullback (X := pullback f (S.affineCover.f i)) (Y := pullback (S.affineCover.f i) g)
      (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g))
    (pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g))
⊢ P (X := pullback (X := pullback f g) (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))
    (pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))

Tactic:
rw [← this, P.cancel_left_of_respectsIso]

Premises used: CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
e : pullback (X := pullback f g) (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≅
  pullback (X := pullback f (S.affineCover.f i)) (Y := pullback (S.affineCover.f i) g)
    (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) :=
  pullbackSymmetry (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
    pullbackRightPullbackFstIso f g ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
      asIso
          (pullback.map ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) g
            (pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i) g
            (𝟙 ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫
        Iso.symm (pullbackRightPullbackFstIso (S.affineCover.f i) g (pullback.snd f (S.affineCover.f i)))
this :
  e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) =
    pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i)
H₁ : Q (X := pullback (S.affineCover.f i) g) (pullback.fst (S.affineCover.f i) g)
⊢ P (X :=
    pullback (X := pullback f (S.affineCover.f i)) (Y := pullback (S.affineCover.f i) g)
      (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g))
    (pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g))

Tactic:
apply HasAffineProperty.pullback_fst_of_right hP'

Premises used: _private.0.AlgebraicGeometry.HasAffineProperty.pullback_fst_of_right
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Basic
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
h : HasPullback f g
H : P g
i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀
e : pullback (X := pullback f g) (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≅
  pullback (X := pullback f (S.affineCover.f i)) (Y := pullback (S.affineCover.f i) g)
    (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) :=
  pullbackSymmetry (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
    pullbackRightPullbackFstIso f g ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i) ≪≫
      asIso
          (pullback.map ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i ≫ f) g
            (pullback.snd f (S.affineCover.f i) ≫ S.affineCover.f i) g
            (𝟙 ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i)) (𝟙 Y) (𝟙 S) ⋯ ⋯) ≪≫
        Iso.symm (pullbackRightPullbackFstIso (S.affineCover.f i) g (pullback.snd f (S.affineCover.f i)))
this :
  e.hom ≫ pullback.fst (pullback.snd f (S.affineCover.f i)) (pullback.fst (S.affineCover.f i) g) =
    pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i)
H₁ : Q (X := pullback (S.affineCover.f i) g) (pullback.fst (S.affineCover.f i) g)
⊢ Q (X := pullback (S.affineCover.f i) g) (pullback.fst (S.affineCover.f i) g)

Tactic:
letI := isLocal_affineProperty P