awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
⊢ HasPullback f g

Tactic:
⟨⟨⟨_, gluedIsLimit 𝒰 f g⟩⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk, AlgebraicGeometry.Scheme.Pullback.gluedIsLimit
-- 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
A B C : CommRingCat
f : Spec A ⟶ Spec C
g : Spec B ⟶ Spec C
rw : HasPullback (Scheme.Spec.map (Scheme.Spec.preimage f)) (Scheme.Spec.map (Scheme.Spec.preimage g))
⊢ HasPullback f g

Tactic:
rw [← Scheme.Spec.map_preimage f, ← Scheme.Spec.map_preimage g]

Premises used: AlgebraicGeometry.Scheme.Spec, CategoryTheory.Functor.map_preimage
-- 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
A B C : CommRingCat
f : Spec A ⟶ Spec C
g : Spec B ⟶ Spec C
⊢ HasPullback (Scheme.Spec.map (Scheme.Spec.preimage f)) (Scheme.Spec.map (Scheme.Spec.preimage g))

Tactic:
⟨⟨⟨_, isLimitOfHasPullbackOfPreservesLimit
    Scheme.Spec (Scheme.Spec.preimage f) (Scheme.Spec.preimage g)⟩⟩⟩

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.Limits.isLimitOfHasPullbackOfPreservesLimit, AlgebraicGeometry.Scheme.Spec, Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk
-- 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
A B C : CommRingCat
f : Spec A ⟶ Spec C
g : Spec B ⟶ Spec C
⊢ HasPullback (Scheme.Spec.map (Scheme.Spec.preimage f)) (Scheme.Spec.map (Scheme.Spec.preimage g))

Tactic:
exact ⟨⟨⟨_, isLimitOfHasPullbackOfPreservesLimit
    Scheme.Spec (Scheme.Spec.preimage f) (Scheme.Spec.preimage g)⟩⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
B C : CommRingCat
X : Scheme
f : X ⟶ Spec C
g : Spec B ⟶ Spec C
⊢ HasPullback f g

Tactic:
hasPullback_of_cover X.affineCover f g

Premises used: AlgebraicGeometry.Scheme.affineCover, AlgebraicGeometry.Scheme.Pullback.hasPullback_of_cover
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X_1 Y_1 Z : Scheme
𝒰 : X_1.OpenCover
f_1 : X_1 ⟶ Z
g_1 : Y_1 ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
C : CommRingCat
X Y : Scheme
f : X ⟶ Spec C
g : Y ⟶ Spec C
⊢ HasPullback f g

Tactic:
@hasPullback_symmetry _ _ _ _ _ _ _
    (@hasPullback_of_cover _ _ _ Y.affineCover g f fun _ =>
      @hasPullback_symmetry _ _ _ _ _ _ _ <| affine_affine_hasPullback _ _)

Premises used: CategoryTheory.Limits.hasPullback_symmetry
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X_1 Y_1 Z_1 : Scheme
𝒰 : X_1.OpenCover
f_1 : X_1 ⟶ Z_1
g_1 : Y_1 ⟶ Z_1
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
i : Z.affineCover.I₀
⊢ HasPullback ((Precoverage.ZeroHypercover.pullback₁ f Z.affineCover).f i ≫ f) g

Tactic:
simpa [pullback.condition] using
    hasPullback_assoc_symm f (Z.affineCover.f i) (Z.affineCover.f i) g

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.hasPullback_assoc_symm, CategoryTheory.Limits.pullback.condition, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X_1 Y_1 Z_1 : Scheme
𝒰 : X_1.OpenCover
f_1 : X_1 ⟶ Z_1
g_1 : Y_1 ⟶ Z_1
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
⊢ HasPullback f g

Tactic:
hasPullback_of_cover (Z.affineCover.pullback₁ f) f g

Premises used: CategoryTheory.Precoverage.ZeroHypercover.pullback₁, AlgebraicGeometry.Scheme.affineCover, AlgebraicGeometry.Scheme.Pullback.hasPullback_of_cover
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
⊢ HasPullbacks Scheme

Tactic:
hasPullbacks_of_hasLimit_cospan _

Premises used: CategoryTheory.Limits.hasPullbacks_of_hasLimit_cospan
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X_1 Y_1 Z_1 : Scheme
𝒰 : X_1.OpenCover
f_1 : X_1 ⟶ Z_1
g_1 : Y_1 ⟶ Z_1
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f_1) g_1
s : PullbackCone f_1 g_1
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsAffine X
inst_2 : IsAffine Y
inst_3 : IsAffine Z
⊢ IsAffine.{u_1} (pullback f g)

Tactic:
.of_isIso
    (pullback.map f g (Spec.map (Γ.map f.op)) (Spec.map (Γ.map g.op))
        X.toSpecΓ Y.toSpecΓ Z.toSpecΓ
        (Scheme.toSpecΓ_naturality f) (Scheme.toSpecΓ_naturality g) ≫
      (PreservesPullback.iso Scheme.Spec _ _).inv)

Premises used: AlgebraicGeometry.IsAffine.of_isIso, Quiver.Hom.op, AlgebraicGeometry.Scheme.toSpecΓ_naturality, AlgebraicGeometry.Scheme.Γ, CategoryTheory.Limits.PreservesPullback.iso, AlgebraicGeometry.Spec.map, AlgebraicGeometry.Scheme.Spec, CategoryTheory.Functor.map, CategoryTheory.Limits.pullback.map, AlgebraicGeometry.Scheme.toSpecΓ, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Pullbacks
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
H : Disjoint (α := Set ↥S) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥Y) ⇑g)
⊢ IsEmpty.{u + 1} ↥(pullback f g)

Tactic:
isEmpty_of_commSq (IsPullback.of_hasPullback f g).toCommSq H

Premises used: AlgebraicGeometry.Scheme.isEmpty_of_commSq, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.IsPullback.toCommSq
-- 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 : 𝒰.I₀
⊢ (𝒰.f i ≫ f) ≫ 𝟙 Z = 𝒰.f i ≫ 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} X
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g

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} X
f : X ⟶ Z
g : Y ⟶ Z
rw :
  (∀ (x : ↥(pullback f g)),
      ∃ (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) ⋯ ⋯ }),
        Membership.mem (γ := Set ↥(pullback f g))
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { 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) ⋯ ⋯ :
                  PreZeroHypercover.{v, u, u + 1} (pullback f g) }
                i))
            ⇑(PreZeroHypercover.f
                { 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) ⋯ ⋯ :
                  PreZeroHypercover.{v, u, u + 1} (pullback f g) }
                i))
          x) ∧
    ∀
      (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) ⋯ ⋯ }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { 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) ⋯ ⋯ :
            PreZeroHypercover.{v, u, u + 1} (pullback f g) }
          i)
⊢ Membership.mem (γ := Set (Presieve (pullback f g))) ((precoverage IsOpenImmersion).coverings (pullback f g))
    (PreZeroHypercover.presieve₀.{v, u, u + 1}
      { 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) ⋯ ⋯ })

Tactic:
rw [ofArrows_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.ofArrows_mem_precoverage_iff
-- 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
⊢ (∀ (x : ↥(pullback f g)),
      ∃ (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) ⋯ ⋯ }),
        Membership.mem (γ := Set ↥(pullback f g))
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { 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) ⋯ ⋯ :
                  PreZeroHypercover.{v, u, u + 1} (pullback f g) }
                i))
            ⇑(PreZeroHypercover.f
                { 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) ⋯ ⋯ :
                  PreZeroHypercover.{v, u, u + 1} (pullback f g) }
                i))
          x) ∧
    ∀
      (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) ⋯ ⋯ }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { 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) ⋯ ⋯ :
            PreZeroHypercover.{v, u, u + 1} (pullback f g) }
          i)

Tactic:
⟨fun x ↦ ?_, fun i ↦ ?_⟩

Premises used: And.intro
-- 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
x : ↥(pullback f g)
i : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g

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} X
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
i : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀
⊢ CategoryStruct.comp (Y := pullback f g)
      (pullback.map ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g f g ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i)
        (𝟙 Y) (𝟙 Z) ⋯ ⋯)
      (pullback.fst f g) =
    CategoryStruct.comp (Y := pullback f g)
      (Iso.hom (Iso.refl (pullback ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g)) ≫
        (gluing (Cover.ulift (P := IsOpenImmersion) 𝒰) f g).ι
            (Sigma.snd (β := fun (i : PUnit.{u + 1}) ↦ (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀)
              ((Equiv.trans (Equiv.symm (Equiv.punitProd (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀))
                    (Equiv.symm (Equiv.sigmaEquivProd PUnit.{u + 1} (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀)) :
                  (a : (Cover.ulift 𝒰).I₀) → (_ : PUnit.{u + 1}) × (Cover.ulift 𝒰).I₀)
                ((Equiv.refl (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀ : (a : (Cover.ulift 𝒰).I₀) → (Cover.ulift 𝒰).I₀)
                    i :
                  (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀))) ≫
          Iso.inv
            (limit.isoLimitCone
              {
                cone :=
                  PullbackCone.mk (W := (gluing (Cover.ulift (P := IsOpenImmersion) 𝒰) f g).glued)
                    (p1 (Cover.ulift (P := IsOpenImmersion) 𝒰) f g) (p2 (Cover.ulift (P := IsOpenImmersion) 𝒰) f g) ⋯,
                isLimit := gluedIsLimit (Cover.ulift (P := IsOpenImmersion) 𝒰) f g : LimitCone (cospan f g) }))
      (pullback.fst f g)

Tactic:
simp [p1]

Premises used: AlgebraicGeometry.Scheme.Pullback.p1
-- 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
x : ↥(pullback f g)
i : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀
⊢ CategoryStruct.comp (Y := pullback f g)
      (pullback.map ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g f g ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i)
        (𝟙 Y) (𝟙 Z) ⋯ ⋯)
      (pullback.snd f g) =
    CategoryStruct.comp (Y := pullback f g)
      (Iso.hom (Iso.refl (pullback ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g)) ≫
        (gluing (Cover.ulift (P := IsOpenImmersion) 𝒰) f g).ι
            (Sigma.snd (β := fun (i : PUnit.{u + 1}) ↦ (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀)
              ((Equiv.trans (Equiv.symm (Equiv.punitProd (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀))
                    (Equiv.symm (Equiv.sigmaEquivProd PUnit.{u + 1} (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀)) :
                  (a : (Cover.ulift 𝒰).I₀) → (_ : PUnit.{u + 1}) × (Cover.ulift 𝒰).I₀)
                ((Equiv.refl (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀ : (a : (Cover.ulift 𝒰).I₀) → (Cover.ulift 𝒰).I₀)
                    i :
                  (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀))) ≫
          Iso.inv
            (limit.isoLimitCone
              {
                cone :=
                  PullbackCone.mk (W := (gluing (Cover.ulift (P := IsOpenImmersion) 𝒰) f g).glued)
                    (p1 (Cover.ulift (P := IsOpenImmersion) 𝒰) f g) (p2 (Cover.ulift (P := IsOpenImmersion) 𝒰) f g) ⋯,
                isLimit := gluedIsLimit (Cover.ulift (P := IsOpenImmersion) 𝒰) f g : LimitCone (cospan f g) }))
      (pullback.snd f g)

Tactic:
simp [p2]

Premises used: AlgebraicGeometry.Scheme.Pullback.p2
-- 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
x : ↥(pullback f g)
i : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀
⊢ Eq (α := pullback ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g ⟶ limit (cospan f g))
    (pullback.map ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g f g ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i)
      (𝟙 Y) (𝟙 Z) ⋯ ⋯)
    (Iso.hom (Iso.refl (pullback ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g)) ≫
      (gluing (Cover.ulift (P := IsOpenImmersion) 𝒰) f g).ι
          (Sigma.snd (β := fun (i : PUnit.{u + 1}) ↦ (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀)
            ((Equiv.trans (Equiv.symm (Equiv.punitProd (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀))
                  (Equiv.symm (Equiv.sigmaEquivProd PUnit.{u + 1} (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀)) :
                (a : (Cover.ulift 𝒰).I₀) → (_ : PUnit.{u + 1}) × (Cover.ulift 𝒰).I₀)
              ((Equiv.refl (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀ : (a : (Cover.ulift 𝒰).I₀) → (Cover.ulift 𝒰).I₀)
                  i :
                (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀))) ≫
        Iso.inv
          (limit.isoLimitCone
            {
              cone :=
                PullbackCone.mk (W := (gluing (Cover.ulift (P := IsOpenImmersion) 𝒰) f g).glued)
                  (p1 (Cover.ulift (P := IsOpenImmersion) 𝒰) f g) (p2 (Cover.ulift (P := IsOpenImmersion) 𝒰) f g) ⋯,
              isLimit := gluedIsLimit (Cover.ulift (P := IsOpenImmersion) 𝒰) f g : LimitCone (cospan f g) }))

Tactic:
exact pullback.hom_ext (by simp [p1]) (by simp [p2])

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} X
f : X ⟶ Z
g : Y ⟶ Z
𝒱 : Cover (precoverage IsOpenImmersion) (limit (cospan f g)) :=
  Cover.copy (P := IsOpenImmersion)
    (Cover.pushforwardIso (P := IsOpenImmersion) (gluing (Cover.ulift (P := IsOpenImmersion) 𝒰) f g).openCover
      (Iso.inv
        (limit.isoLimitCone
          {
            cone :=
              PullbackCone.mk (W := (gluing (Cover.ulift (P := IsOpenImmersion) 𝒰) f g).glued)
                (p1 (Cover.ulift (P := IsOpenImmersion) 𝒰) f g) (p2 (Cover.ulift (P := IsOpenImmersion) 𝒰) f g) ⋯,
            isLimit := gluedIsLimit (Cover.ulift (P := IsOpenImmersion) 𝒰) f g : LimitCone (cospan f g) })))
    (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀
    (fun (i : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀) ↦ pullback ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g)
    (fun (i : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀) ↦
      pullback.map ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g f g ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i)
        (𝟙 Y) (𝟙 Z) ⋯ ⋯)
    (Equiv.refl (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀)
    (fun (x : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀) ↦
      Iso.refl
        ((fun (i : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀) ↦
            pullback ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g)
          x))
    ⋯
i : 𝒱.I₀
x : ↥(𝒱.X i)
⊢ ∃ (i_1 :
    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) ⋯ ⋯ }),
    Membership.mem (α := ↥(pullback f g)) (γ := Set ↥(pullback f g))
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { 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) ⋯ ⋯ :
              PreZeroHypercover.{v, u, u + 1} (pullback f g) }
            i_1))
        ⇑(PreZeroHypercover.f
            { 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) ⋯ ⋯ :
              PreZeroHypercover.{v, u, u + 1} (pullback f g) }
            i_1))
      ((𝒱.f i) x : ↥(limit (cospan f g)))

Tactic:
⟨_, x, rfl⟩

Premises used: Exists.intro, 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} X
f : X ⟶ Z
g : Y ⟶ Z
𝒱 : Cover (precoverage IsOpenImmersion) (limit (cospan f g)) :=
  Cover.copy (P := IsOpenImmersion)
    (Cover.pushforwardIso (P := IsOpenImmersion) (gluing (Cover.ulift (P := IsOpenImmersion) 𝒰) f g).openCover
      (Iso.inv
        (limit.isoLimitCone
          {
            cone :=
              PullbackCone.mk (W := (gluing (Cover.ulift (P := IsOpenImmersion) 𝒰) f g).glued)
                (p1 (Cover.ulift (P := IsOpenImmersion) 𝒰) f g) (p2 (Cover.ulift (P := IsOpenImmersion) 𝒰) f g) ⋯,
            isLimit := gluedIsLimit (Cover.ulift (P := IsOpenImmersion) 𝒰) f g : LimitCone (cospan f g) })))
    (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀
    (fun (i : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀) ↦ pullback ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g)
    (fun (i : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀) ↦
      pullback.map ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g f g ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i)
        (𝟙 Y) (𝟙 Z) ⋯ ⋯)
    (Equiv.refl (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀)
    (fun (x : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀) ↦
      Iso.refl
        ((fun (i : (Cover.ulift (P := IsOpenImmersion) 𝒰).I₀) ↦
            pullback ((Cover.ulift (P := IsOpenImmersion) 𝒰).f i ≫ f) g)
          x))
    ⋯
i : 𝒱.I₀
x : ↥(𝒱.X i)
⊢ ∃ (i_1 :
    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) ⋯ ⋯ }),
    Membership.mem (α := ↥(pullback f g)) (γ := Set ↥(pullback f g))
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { 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) ⋯ ⋯ :
              PreZeroHypercover.{v, u, u + 1} (pullback f g) }
            i_1))
        ⇑(PreZeroHypercover.f
            { 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) ⋯ ⋯ :
              PreZeroHypercover.{v, u, u + 1} (pullback f g) }
            i_1))
      ((𝒱.f i) x : ↥(limit (cospan f g)))

Tactic:
exact ⟨_, x, 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} 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) ⋯ ⋯ }
⊢ (𝒰.f i ≫ f) ≫ 𝟙 Z = 𝒰.f i ≫ 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} 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) ⋯ ⋯ }
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g

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} 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) ⋯ ⋯ }
⊢ 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)

Tactic:
aesop
-- 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) ⋯ ⋯ }
⊢ 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)

Tactic:
have : pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) (by simp) (by simp) =
        (pullbackSymmetry _ _).hom ≫ (pullbackLeftPullbackSndIso _ _ _).inv ≫
          pullback.fst _ _ ≫ (pullbackSymmetry _ _).hom := by aesop