awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
H₁ :
  ∀
    (this :
      ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g] (h : P' f)
        (hf : P (X := pullback f g) (pullback.fst f g)) (hZ : ∃ (R : CommRingCat.{u}), Z = Spec R), P g)
    (hZ : ¬∃ (R : CommRingCat.{u}), Z = Spec R), P g
wlog :
  ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g] (h : P' f)
    (hf : P (X := pullback f g) (pullback.fst f g)) (hZ : ∃ (R : CommRingCat.{u}), Z = Spec R), P g
⊢ P g

Tactic:
wlog hZ : ∃ R, Z = Spec R generalizing X Y Z
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g] (h : P' f)
    (hf : P (X := pullback f g) (pullback.fst f g)) (hZ : ∃ (R : CommRingCat.{u}), Z = Spec R), P g
hZ : ¬∃ (R : CommRingCat.{u}), Z = Spec R
H₁ :
  ∀ (i : Z.affineCover.toPreZeroHypercover.1),
    P (X := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Z.affineCover g i :
        (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i ⟶ Z.affineCover.X i)
⊢ P g

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

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g] (h : P' f)
    (hf : P (X := pullback f g) (pullback.fst f g)) (hZ : ∃ (R : CommRingCat.{u}), Z = Spec R), P g
hZ : ¬∃ (R : CommRingCat.{u}), Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
H₁ :
  P (X := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Z.affineCover g i :
      (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i ⟶ Z.affineCover.X i)
⊢ P (X := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Z.affineCover g i :
      (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i ⟶ Z.affineCover.X i)

Tactic:
let ι := Z.affineCover.f i
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g] (h : P' f)
    (hf : P (X := pullback f g) (pullback.fst f g)) (hZ : ∃ (R : CommRingCat.{u}), Z = Spec R), P g
hZ : ¬∃ (R : CommRingCat.{u}), Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
ι : Z.affineCover.X i ⟶ Z := Z.affineCover.f i
e : pullback (X := pullback f ι) (Y := pullback g ι) (pullback.snd f ι) (pullback.snd g ι) ≅
  pullback (X := pullback f g) (Y := pullback f ι) (pullback.fst f g) (pullback.fst f ι) :=
  pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
    Iso.trans (Y := pullback (Y := pullback g ι) f (pullback.fst g ι ≫ g)) (pullback.congrHom ⋯ ⋯)
      (Iso.trans (Y := pullback (X := pullback f g) (pullback.snd f g ≫ g) ι) (Iso.symm (pullbackAssoc f g g ι))
        (pullback.congrHom ⋯ ⋯ ≪≫ Iso.symm (pullbackRightPullbackFstIso f ι (pullback.fst f g))))
h₀ :
  (e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι)) ≫ pullback.fst f ι =
    pullback.fst (pullback.snd f ι) (pullback.snd g ι) ≫ pullback.fst f ι
h₁ :
  (e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι)) ≫ pullback.snd f ι =
    pullback.fst (pullback.snd f ι) (pullback.snd g ι) ≫ pullback.snd f ι
⊢ e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) = pullback.fst (pullback.snd f ι) (pullback.snd g ι)

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g] (h : P' f)
    (hf : P (X := pullback f g) (pullback.fst f g)) (hZ : ∃ (R : CommRingCat.{u}), Z = Spec R), P g
hZ : ¬∃ (R : CommRingCat.{u}), Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
ι : Z.affineCover.X i ⟶ Z := Z.affineCover.f i
e : pullback (X := pullback f ι) (Y := pullback g ι) (pullback.snd f ι) (pullback.snd g ι) ≅
  pullback (X := pullback f g) (Y := pullback f ι) (pullback.fst f g) (pullback.fst f ι) :=
  pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
    Iso.trans (Y := pullback (Y := pullback g ι) f (pullback.fst g ι ≫ g)) (pullback.congrHom ⋯ ⋯)
      (Iso.trans (Y := pullback (X := pullback f g) (pullback.snd f g ≫ g) ι) (Iso.symm (pullbackAssoc f g g ι))
        (pullback.congrHom ⋯ ⋯ ≪≫ Iso.symm (pullbackRightPullbackFstIso f ι (pullback.fst f g))))
⊢ (e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι)) ≫ pullback.fst f ι =
    pullback.fst (pullback.snd f ι) (pullback.snd g ι) ≫ pullback.fst f ι

Tactic:
simp [e, pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g] (h : P' f)
    (hf : P (X := pullback f g) (pullback.fst f g)) (hZ : ∃ (R : CommRingCat.{u}), Z = Spec R), P g
hZ : ¬∃ (R : CommRingCat.{u}), Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
ι : Z.affineCover.X i ⟶ Z := Z.affineCover.f i
e : pullback (X := pullback f ι) (Y := pullback g ι) (pullback.snd f ι) (pullback.snd g ι) ≅
  pullback (X := pullback f g) (Y := pullback f ι) (pullback.fst f g) (pullback.fst f ι) :=
  pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
    Iso.trans (Y := pullback (Y := pullback g ι) f (pullback.fst g ι ≫ g)) (pullback.congrHom ⋯ ⋯)
      (Iso.trans (Y := pullback (X := pullback f g) (pullback.snd f g ≫ g) ι) (Iso.symm (pullbackAssoc f g g ι))
        (pullback.congrHom ⋯ ⋯ ≪≫ Iso.symm (pullbackRightPullbackFstIso f ι (pullback.fst f g))))
⊢ (e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι)) ≫ pullback.snd f ι =
    pullback.fst (pullback.snd f ι) (pullback.snd g ι) ≫ pullback.snd f ι

Tactic:
simp [e, pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g] (h : P' f)
    (hf : P (X := pullback f g) (pullback.fst f g)) (hZ : ∃ (R : CommRingCat.{u}), Z = Spec R), P g
hZ : ¬∃ (R : CommRingCat.{u}), Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
ι : Z.affineCover.X i ⟶ Z := Z.affineCover.f i
e : pullback (X := pullback f ι) (Y := pullback g ι) (pullback.snd f ι) (pullback.snd g ι) ≅
  pullback (X := pullback f g) (Y := pullback f ι) (pullback.fst f g) (pullback.fst f ι) :=
  pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
    Iso.trans (Y := pullback (Y := pullback g ι) f (pullback.fst g ι ≫ g)) (pullback.congrHom ⋯ ⋯)
      (Iso.trans (Y := pullback (X := pullback f g) (pullback.snd f g ≫ g) ι) (Iso.symm (pullbackAssoc f g g ι))
        (pullback.congrHom ⋯ ⋯ ≪≫ Iso.symm (pullbackRightPullbackFstIso f ι (pullback.fst f g))))
⊢ e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) = pullback.fst (pullback.snd f ι) (pullback.snd g ι)

Tactic:
have heq : e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) =
        pullback.fst (pullback.snd f ι) (pullback.snd g ι) := by
      apply pullback.hom_ext <;> simp [e, pullback.condition]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g] (h : P' f)
    (hf : P (X := pullback f g) (pullback.fst f g)) (hZ : ∃ (R : CommRingCat.{u}), Z = Spec R), P g
hZ : ¬∃ (R : CommRingCat.{u}), Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
ι : Z.affineCover.X i ⟶ Z := Z.affineCover.f i
e : pullback (X := pullback f ι) (Y := pullback g ι) (pullback.snd f ι) (pullback.snd g ι) ≅
  pullback (X := pullback f g) (Y := pullback f ι) (pullback.fst f g) (pullback.fst f ι) :=
  pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
    Iso.trans (Y := pullback (Y := pullback g ι) f (pullback.fst g ι ≫ g)) (pullback.congrHom ⋯ ⋯)
      (Iso.trans (Y := pullback (X := pullback f g) (pullback.snd f g ≫ g) ι) (Iso.symm (pullbackAssoc f g g ι))
        (pullback.congrHom ⋯ ⋯ ≪≫ Iso.symm (pullbackRightPullbackFstIso f ι (pullback.fst f g))))
heq : e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) = pullback.fst (pullback.snd f ι) (pullback.snd g ι)
⊢ P (X := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Z.affineCover g i :
      (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i ⟶ Z.affineCover.X i)

Tactic:
this (f := pullback.snd f ι) ?_ ?_ ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g] (h : P' f)
    (hf : P (X := pullback f g) (pullback.fst f g)) (hZ : ∃ (R : CommRingCat.{u}), Z = Spec R), P g
hZ : ¬∃ (R : CommRingCat.{u}), Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
ι : Z.affineCover.X i ⟶ Z := Z.affineCover.f i
e : pullback (X := pullback f ι) (Y := pullback g ι) (pullback.snd f ι) (pullback.snd g ι) ≅
  pullback (X := pullback f g) (Y := pullback f ι) (pullback.fst f g) (pullback.fst f ι) :=
  pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
    Iso.trans (Y := pullback (Y := pullback g ι) f (pullback.fst g ι ≫ g)) (pullback.congrHom ⋯ ⋯)
      (Iso.trans (Y := pullback (X := pullback f g) (pullback.snd f g ≫ g) ι) (Iso.symm (pullbackAssoc f g g ι))
        (pullback.congrHom ⋯ ⋯ ≪≫ Iso.symm (pullbackRightPullbackFstIso f ι (pullback.fst f g))))
heq : e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) = pullback.fst (pullback.snd f ι) (pullback.snd g ι)
H₁ : P' (X := pullback f ι) (pullback.snd f ι)
H₂ :
  P (X :=
    pullback (X := pullback f ι) (Y := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i) (pullback.snd f ι)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Z.affineCover g i :
        (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i ⟶ Z.affineCover.X i))
    (pullback.fst (pullback.snd f ι) (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Z.affineCover g i) :
      pullback (X := pullback f ι) (Y := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i) (pullback.snd f ι)
          (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Z.affineCover g i :
            (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i ⟶ Z.affineCover.X i) ⟶
        pullback f ι)
⊢ P (X := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Z.affineCover g i :
      (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i ⟶ Z.affineCover.X i)

Tactic:
refine this (f := pullback.snd f ι) ?_ ?_ ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g] (h : P' f)
    (hf : P (X := pullback f g) (pullback.fst f g)) (hZ : ∃ (R : CommRingCat.{u}), Z = Spec R), P g
hZ : ¬∃ (R : CommRingCat.{u}), Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
ι : Z.affineCover.X i ⟶ Z := Z.affineCover.f i
e : pullback (X := pullback f ι) (Y := pullback g ι) (pullback.snd f ι) (pullback.snd g ι) ≅
  pullback (X := pullback f g) (Y := pullback f ι) (pullback.fst f g) (pullback.fst f ι) :=
  pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
    Iso.trans (Y := pullback (Y := pullback g ι) f (pullback.fst g ι ≫ g)) (pullback.congrHom ⋯ ⋯)
      (Iso.trans (Y := pullback (X := pullback f g) (pullback.snd f g ≫ g) ι) (Iso.symm (pullbackAssoc f g g ι))
        (pullback.congrHom ⋯ ⋯ ≪≫ Iso.symm (pullbackRightPullbackFstIso f ι (pullback.fst f g))))
heq : e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) = pullback.fst (pullback.snd f ι) (pullback.snd g ι)
⊢ P' (X := pullback f ι) (pullback.snd f ι)

Tactic:
P'.pullback_snd _ _ h

Premises used: CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g] (h : P' f)
    (hf : P (X := pullback f g) (pullback.fst f g)) (hZ : ∃ (R : CommRingCat.{u}), Z = Spec R), P g
hZ : ¬∃ (R : CommRingCat.{u}), Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
ι : Z.affineCover.X i ⟶ Z := Z.affineCover.f i
e : pullback (X := pullback f ι) (Y := pullback g ι) (pullback.snd f ι) (pullback.snd g ι) ≅
  pullback (X := pullback f g) (Y := pullback f ι) (pullback.fst f g) (pullback.fst f ι) :=
  pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
    Iso.trans (Y := pullback (Y := pullback g ι) f (pullback.fst g ι ≫ g)) (pullback.congrHom ⋯ ⋯)
      (Iso.trans (Y := pullback (X := pullback f g) (pullback.snd f g ≫ g) ι) (Iso.symm (pullbackAssoc f g g ι))
        (pullback.congrHom ⋯ ⋯ ≪≫ Iso.symm (pullbackRightPullbackFstIso f ι (pullback.fst f g))))
heq : e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) = pullback.fst (pullback.snd f ι) (pullback.snd g ι)
⊢ P' (X := pullback f ι) (pullback.snd f ι)

Tactic:
exact P'.pullback_snd _ _ h

Premises used: CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g] (h : P' f)
    (hf : P (X := pullback f g) (pullback.fst f g)) (hZ : ∃ (R : CommRingCat.{u}), Z = Spec R), P g
hZ : ¬∃ (R : CommRingCat.{u}), Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
ι : Z.affineCover.X i ⟶ Z := Z.affineCover.f i
e : pullback (X := pullback f ι) (Y := pullback g ι) (pullback.snd f ι) (pullback.snd g ι) ≅
  pullback (X := pullback f g) (Y := pullback f ι) (pullback.fst f g) (pullback.fst f ι) :=
  pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
    Iso.trans (Y := pullback (Y := pullback g ι) f (pullback.fst g ι ≫ g)) (pullback.congrHom ⋯ ⋯)
      (Iso.trans (Y := pullback (X := pullback f g) (pullback.snd f g ≫ g) ι) (Iso.symm (pullbackAssoc f g g ι))
        (pullback.congrHom ⋯ ⋯ ≪≫ Iso.symm (pullbackRightPullbackFstIso f ι (pullback.fst f g))))
heq : e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) = pullback.fst (pullback.snd f ι) (pullback.snd g ι)
H₁ :
  P (X := pullback (X := pullback f ι) (Y := pullback g ι) (pullback.snd f ι) (pullback.snd g ι))
    (pullback.fst (pullback.snd f ι) (pullback.snd g ι))
⊢ P (X :=
    pullback (X := pullback f ι) (Y := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i) (pullback.snd f ι)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Z.affineCover g i :
        (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i ⟶ Z.affineCover.X i))
    (pullback.fst (pullback.snd f ι) (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Z.affineCover g i) :
      pullback (X := pullback f ι) (Y := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i) (pullback.snd f ι)
          (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Z.affineCover g i :
            (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i ⟶ Z.affineCover.X i) ⟶
        pullback f ι)

Tactic:
change P (pullback.fst (pullback.snd f ι) (pullback.snd g ι))

Premises used: CategoryTheory.Limits.pullback.snd, CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g] (h : P' f)
    (hf : P (X := pullback f g) (pullback.fst f g)) (hZ : ∃ (R : CommRingCat.{u}), Z = Spec R), P g
hZ : ¬∃ (R : CommRingCat.{u}), Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
ι : Z.affineCover.X i ⟶ Z := Z.affineCover.f i
e : pullback (X := pullback f ι) (Y := pullback g ι) (pullback.snd f ι) (pullback.snd g ι) ≅
  pullback (X := pullback f g) (Y := pullback f ι) (pullback.fst f g) (pullback.fst f ι) :=
  pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
    Iso.trans (Y := pullback (Y := pullback g ι) f (pullback.fst g ι ≫ g)) (pullback.congrHom ⋯ ⋯)
      (Iso.trans (Y := pullback (X := pullback f g) (pullback.snd f g ≫ g) ι) (Iso.symm (pullbackAssoc f g g ι))
        (pullback.congrHom ⋯ ⋯ ≪≫ Iso.symm (pullbackRightPullbackFstIso f ι (pullback.fst f g))))
heq : e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) = pullback.fst (pullback.snd f ι) (pullback.snd g ι)
H₁ :
  P (X := pullback (X := pullback f g) (Y := pullback f ι) (pullback.fst f g) (pullback.fst f ι))
    (pullback.snd (pullback.fst f g) (pullback.fst f ι))
⊢ P (X := pullback (X := pullback f ι) (Y := pullback g ι) (pullback.snd f ι) (pullback.snd g ι))
    (pullback.fst (pullback.snd f ι) (pullback.snd g ι))

Tactic:
rw [← heq, P.cancel_left_of_respectsIso]

Premises used: CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g] (h : P' f)
    (hf : P (X := pullback f g) (pullback.fst f g)) (hZ : ∃ (R : CommRingCat.{u}), Z = Spec R), P g
hZ : ¬∃ (R : CommRingCat.{u}), Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
ι : Z.affineCover.X i ⟶ Z := Z.affineCover.f i
e : pullback (X := pullback f ι) (Y := pullback g ι) (pullback.snd f ι) (pullback.snd g ι) ≅
  pullback (X := pullback f g) (Y := pullback f ι) (pullback.fst f g) (pullback.fst f ι) :=
  pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
    Iso.trans (Y := pullback (Y := pullback g ι) f (pullback.fst g ι ≫ g)) (pullback.congrHom ⋯ ⋯)
      (Iso.trans (Y := pullback (X := pullback f g) (pullback.snd f g ≫ g) ι) (Iso.symm (pullbackAssoc f g g ι))
        (pullback.congrHom ⋯ ⋯ ≪≫ Iso.symm (pullbackRightPullbackFstIso f ι (pullback.fst f g))))
heq : e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) = pullback.fst (pullback.snd f ι) (pullback.snd g ι)
⊢ P (X := pullback (X := pullback f g) (Y := pullback f ι) (pullback.fst f g) (pullback.fst f ι))
    (pullback.snd (pullback.fst f g) (pullback.fst f ι))

Tactic:
AlgebraicGeometry.IsZariskiLocalAtTarget.of_isPullback (iY := pullback.fst f ι)
        (CategoryTheory.IsPullback.of_hasPullback _ _) hf

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.of_isPullback, CategoryTheory.IsPullback.of_hasPullback