awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰X : OpenCover.{v, u} X
𝒰Y : OpenCover.{w, u} Y
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰X.I₀
j : 𝒰Y.I₀
⊢ Eq (α := pullback (X := 𝒰X.X (i, j).1) (Y := 𝒰Y.X (i, j).2) (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) ⟶ pullback f g)
    (pullback.map (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) f g (𝒰X.f (i, j).1) (𝒰Y.f (i, j).2) (𝟙 Z) ⋯ ⋯ :
      pullback (X := 𝒰X.X (i, j).1) (Y := 𝒰Y.X (i, j).2) (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) ⟶ pullback f g)
    (Iso.hom
          (Iso.refl
            ((fun (ij : Prod.{v, w} 𝒰X.I₀ 𝒰Y.I₀) ↦
                pullback (X := 𝒰X.X ij.1) (Y := 𝒰Y.X ij.2) (𝒰X.f ij.1 ≫ f) (𝒰Y.f ij.2 ≫ g))
              (i, j))) ≫
        (Precoverage.ZeroHypercover.bind.{w, v, u, u + 1} (openCoverOfLeft 𝒰X f g)
              fun (x : (openCoverOfLeft 𝒰X f g).I₀) ↦ openCoverOfRight 𝒰Y (𝒰X.f x ≫ f) g).f
          ((Equiv.symm (Equiv.sigmaEquivProd 𝒰X.I₀ 𝒰Y.I₀) :
              (a : 𝒰X.I₀ × 𝒰Y.I₀) →
                (Precoverage.ZeroHypercover.bind (openCoverOfLeft 𝒰X f g) fun (x : (openCoverOfLeft 𝒰X f g).I₀) ↦
                    openCoverOfRight 𝒰Y (𝒰X.f x ≫ f) g).I₀)
            (i, j)) :
      pullback (X := 𝒰X.X (i, j).1) (Y := 𝒰Y.X (i, j).2) (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) ⟶ pullback f g)
have h₀ : Eq (α := pullback (X := 𝒰X.X (i, j).1) (Y := 𝒰Y.X (i, j).2) (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) ⟶ X)
  (CategoryStruct.comp (Y := pullback f g)
      (pullback.map (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) f g (𝒰X.f (i, j).1) (𝒰Y.f (i, j).2) (𝟙 Z) sorry sorry)
      (pullback.fst f g) :
    pullback (X := 𝒰X.X (i, j).1) (Y := 𝒰Y.X (i, j).2) (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) ⟶ X)
  (CategoryStruct.comp (Y := pullback f g)
      (Iso.hom
          (Iso.refl
            ((fun (ij : Prod.{v, w} 𝒰X.I₀ 𝒰Y.I₀) ↦
                pullback (X := 𝒰X.X ij.1) (Y := 𝒰Y.X ij.2) (𝒰X.f ij.1 ≫ f) (𝒰Y.f ij.2 ≫ g))
              (i, j))) ≫
        (Precoverage.ZeroHypercover.bind.{w, v, u, u + 1} (openCoverOfLeft 𝒰X f g)
              fun (x : (openCoverOfLeft 𝒰X f g).I₀) ↦ openCoverOfRight 𝒰Y (𝒰X.f x ≫ f) g).f
          ((Equiv.symm (Equiv.sigmaEquivProd 𝒰X.I₀ 𝒰Y.I₀) :
              (a : 𝒰X.I₀ × 𝒰Y.I₀) →
                (Precoverage.ZeroHypercover.bind (openCoverOfLeft 𝒰X f g) fun (x : (openCoverOfLeft 𝒰X f g).I₀) ↦
                    openCoverOfRight 𝒰Y (𝒰X.f x ≫ f) g).I₀)
            (i, j)))
      (pullback.fst f g) :
    pullback (X := 𝒰X.X (i, j).1) (Y := 𝒰Y.X (i, j).2) (𝒰X.f (i, j).1 ≫ f) (𝒰Y.f (i, j).2 ≫ g) ⟶ X)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰_1 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰_1.I₀), HasPullback (𝒰_1.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰 : OpenCover.{v, u} Z
f : X ⟶ Z
g : Y ⟶ Z
⊢ OpenCover.{v, u} (pullback f g)
have apply : (i : (openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).I₀) →
  Precoverage.ZeroHypercover.{v, u, u + 1} (precoverage IsOpenImmersion)
    ((openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).X i)
Tactic: apply (openCoverOfLeft (𝒰.pullback₁ f) f g).bind
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (hypothesis)
Goal:
X Y Z : Scheme
𝒰_1 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰_1.I₀), HasPullback (𝒰_1.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰 : OpenCover.{v, u} Z
f : X ⟶ Z
g : Y ⟶ Z
i : (openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).I₀
⊢ Precoverage.ZeroHypercover.{v, u, u + 1} (precoverage IsOpenImmersion)
    ((openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).X i)
have this : IsPullback (P :=
  pullback (X := pullback g (𝒰.f i)) (Y := pullback f (𝒰.f i)) (pullback.snd g (𝒰.f i)) (pullback.snd f (𝒰.f i)))
  (pullback.snd (pullback.snd g (𝒰.f i)) (pullback.snd f (𝒰.f i)))
  (pullback.fst (pullback.snd g (𝒰.f i)) (pullback.snd f (𝒰.f i)) ≫ pullback.fst g (𝒰.f i))
  (pullback.snd f (𝒰.f i) ≫ 𝒰.f i) g
Tactic: haveI := ((IsPullback.of_hasPullback (pullback.snd g (𝒰.f i))
    (pullback.snd f (𝒰.f i))).paste_horiz (IsPullback.of_hasPullback _ _)).flip
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰_1 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰_1.I₀), HasPullback (𝒰_1.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰 : OpenCover.{v, u} Z
f : X ⟶ Z
g : Y ⟶ Z
i : (openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).I₀
this :
  IsPullback (P :=
    pullback (X := pullback g (𝒰.f i)) (Y := pullback f (𝒰.f i)) (pullback.snd g (𝒰.f i)) (pullback.snd f (𝒰.f i)))
    (pullback.snd (pullback.snd g (𝒰.f i)) (pullback.snd f (𝒰.f i)))
    (pullback.fst (pullback.snd g (𝒰.f i)) (pullback.snd f (𝒰.f i)) ≫ pullback.fst g (𝒰.f i))
    (pullback.snd f (𝒰.f i) ≫ 𝒰.f i) g
⊢ Precoverage.ZeroHypercover.{v, u, u + 1} (precoverage IsOpenImmersion)
    ((openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).X i)
have refine_1 : (pullback.snd f (𝒰.f i) ≫ 𝒰.f i) ≫ 𝟙 Z = 𝟙 (pullback f (𝒰.f i)) ≫ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f
Tactic: refine
    @coverOfIsIso _ _ _ _ _
      (f := (pullbackSymmetry (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i))).hom ≫
        (limit.isoLimitCone ⟨_, this.isLimit⟩).inv ≫
        pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) ?_ ?_) inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰_1 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰_1.I₀), HasPullback (𝒰_1.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰 : OpenCover.{v, u} Z
f : X ⟶ Z
g : Y ⟶ Z
i : (openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).I₀
this :
  IsPullback (P :=
    pullback (X := pullback g (𝒰.f i)) (Y := pullback f (𝒰.f i)) (pullback.snd g (𝒰.f i)) (pullback.snd f (𝒰.f i)))
    (pullback.snd (pullback.snd g (𝒰.f i)) (pullback.snd f (𝒰.f i)))
    (pullback.fst (pullback.snd g (𝒰.f i)) (pullback.snd f (𝒰.f i)) ≫ pullback.fst g (𝒰.f i))
    (pullback.snd f (𝒰.f i) ≫ 𝒰.f i) g
refine_1 :
  (pullback.snd f (𝒰.f i) ≫ 𝒰.f i) ≫ 𝟙 Z = 𝟙 (pullback f (𝒰.f i)) ≫ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f
⊢ Precoverage.ZeroHypercover.{v, u, u + 1} (precoverage IsOpenImmersion)
    ((openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).X i)
have refine_2 : g ≫ 𝟙 Z = 𝟙 Y ≫ g
Tactic: refine
    @coverOfIsIso _ _ _ _ _
      (f := (pullbackSymmetry (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i))).hom ≫
        (limit.isoLimitCone ⟨_, this.isLimit⟩).inv ≫
        pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) ?_ ?_) inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰_1 : X.OpenCover
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
inst : ∀ (i : 𝒰_1.I₀), HasPullback (𝒰_1.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
𝒰 : OpenCover.{v, u} Z
f : X ⟶ Z
g : Y ⟶ Z
⊢ OpenCover.{v, u} (pullback f g)
have 𝒰₁ : ∀ (i : 𝒰.I₀),
  Eq (α :=
    pullback (X := pullback f (𝒰.f i)) (Y := pullback g (𝒰.f i)) (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) ⟶
      pullback f g)
    (pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) f g (pullback.fst f (𝒰.f i))
      (pullback.fst g (𝒰.f i)) (𝒰.f i) sorry sorry)
    (Iso.hom
        (Iso.refl
          ((fun (i : 𝒰.I₀) ↦
              pullback (X := pullback f (𝒰.f i)) (Y := pullback g (𝒰.f i)) (pullback.snd f (𝒰.f i))
                (pullback.snd g (𝒰.f i)))
            i)) ≫
      (openCoverOfBase' 𝒰 f g).f
        ((Equiv.trans (Equiv.symm (Equiv.prodPUnit 𝒰.I₀)) (Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1})) :
            (a : 𝒰.I₀) → (openCoverOfBase' 𝒰 f g).I₀)
          i))
Tactic: apply
    (openCoverOfBase' 𝒰 f g).copy 𝒰.I₀
      (fun i =>
        pullback (pullback.snd _ _ : pullback f (𝒰.f i) ⟶ _)
          (pullback.snd _ _ : pullback g (𝒰.f i) ⟶ _))
      (fun i =>
        pullback.map _ _ _ _ (pullback.fst _ _) (pullback.fst _ _) (𝒰.f i)
          pullback.condition.symm pullback.condition.symm)
      ((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit).symm) fun _ => Iso.refl _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (hypothesis)
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
⊢ IsPullback fWX fWY fXZ fYZ
have h : fWX ≫ fXZ = fWY ≫ fYZ
Tactic: have h : fWX ≫ fXZ = fWY ≫ fYZ :=
    Scheme.Cover.hom_ext (𝒰.pullback₁ fWX) _ _ fun i ↦ by simpa using (H i).w
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
⊢ IsPullback fWX fWY fXZ fYZ
have suffices : IsIso (Y := pullback fXZ fYZ) (pullback.lift fWX fWY h)
Tactic: suffices IsIso (lift fWX fWY h) from .of_iso_pullback ⟨h⟩ (asIso (lift _ _ h)) (by simp) (by simp)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (hypothesis)
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
⊢ IsIso (X := (Precoverage.ZeroHypercover.pullback₁ (pullback.lift fWX fWY h) (openCoverOfLeft 𝒰 fXZ fYZ)).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) (openCoverOfLeft 𝒰 fXZ fYZ) (pullback.lift fWX fWY h) i :
      (Precoverage.ZeroHypercover.pullback₁ (pullback.lift fWX fWY h) (openCoverOfLeft 𝒰 fXZ fYZ)).X i ⟶
        (openCoverOfLeft 𝒰 fXZ fYZ).X i)
have this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
Tactic: have : IsPullback (fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (fst _ _) := by
      simpa [← IsPullback.paste_vert_iff (.of_hasPullback _ _), f] using .of_hasPullback _ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ Eq (α := pullback fWX (𝒰.f i) ⟶ pullback fXZ fYZ) (pullback.fst fWX (𝒰.f i) ≫ pullback.lift fWX fWY h)
    (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯ ≫ f)
have h₀ : Eq (α := pullback fWX (𝒰.f i) ⟶ X)
  (CategoryStruct.comp (Y := pullback fXZ fYZ) (pullback.fst fWX (𝒰.f i) ≫ pullback.lift fWX fWY h)
    (pullback.fst fXZ fYZ))
  ((pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) sorry ≫ f) ≫ pullback.fst fXZ fYZ)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
h₀ :
  Eq (α := pullback fWX (𝒰.f i) ⟶ X)
    (CategoryStruct.comp (Y := pullback fXZ fYZ) (pullback.fst fWX (𝒰.f i) ≫ pullback.lift fWX fWY h)
      (pullback.fst fXZ fYZ))
    ((pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯ ≫ f) ≫ pullback.fst fXZ fYZ)
⊢ Eq (α := pullback fWX (𝒰.f i) ⟶ pullback fXZ fYZ) (pullback.fst fWX (𝒰.f i) ≫ pullback.lift fWX fWY h)
    (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯ ≫ f)
have h₁ : Eq (α := pullback fWX (𝒰.f i) ⟶ Y)
  (CategoryStruct.comp (Y := pullback fXZ fYZ) (pullback.fst fWX (𝒰.f i) ≫ pullback.lift fWX fWY h)
    (pullback.snd fXZ fYZ))
  ((pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) sorry ≫ f) ≫ pullback.snd fXZ fYZ)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ IsPullback (P := pullback fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i))
    (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯) (pullback.lift fWX fWY h) f
have rw : IsPullback (P := pullback fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i))
  (CategoryStruct.comp (Y := pullback (𝒰.f i ≫ fXZ) fYZ)
    (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) sorry) (pullback.fst (𝒰.f i ≫ fXZ) fYZ))
  (CategoryStruct.comp (Y := pullback fXZ fYZ) (pullback.lift fWX fWY h) (pullback.fst fXZ fYZ)) (𝒰.f i)
Tactic: rw [← IsPullback.paste_vert_iff this.flip (by ext <;> simp [f])]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (hypothesis)
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ IsIso (X := (Precoverage.ZeroHypercover.pullback₁ (pullback.lift fWX fWY h) (openCoverOfLeft 𝒰 fXZ fYZ)).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) (openCoverOfLeft 𝒰 fXZ fYZ) (pullback.lift fWX fWY h) i :
      (Precoverage.ZeroHypercover.pullback₁ (pullback.lift fWX fWY h) (openCoverOfLeft 𝒰 fXZ fYZ)).X i ⟶
        (openCoverOfLeft 𝒰 fXZ fYZ).X i)
have H' : IsPullback (P := pullback fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i))
  (pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) sorry) (pullback.lift fWX fWY h) f
Tactic: have H' : IsPullback (fst fWX (𝒰.f i)) (lift (snd _ _) (fst _ _ ≫ fWY) (by simp [← h]))
        (lift fWX fWY h) f := by
      rw [← IsPullback.paste_vert_iff this.flip (by ext <;> simp [f])]
      simpa using .of_hasPullback _ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (hypothesis)
Goal:
X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : OpenCover.{u_1, u} X
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 fWX i)
      ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
⊢ IsIso (Y := pullback fXZ fYZ) (pullback.lift fWX fWY h)
have H₁ : ∀ (i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1),
  IsIso (X := (Precoverage.ZeroHypercover.pullback₁ (pullback.lift fWX fWY h) (openCoverOfLeft 𝒰 fXZ fYZ)).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) (openCoverOfLeft 𝒰 fXZ fYZ) (pullback.lift fWX fWY h) i :
      (Precoverage.ZeroHypercover.pullback₁ (pullback.lift fWX fWY h) (openCoverOfLeft 𝒰 fXZ fYZ)).X i ⟶
        (openCoverOfLeft 𝒰 fXZ fYZ).X i)
Tactic: have H₁ (i : _) : IsIso ((openCoverOfLeft 𝒰 fXZ fYZ).pullbackHom (lift fWX fWY h) i) := by
    let f := map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) (by simp) (by simp)
    have : IsPullback (fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (fst _ _) := by
      simpa [← IsPullback.paste_vert_iff (.of_hasPullback _ _), f] using .of_hasPullback _ _
    have H' : IsPullback (fst fWX (𝒰.f i)) (lift (snd _ _) (fst _ _ ≫ fWY) (by simp [← h]))
        (lift fWX fWY h) f := by
      rw [← IsPullback.paste_vert_iff this.flip (by ext <;> simp [f])]
      simpa using .of_hasPullback _ _
    convert! (inferInstance : IsIso (H'.isoPullback.inv ≫ (H i).isoPullback.hom))
    aesop (add simp [Iso.eq_inv_comp, Scheme.Cover.pullbackHom])
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y S X' Y' S' : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst : IsOpenImmersion i₁
inst_1 : IsOpenImmersion i₂
inst_2 : Mono i₃
⊢ IsOpenImmersion (X := pullback f g) (Y := pullback f' g') (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)
have rw : IsOpenImmersion (X := pullback f g) (Y := pullback f' g')
  (CategoryStruct.comp (Y :=
      pullback (X := pullback (X := pullback f' g') (pullback.fst f' g') i₁) (Y :=
        pullback (X := pullback f' g') (pullback.snd f' g') i₂) (pullback.fst (pullback.fst f' g') i₁)
        (pullback.fst (pullback.snd f' g') i₂))
      (Iso.inv (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂) :
        pullback f g ⟶
          pullback (X := pullback (X := pullback f' g') (pullback.fst f' g') i₁) (Y :=
            pullback (X := pullback f' g') (pullback.snd f' g') i₂) (pullback.fst (pullback.fst f' g') i₁)
            (pullback.fst (pullback.snd f' g') i₂))
      (pullback.snd (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂) ≫
          pullback.fst (pullback.snd f' g') i₂ :
        pullback (X := pullback (X := pullback f' g') (pullback.fst f' g') i₁) (Y :=
            pullback (X := pullback f' g') (pullback.snd f' g') i₂) (pullback.fst (pullback.fst f' g') i₁)
            (pullback.fst (pullback.snd f' g') i₂) ⟶
          pullback f' g') :
    pullback f g ⟶ pullback f' g')
Tactic: rw [pullback_map_eq_pullbackFstFstIso_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
⊢ Eq (α :=
    pullback (X := Spec (of S)) (Y := Spec (of T)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R T))) ⟶
      Spec (of S))
    (Iso.hom (pullbackSpecIso R S T) ≫ Spec.map (ofHom includeLeftRingHom))
    (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
have rw : Eq (α :=
  pullback (X := Spec (of S)) (Y := Spec (of T)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
      (Spec.map (ofHom (algebraMap R T))) ⟶
    Spec (of S))
  (Iso.hom (pullbackSpecIso R S T) ≫
    Iso.inv (pullbackSpecIso R S T) ≫
      pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
  (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
Tactic: rw [← pullbackSpecIso_inv_fst, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
rw :
  Eq (α :=
    pullback (X := Spec (of S)) (Y := Spec (of T)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R T))) ⟶
      Spec (of S))
    (Iso.hom (pullbackSpecIso R S T) ≫
      Iso.inv (pullbackSpecIso R S T) ≫
        pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
    (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
⊢ Eq (α :=
    pullback (X := Spec (of S)) (Y := Spec (of T)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R T))) ⟶
      Spec (of S))
    (Iso.hom (pullbackSpecIso R S T) ≫ Spec.map (ofHom includeLeftRingHom))
    (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
have rw₁ : Eq (α :=
  pullback (X := Spec (of S)) (Y := Spec (of T)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
      (Spec.map (ofHom (algebraMap R T))) ⟶
    Spec (of S))
  (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
  (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
Tactic: rw [← pullbackSpecIso_inv_fst, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
⊢ Iso.hom (pullbackSpecIso R S T) ≫ Spec.map (ofHom (↑includeRight : T →+* S ⊗[R] T)) =
    pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T)))
have rw : Eq (α :=
  pullback (X := Spec (of S)) (Y := Spec (of T)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
      (Spec.map (ofHom (algebraMap R T))) ⟶
    Spec (of T))
  (Iso.hom (pullbackSpecIso R S T) ≫
    Iso.inv (pullbackSpecIso R S T) ≫
      pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
  (pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
Tactic: rw [← pullbackSpecIso_inv_snd, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
rw :
  Eq (α :=
    pullback (X := Spec (of S)) (Y := Spec (of T)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R T))) ⟶
      Spec (of T))
    (Iso.hom (pullbackSpecIso R S T) ≫
      Iso.inv (pullbackSpecIso R S T) ≫
        pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
    (pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
⊢ Iso.hom (pullbackSpecIso R S T) ≫ Spec.map (ofHom (↑includeRight : T →+* S ⊗[R] T)) =
    pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T)))
have rw₁ : Eq (α :=
  pullback (X := Spec (of S)) (Y := Spec (of T)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
      (Spec.map (ofHom (algebraMap R T))) ⟶
    Spec (of T))
  (pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
  (pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T))))
Tactic: rw [← pullbackSpecIso_inv_snd, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
A B C : CommRingCat
f : A ⟶ B
g : A ⟶ C
⊢ IsPullback (P := Spec (pushout f g)) (Spec.map (pushout.inl f g)) (Spec.map (pushout.inr f g)) (Spec.map f)
    (Spec.map g)
have h : IsPushout (P := pushout f g) f g (pushout.inl f g) (pushout.inr f g)
Tactic: apply isPullback_SpecMap_of_isPushout