awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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} X
f : X ⟶ Z
g : Y ⟶ Z
i :
  PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := pullback f g)
    { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
      f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }
this :
  Eq (α := pullback (𝒰.f i ≫ f) g ⟶ pullback f g)
    (pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ : pullback (𝒰.f i ≫ f) g ⟶ pullback f g)
    (Iso.hom (pullbackSymmetry (𝒰.f i ≫ f) g) ≫
        CategoryStruct.comp (Y := pullback (X := pullback g f) (pullback.snd g f) (𝒰.f i))
          (Iso.inv (pullbackLeftPullbackSndIso g f (𝒰.f i)))
          (pullback.fst (pullback.snd g f) (𝒰.f i) ≫ Iso.hom (pullbackSymmetry g f)) :
      pullback (𝒰.f i ≫ f) g ⟶ pullback f g)
refine_2 :
  IsOpenImmersion (X := pullback (𝒰.f i ≫ f) g) (Y := pullback f g)
    (Iso.hom (pullbackSymmetry (𝒰.f i ≫ f) g) ≫
        CategoryStruct.comp (Y := pullback (X := pullback g f) (pullback.snd g f) (𝒰.f i))
          (Iso.inv (pullbackLeftPullbackSndIso g f (𝒰.f i)))
          (pullback.fst (pullback.snd g f) (𝒰.f i) ≫ Iso.hom (pullbackSymmetry g f)) :
      pullback (𝒰.f i ≫ f) g ⟶ pullback f g)
⊢ IsOpenImmersion (X := pullback (𝒰.f i ≫ f) g) (Y := pullback f g)
    (pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯)

Tactic:
rw [this]
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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} X
f : X ⟶ Z
g : Y ⟶ Z
i :
  PreZeroHypercover.I₀.{v, u, u + 1} (C := Scheme) (S := pullback f g)
    { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ pullback (𝒰.f i ≫ f) g,
      f := fun (i : 𝒰.I₀) ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }
this :
  Eq (α := pullback (𝒰.f i ≫ f) g ⟶ pullback f g)
    (pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ : pullback (𝒰.f i ≫ f) g ⟶ pullback f g)
    (Iso.hom (pullbackSymmetry (𝒰.f i ≫ f) g) ≫
        CategoryStruct.comp (Y := pullback (X := pullback g f) (pullback.snd g f) (𝒰.f i))
          (Iso.inv (pullbackLeftPullbackSndIso g f (𝒰.f i)))
          (pullback.fst (pullback.snd g f) (𝒰.f i) ≫ Iso.hom (pullbackSymmetry g f)) :
      pullback (𝒰.f i ≫ f) g ⟶ pullback f g)
⊢ IsOpenImmersion (X := pullback (𝒰.f i ≫ f) g) (Y := pullback f g)
    (Iso.hom (pullbackSymmetry (𝒰.f i ≫ f) g) ≫
        CategoryStruct.comp (Y := pullback (X := pullback g f) (pullback.snd g f) (𝒰.f i))
          (Iso.inv (pullbackLeftPullbackSndIso g f (𝒰.f i)))
          (pullback.fst (pullback.snd g f) (𝒰.f i) ≫ Iso.hom (pullbackSymmetry g f)) :
      pullback (𝒰.f i ≫ f) g ⟶ pullback f g)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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} Y
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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} Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰₁ :
  ∀ (i : 𝒰.I₀),
    Eq (α := pullback f (𝒰.f i ≫ g) ⟶ pullback f g) (pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯)
      (Iso.hom (pullbackSymmetry f (𝒰.f i ≫ g)) ≫
        (Cover.pushforwardIso (P := IsOpenImmersion) (openCoverOfLeft 𝒰 g f) (Iso.hom (pullbackSymmetry g f))).f
          ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Cover.pushforwardIso (openCoverOfLeft 𝒰 g f) (pullbackSymmetry g f).hom).I₀)
            i))
⊢ OpenCover.{v, u} (pullback f g)

Tactic:
fapply
    ((openCoverOfLeft 𝒰 g f).pushforwardIso (pullbackSymmetry _ _).hom).copy 𝒰.I₀
      (fun i => pullback f (𝒰.f i ≫ g))
      (fun i => pullback.map _ _ _ _ (𝟙 _) (𝒰.f i) (𝟙 _) (by simp) (Category.comp_id _))
      (Equiv.refl _) fun i => pullbackSymmetry _ _

Premises used: CategoryTheory.Limits.pullbackSymmetry, CategoryTheory.Limits.pullback, CategoryTheory.PreZeroHypercover.f, CategoryTheory.CategoryStruct.id, AlgebraicGeometry.Scheme.Cover.copy, CategoryTheory.Category.comp_id, CategoryTheory.PreZeroHypercover.I₀, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft, CategoryTheory.Limits.pullback.map, AlgebraicGeometry.Scheme.Cover.pushforwardIso, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, Equiv.refl, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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} Y
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
dsimp :
  Eq (α := pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
    (pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯ : pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
    (Iso.hom (pullbackSymmetry f (𝒰.f i ≫ g)) ≫
        CategoryStruct.comp (Y := pullback g f) (pullback.map (𝒰.f i ≫ g) f g f (𝒰.f i) (𝟙 X) (𝟙 Z) ⋯ ⋯)
          (Iso.hom (pullbackSymmetry g f)) :
      pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
⊢ Eq (α := pullback f (𝒰.f i ≫ g) ⟶ pullback f g) (pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯)
    (Iso.hom (pullbackSymmetry f (𝒰.f i ≫ g)) ≫
      (Cover.pushforwardIso (P := IsOpenImmersion) (openCoverOfLeft 𝒰 g f) (Iso.hom (pullbackSymmetry g f))).f
        ((Equiv.refl 𝒰.I₀ : (a : 𝒰.I₀) → (Cover.pushforwardIso (openCoverOfLeft 𝒰 g f) (pullbackSymmetry g f).hom).I₀)
          i))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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} Y
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
h₀ :
  Eq (α := pullback f (𝒰.f i ≫ g) ⟶ X)
    (CategoryStruct.comp (Y := pullback f g) (pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯)
      (pullback.fst f g))
    (CategoryStruct.comp (Y := pullback f g)
      (Iso.hom (pullbackSymmetry f (𝒰.f i ≫ g)) ≫
          CategoryStruct.comp (Y := pullback g f) (pullback.map (𝒰.f i ≫ g) f g f (𝒰.f i) (𝟙 X) (𝟙 Z) ⋯ ⋯)
            (Iso.hom (pullbackSymmetry g f)) :
        pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
      (pullback.fst f g : pullback f g ⟶ X))
h₁ :
  Eq (α := pullback f (𝒰.f i ≫ g) ⟶ Y)
    (CategoryStruct.comp (Y := pullback f g) (pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯)
      (pullback.snd f g))
    (CategoryStruct.comp (Y := pullback f g)
      (Iso.hom (pullbackSymmetry f (𝒰.f i ≫ g)) ≫
          CategoryStruct.comp (Y := pullback g f) (pullback.map (𝒰.f i ≫ g) f g f (𝒰.f i) (𝟙 X) (𝟙 Z) ⋯ ⋯)
            (Iso.hom (pullbackSymmetry g f)) :
        pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
      (pullback.snd f g : pullback f g ⟶ Y))
⊢ Eq (α := pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
    (pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯ : pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
    (Iso.hom (pullbackSymmetry f (𝒰.f i ≫ g)) ≫
        CategoryStruct.comp (Y := pullback g f) (pullback.map (𝒰.f i ≫ g) f g f (𝒰.f i) (𝟙 X) (𝟙 Z) ⋯ ⋯)
          (Iso.hom (pullbackSymmetry g f)) :
      pullback f (𝒰.f i ≫ g) ⟶ pullback f g)

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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} Y
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ Eq (α := pullback f (𝒰.f i ≫ g) ⟶ X)
    (CategoryStruct.comp (Y := pullback f g) (pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯)
      (pullback.fst f g))
    (CategoryStruct.comp (Y := pullback f g)
      (Iso.hom (pullbackSymmetry f (𝒰.f i ≫ g)) ≫
          CategoryStruct.comp (Y := pullback g f) (pullback.map (𝒰.f i ≫ g) f g f (𝒰.f i) (𝟙 X) (𝟙 Z) ⋯ ⋯)
            (Iso.hom (pullbackSymmetry g f)) :
        pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
      (pullback.fst f g : pullback f g ⟶ X))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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} Y
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ Eq (α := pullback f (𝒰.f i ≫ g) ⟶ Y)
    (CategoryStruct.comp (Y := pullback f g) (pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯)
      (pullback.snd f g))
    (CategoryStruct.comp (Y := pullback f g)
      (Iso.hom (pullbackSymmetry f (𝒰.f i ≫ g)) ≫
          CategoryStruct.comp (Y := pullback g f) (pullback.map (𝒰.f i ≫ g) f g f (𝒰.f i) (𝟙 X) (𝟙 Z) ⋯ ⋯)
            (Iso.hom (pullbackSymmetry g f)) :
        pullback f (𝒰.f i ≫ g) ⟶ pullback f g)
      (pullback.snd f g : pullback f g ⟶ Y))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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
𝒰X₁ :
  ∀ (i : Prod.{v, w} 𝒰X.I₀ 𝒰Y.I₀),
    Eq (α := pullback (X := 𝒰X.X i.1) (Y := 𝒰Y.X i.2) (𝒰X.f i.1 ≫ f) (𝒰Y.f i.2 ≫ g) ⟶ pullback f g)
      (pullback.map (𝒰X.f i.1 ≫ f) (𝒰Y.f i.2 ≫ g) f g (𝒰X.f i.1) (𝒰Y.f i.2) (𝟙 Z) ⋯ ⋯ :
        pullback (X := 𝒰X.X i.1) (Y := 𝒰Y.X i.2) (𝒰X.f i.1 ≫ f) (𝒰Y.f i.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)) ≫
          (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) :
        pullback (X := 𝒰X.X i.1) (Y := 𝒰Y.X i.2) (𝒰X.f i.1 ≫ f) (𝒰Y.f i.2 ≫ g) ⟶ pullback f g)
⊢ (pullback f g).OpenCover

Tactic:
fapply
    Cover.copy ((openCoverOfLeft 𝒰X f g).bind fun x => openCoverOfRight 𝒰Y (𝒰X.f x ≫ f) g)
      (𝒰X.I₀ × 𝒰Y.I₀) (fun ij => pullback (𝒰X.f ij.1 ≫ f) (𝒰Y.f ij.2 ≫ g))
      (fun ij =>
        pullback.map _ _ _ _ (𝒰X.f ij.1) (𝒰Y.f ij.2) (𝟙 _) (Category.comp_id _)
          (Category.comp_id _))
      (Equiv.sigmaEquivProd _ _).symm fun _ => Iso.refl _

Premises used: CategoryTheory.Limits.pullback, CategoryTheory.PreZeroHypercover.f, CategoryTheory.CategoryStruct.id, CategoryTheory.Iso.refl, AlgebraicGeometry.Scheme.Cover.copy, CategoryTheory.Category.comp_id, CategoryTheory.PreZeroHypercover.I₀, Prod.fst, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft, CategoryTheory.Limits.pullback.map, CategoryTheory.CategoryStruct.comp, Equiv.symm, Prod, Prod.snd, AlgebraicGeometry.Scheme.Pullback.openCoverOfRight, CategoryTheory.Precoverage.ZeroHypercover.bind, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, Equiv.sigmaEquivProd
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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) ⟶ 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) ⋯ ⋯)
        (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:
simp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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) ⟶ Y)
    (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) ⋯ ⋯)
        (pullback.snd 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) ⟶ Y)
    (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.snd 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) ⟶ Y)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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
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)
⊢ OpenCover.{v, u} (pullback f g)

Tactic:
apply (openCoverOfLeft (𝒰.pullback₁ f) f g).bind

Premises used: AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, CategoryTheory.Precoverage.ZeroHypercover.bind
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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₀
⊢ 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
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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
refine_2 : g ≫ 𝟙 Z = 𝟙 Y ≫ g
⊢ Precoverage.ZeroHypercover.{v, u, u + 1} (precoverage IsOpenImmersion)
    ((openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).X i)

Tactic:
refine
    @coverOfIsIso _ _ _ _ _
      (f := (pullbackSymmetry (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i))).hom ≫
        (limit.isoLimitCone ⟨_, this.isLimit⟩).inv ≫
        pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) ?_ ?_) inferInstance

Premises used: CategoryTheory.Limits.pullbackSymmetry, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.coverOfIsIso, CategoryTheory.Limits.pullback.snd, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.limit.isoLimitCone, CategoryTheory.Limits.pullback.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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
⊢ (pullback.snd f (𝒰.f i) ≫ 𝒰.f i) ≫ 𝟙 Z = 𝟙 (pullback f (𝒰.f i)) ≫ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f

Tactic:
simp [← pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g

Tactic:
simp only [Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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 : 𝒰.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) ⋯ ⋯)
      (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))
⊢ OpenCover.{v, u} (pullback f g)

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 _

Premises used: CategoryTheory.Limits.pullback, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Pullback.openCoverOfBase', Equiv.trans, CategoryTheory.Limits.pullback.snd, CategoryTheory.Iso.refl, AlgebraicGeometry.Scheme.Cover.copy, CategoryTheory.PreZeroHypercover.I₀, CategoryTheory.Limits.pullback.map, PUnit, CategoryTheory.Limits.pullback.fst, Equiv.symm, CategoryTheory.Limits.pullback.condition, Eq.symm, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, Equiv.sigmaEquivProd, Equiv.prodPUnit
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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 : 𝒰.I₀
⊢ Eq (α :=
    pullback (X := pullback f (𝒰.f i)) (Y := pullback g (𝒰.f i)) (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) ⟶ X)
    (pullback.fst (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) ≫ pullback.fst f (𝒰.f i))
    (pullback.fst
        (pullback.snd f
          (𝒰.f
            (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
              ((Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}) :
                  (a : 𝒰.I₀ × PUnit.{v + 1}) → (openCoverOfBase' 𝒰 f g).I₀)
                (i, PUnit.unit)))))
        (pullback.snd g
          (𝒰.f
            (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
              ((Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}) :
                  (a : 𝒰.I₀ × PUnit.{v + 1}) → (openCoverOfBase' 𝒰 f g).I₀)
                (i, PUnit.unit))))) ≫
      pullback.fst f
        (𝒰.f
          (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
            ((Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}) :
                (a : 𝒰.I₀ × PUnit.{v + 1}) → (openCoverOfBase' 𝒰 f g).I₀)
              (i, PUnit.unit)))))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
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 : 𝒰.I₀
⊢ Eq (α :=
    pullback (X := pullback f (𝒰.f i)) (Y := pullback g (𝒰.f i)) (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) ⟶ Y)
    (pullback.snd (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) ≫ pullback.fst g (𝒰.f i))
    (pullback.snd
        (pullback.snd f
          (𝒰.f
            (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
              ((Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}) :
                  (a : 𝒰.I₀ × PUnit.{v + 1}) → (openCoverOfBase' 𝒰 f g).I₀)
                (i, PUnit.unit)))))
        (pullback.snd g
          (𝒰.f
            (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
              ((Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}) :
                  (a : 𝒰.I₀ × PUnit.{v + 1}) → (openCoverOfBase' 𝒰 f g).I₀)
                (i, PUnit.unit))))) ≫
      pullback.fst g
        (𝒰.f
          (Sigma.fst (β := fun (i : 𝒰.I₀) ↦ PUnit.{v + 1})
            ((Equiv.symm (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}) :
                (a : 𝒰.I₀ × PUnit.{v + 1}) → (openCoverOfBase' 𝒰 f g).I₀)
              (i, PUnit.unit)))))

Tactic:
rfl