awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : CompactSpace.{u} ↥X
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
i : X.affineCover.finiteSubcover.I₀
x : ↥(X.affineCover.finiteSubcover.X i)
h : Eq (α := ↥X) ((Sigma.ι X.affineCover.finiteSubcover.X i ≫ p) x : ↥X) ((X.affineCover.finiteSubcover.f i) x : ↥X)
⊢ Eq (α := ↥X) (p ((Sigma.ι X.affineCover.finiteSubcover.X i) x : ↥(∐ X.affineCover.finiteSubcover.X)) : ↥X)
    ((X.affineCover.finiteSubcover.f i) x : ↥X)
have h₁ : Eq (α := ↥X) ((𝒰.f i) x : ↥X) ((X.affineCover.finiteSubcover.f i) x : ↥X)
Tactic: rw [← Scheme.Hom.comp_apply, Sigma.ι_desc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
Goal:
P : MorphismProperty Scheme
X : Scheme
inst : CompactSpace.{u} ↥X
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.ContainsIdentities
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
⊢ P p
have refine_2 : ∀
  (i :
    PreZeroHypercover.I₀ (S := ∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)
      (Precoverage.ZeroHypercover.toPreZeroHypercover (sigmaOpenCover fun (i : 𝒰.I₀) ↦ 𝒰.X i) :
        PreZeroHypercover (C := Scheme) (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i))),
  P (X :=
    PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (sigmaOpenCover fun (i : 𝒰.I₀) ↦ 𝒰.X i)) i)
    (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (sigmaOpenCover fun (i : 𝒰.I₀) ↦ 𝒰.X i)) i ≫
        p :
      PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (sigmaOpenCover fun (i : 𝒰.I₀) ↦ 𝒰.X i)) i ⟶
        X)
Tactic: rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (sigmaOpenCover _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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
⊢ P.DescendsAlong P'
have H₁ : ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g],
  P' f → P (X := pullback f g) (pullback.fst f g) → P g
Tactic: apply MorphismProperty.DescendsAlong.mk'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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)
⊢ P g
have 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
Tactic: wlog hZ : ∃ R, Z = Spec R generalizing X Y Z
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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
⊢ P g
have 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
Tactic: wlog hZ : ∃ R, Z = Spec R generalizing X Y Z
Cleared hypotheses: X, Y, Z, f, g, inst_2, h, hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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
⊢ P g
have 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)
Tactic: rw [IsZariskiLocalAtTarget.iff_of_openCover (P := P) Z.affineCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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 ι)
have 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 ι
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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 ι
⊢ e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) = pullback.fst (pullback.snd f ι) (pullback.snd g ι)
have 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 ι
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (hypothesis)
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))))
⊢ 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)
have heq : 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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)
have H₁ : P' (X := pullback f ι) (pullback.snd f ι)
Tactic: refine this (f := pullback.snd f ι) ?_ ?_ ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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 ι)
⊢ 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)
have 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 ι)
Tactic: refine this (f := pullback.snd f ι) ?_ ?_ ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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 ι) (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 ι)
have H₁ : P (X := pullback (X := pullback f ι) (Y := pullback g ι) (pullback.snd f ι) (pullback.snd g ι))
  (pullback.fst (pullback.snd f ι) (pullback.snd g ι))
Tactic: change P (pullback.fst (pullback.snd f ι) (pullback.snd g ι))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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 ι) (Y := pullback g ι) (pullback.snd f ι) (pullback.snd g ι))
    (pullback.fst (pullback.snd f ι) (pullback.snd g ι))
have 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 ι))
Tactic: rw [← heq, P.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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)
hZ : ∃ (R : CommRingCat.{u}), Z = Spec R
⊢ P g
have obtain : ∀ (R : CommRingCat.{u}) {f : X ⟶ Spec R} {g : Y ⟶ Spec R} [inst : HasPullback f g] (h : P' f)
  (hf : P (X := pullback f g) (pullback.fst f g)), P g
Tactic: obtain ⟨R, rfl⟩ := hZ
Cleared hypotheses: Z, f, g, inst_2, h, hf, hZ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : P.RespectsIso
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
f : Spec T ⟶ Spec R
g : Spec S ⟶ Spec R
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
⊢ P g
have obtain : ∀ (φ : R ⟶ S) (hf : P (X := pullback f (Spec.map φ)) (pullback.fst f (Spec.map φ))), P (Spec.map φ)
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective g
Cleared hypotheses: g, hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : P.RespectsIso
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
f : Spec T ⟶ Spec R
h : P' f
φ : R ⟶ S
hf : P (X := pullback f (Spec.map φ)) (pullback.fst f (Spec.map φ))
⊢ P (Spec.map φ)
have obtain : ∀ (ψ : R ⟶ T) (h : P' (Spec.map ψ))
  (hf : P (X := pullback (Spec.map ψ) (Spec.map φ)) (pullback.fst (Spec.map ψ) (Spec.map φ))), P (Spec.map φ)
Tactic: obtain ⟨ψ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, h, hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : P.RespectsIso
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
φ : R ⟶ S
ψ : R ⟶ T
h : P' (Spec.map ψ)
hf : P (X := pullback (Spec.map ψ) (Spec.map φ)) (pullback.fst (Spec.map ψ) (Spec.map φ))
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑T : Type u) := (CommRingCat.Hom.hom ψ).toAlgebra
⊢ P (Spec.map φ)
have replace : ∀
  (hf :
    P (X :=
      pullback (X := Spec (CommRingCat.of (↑T : Type u))) (Y := Spec (CommRingCat.of (↑S : Type u))) (Z :=
        Spec (CommRingCat.of (↑R : Type u))) (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
        (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
      (pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
        (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))),
  P (Spec.map φ)
Tactic: replace hf : P (pullback.fst (Spec.map <| CommRingCat.ofHom <| algebraMap R T)
    (Spec.map <| CommRingCat.ofHom <| algebraMap R S)) := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : P.RespectsIso
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
φ : R ⟶ S
ψ : R ⟶ T
h : P' (Spec.map ψ)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑T : Type u) := (CommRingCat.Hom.hom ψ).toAlgebra
hf :
  P (X :=
    pullback (X := Spec (CommRingCat.of (↑T : Type u))) (Y := Spec (CommRingCat.of (↑S : Type u))) (Z :=
      Spec (CommRingCat.of (↑R : Type u))) (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
    (pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
⊢ P (Spec.map φ)
have rw : Q (CommRingCat.Hom.hom φ)
Tactic: rw [H₂]