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
i j k : 𝒰.I₀
h₀ :
  Eq (α :=
    pullback (X :=
        match (motive := 𝒰.I₀ × 𝒰.I₀ → Scheme) (i, j) with
        | (i, j) => v 𝒰 f g i j)
        (Y :=
        match (motive := 𝒰.I₀ × 𝒰.I₀ → Scheme) (i, k) with
        | (i, j) => v 𝒰 f g i j)
        (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
        (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ⟶
      𝒰.X j)
    (((t' 𝒰 f g i j k ≫
          pullback.snd (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k))
            (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)) ≫
      pullback.fst (𝒰.f j ≫ f) g)
    (((pullback.fst (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
            (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
          t 𝒰 f g i j) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)) ≫
      pullback.fst (𝒰.f j ≫ f) g)
h₁ :
  Eq (α :=
    pullback (X :=
        match (motive := 𝒰.I₀ × 𝒰.I₀ → Scheme) (i, j) with
        | (i, j) => v 𝒰 f g i j)
        (Y :=
        match (motive := 𝒰.I₀ × 𝒰.I₀ → Scheme) (i, k) with
        | (i, j) => v 𝒰 f g i j)
        (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
        (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ⟶
      Y)
    (((t' 𝒰 f g i j k ≫
          pullback.snd (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k))
            (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)) ≫
      pullback.snd (𝒰.f j ≫ f) g)
    (((pullback.fst (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
            (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
          t 𝒰 f g i j) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)) ≫
      pullback.snd (𝒰.f j ≫ f) g)
⊢ Eq (α :=
    pullback (X :=
        match (motive := 𝒰.I₀ × 𝒰.I₀ → Scheme) (i, j) with
        | (i, j) => v 𝒰 f g i j)
        (Y :=
        match (motive := 𝒰.I₀ × 𝒰.I₀ → Scheme) (i, k) with
        | (i, j) => v 𝒰 f g i j)
        (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
        (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ⟶
      pullback (𝒰.f j ≫ f) g)
    ((t' 𝒰 f g i j k ≫
        pullback.snd (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k))
          (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))) ≫
      pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
    ((pullback.fst (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
          (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
        t 𝒰 f g i j) ≫
      pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))

Tactic:
on_goal 1 => apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- 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
i j k : 𝒰.I₀
⊢ Eq (α :=
    pullback (X :=
        match (motive := 𝒰.I₀ × 𝒰.I₀ → Scheme) (i, j) with
        | (i, j) => v 𝒰 f g i j)
        (Y :=
        match (motive := 𝒰.I₀ × 𝒰.I₀ → Scheme) (i, k) with
        | (i, j) => v 𝒰 f g i j)
        (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
        (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ⟶
      𝒰.X j)
    (((t' 𝒰 f g i j k ≫
          pullback.snd (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k))
            (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)) ≫
      pullback.fst (𝒰.f j ≫ f) g)
    (((pullback.fst (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
            (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
          t 𝒰 f g i j) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)) ≫
      pullback.fst (𝒰.f j ≫ f) g)

Tactic:
simp only [t'_snd_fst_fst, t'_snd_fst_snd, t'_snd_snd, t_fst_fst, t_fst_snd, t_snd,
        Category.assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Pullback.t_snd, AlgebraicGeometry.Scheme.Pullback.t_fst_fst, AlgebraicGeometry.Scheme.Pullback.t'_snd_snd, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst, AlgebraicGeometry.Scheme.Pullback.t_fst_snd, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd
-- 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
i j k : 𝒰.I₀
⊢ Eq (α :=
    pullback (X :=
        match (motive := 𝒰.I₀ × 𝒰.I₀ → Scheme) (i, j) with
        | (i, j) => v 𝒰 f g i j)
        (Y :=
        match (motive := 𝒰.I₀ × 𝒰.I₀ → Scheme) (i, k) with
        | (i, j) => v 𝒰 f g i j)
        (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
        (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ⟶
      Y)
    (((t' 𝒰 f g i j k ≫
          pullback.snd (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k))
            (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)) ≫
      pullback.snd (𝒰.f j ≫ f) g)
    (((pullback.fst (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
            (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
          t 𝒰 f g i j) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)) ≫
      pullback.snd (𝒰.f j ≫ f) g)

Tactic:
simp only [t'_snd_fst_fst, t'_snd_fst_snd, t'_snd_snd, t_fst_fst, t_fst_snd, t_snd,
        Category.assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Pullback.t_snd, AlgebraicGeometry.Scheme.Pullback.t_fst_fst, AlgebraicGeometry.Scheme.Pullback.t'_snd_snd, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst, AlgebraicGeometry.Scheme.Pullback.t_fst_snd, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd
-- 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
i j k : 𝒰.I₀
⊢ Eq (α :=
    pullback (X :=
        match (motive := 𝒰.I₀ × 𝒰.I₀ → Scheme) (i, j) with
        | (i, j) => v 𝒰 f g i j)
        (Y :=
        match (motive := 𝒰.I₀ × 𝒰.I₀ → Scheme) (i, k) with
        | (i, j) => v 𝒰 f g i j)
        (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
        (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ⟶
      𝒰.X i)
    ((t' 𝒰 f g i j k ≫
        pullback.snd (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f k))
          (pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))) ≫
      pullback.snd (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
    ((pullback.fst (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
          (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
        t 𝒰 f g i j) ≫
      pullback.snd (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))

Tactic:
simp only [t'_snd_fst_fst, t'_snd_fst_snd, t'_snd_snd, t_fst_fst, t_fst_snd, t_snd,
        Category.assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Pullback.t_snd, AlgebraicGeometry.Scheme.Pullback.t_fst_fst, AlgebraicGeometry.Scheme.Pullback.t'_snd_snd, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst, AlgebraicGeometry.Scheme.Pullback.t_fst_snd, AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd
-- 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
j : 𝒰.I₀
⊢ Eq.{u + 1} (α := (gluing 𝒰 f g).U j ⟶ (gluing 𝒰 f g).glued) ((gluing 𝒰 f g).ι j)
    (Multicoequalizer.π (gluing 𝒰 f g).diagram j)

Tactic:
rfl

Premises used: CategoryTheory.GlueData.ι, rfl, CategoryTheory.Limits.colimit.ι
-- 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
apply :
  ∀ (a : (MultispanShape.prod (gluing 𝒰 f g).J).L),
    (gluing 𝒰 f g).diagram.fst a ≫
        pullback.fst (𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).fst a) ≫ f) g ≫
          𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).fst a) =
      (gluing 𝒰 f g).diagram.snd a ≫
        pullback.fst (𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).snd a) ≫ f) g ≫
          𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).snd a)
⊢ (gluing 𝒰 f g).glued ⟶ X

Tactic:
apply Multicoequalizer.desc (gluing 𝒰 f g).diagram _ fun i ↦ pullback.fst _ _ ≫ 𝒰.f i

Premises used: CategoryTheory.GlueData.diagram, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Pullback.gluing, CategoryTheory.Limits.Multicoequalizer.desc, CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.GlueData.toGlueData, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- 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
⊢ ∀ (a : (MultispanShape.prod (gluing 𝒰 f g).J).L),
    (gluing 𝒰 f g).diagram.fst a ≫
        pullback.fst (𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).fst a) ≫ f) g ≫
          𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).fst a) =
      (gluing 𝒰 f g).diagram.snd a ≫
        pullback.fst (𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).snd a) ≫ f) g ≫
          𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).snd a)

Tactic:
simp [t_fst_fst_assoc, ← pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition, AlgebraicGeometry.Scheme.Pullback.t_fst_fst_assoc
-- 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
apply :
  ∀ (a : (MultispanShape.prod (gluing 𝒰 f g).J).L),
    (gluing 𝒰 f g).diagram.fst a ≫ pullback.snd (𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).fst a) ≫ f) g =
      (gluing 𝒰 f g).diagram.snd a ≫ pullback.snd (𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).snd a) ≫ f) g
⊢ (gluing 𝒰 f g).glued ⟶ Y

Tactic:
apply Multicoequalizer.desc _ _ fun i ↦ pullback.snd _ _

Premises used: CategoryTheory.Limits.Multicoequalizer.desc
-- 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
⊢ ∀ (a : (MultispanShape.prod (gluing 𝒰 f g).J).L),
    (gluing 𝒰 f g).diagram.fst a ≫ pullback.snd (𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).fst a) ≫ f) g =
      (gluing 𝒰 f g).diagram.snd a ≫ pullback.snd (𝒰.f ((MultispanShape.prod (gluing 𝒰 f g).J).snd a) ≫ f) g

Tactic:
simp [t_fst_snd]

Premises used: AlgebraicGeometry.Scheme.Pullback.t_fst_snd
-- 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
h :
  ∀ (b : (MultispanShape.prod (gluing 𝒰 f g).J).R),
    Multicoequalizer.π (gluing 𝒰 f g).diagram b ≫ p1 𝒰 f g ≫ f =
      Multicoequalizer.π (gluing 𝒰 f g).diagram b ≫ p2 𝒰 f g ≫ g
⊢ Eq (α := (gluing 𝒰 f g).glued ⟶ Z) (p1 𝒰 f g ≫ f) (p2 𝒰 f g ≫ g)

Tactic:
apply Multicoequalizer.hom_ext

Premises used: CategoryTheory.Limits.Multicoequalizer.hom_ext
-- 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
⊢ ∀ (b : (MultispanShape.prod (gluing 𝒰 f g).J).R),
    Multicoequalizer.π (gluing 𝒰 f g).diagram b ≫ p1 𝒰 f g ≫ f =
      Multicoequalizer.π (gluing 𝒰 f g).diagram b ≫ p2 𝒰 f g ≫ g

Tactic:
simp [p1, p2, pullback.condition]

Premises used: AlgebraicGeometry.Scheme.Pullback.p2, CategoryTheory.Limits.pullback.condition, AlgebraicGeometry.Scheme.Pullback.p1
-- 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
i j : 𝒰.I₀
refine : pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ s.fst) (𝒰.f j) ⟶ (gluing 𝒰 f g).V (i, j)
⊢ pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
    (gluing 𝒰 f g).V (i, j)

Tactic:
refine (pullbackRightPullbackFstIso _ _ _).hom ≫ ?_

Premises used: CategoryTheory.Limits.pullbackRightPullbackFstIso, CategoryTheory.Iso.hom
-- 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
i j : 𝒰.I₀
refine_1 : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).X i ⟶ pullback (𝒰.f i ≫ f) g
refine_2 :
  ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ s.fst) ≫ 𝟙 X =
    CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫ pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯)
      (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i)
refine_3 : 𝒰.f j ≫ 𝟙 X = 𝟙 (𝒰.X j) ≫ 𝒰.f j
⊢ pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ s.fst) (𝒰.f j) ⟶ (gluing 𝒰 f g).V (i, j)

Tactic:
refine pullback.map _ _ _ _ ?_ (𝟙 _) (𝟙 _) ?_ ?_

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.pullback.map
-- 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
i j : 𝒰.I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).X i ⟶ pullback (𝒰.f i ≫ f) g

Tactic:
exact (pullbackSymmetry _ _).hom ≫
      pullback.map _ _ _ _ (𝟙 _) s.snd f (Category.id_comp _).symm s.condition

Premises used: CategoryTheory.Limits.pullbackSymmetry, CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.pullback.map, CategoryTheory.Limits.PullbackCone.snd, Eq.symm, CategoryTheory.Iso.hom, CategoryTheory.Category.id_comp
-- 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
i j : 𝒰.I₀
⊢ ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ s.fst) ≫ 𝟙 X =
    CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫ pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯)
      (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i)

Tactic:
simpa using pullback.condition

Premises used: CategoryTheory.Limits.pullback.condition
-- 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
i j : 𝒰.I₀
⊢ 𝒰.f j ≫ 𝟙 X = 𝟙 (𝒰.X j) ≫ 𝒰.f j

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
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i j : 𝒰.I₀
⊢ Eq (α :=
    pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
      pullback (𝒰.f i ≫ f) g)
    (gluedLiftPullbackMap 𝒰 f g s i j ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j))
    (pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫ pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯)

Tactic:
simp [gluedLiftPullbackMap]

Premises used: AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap
-- 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
i j : 𝒰.I₀
⊢ CategoryStruct.comp (Y := (gluing 𝒰 f g).V (i, j)) (gluedLiftPullbackMap 𝒰 f g s i j)
      (pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) =
    pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      pullback.snd s.fst (𝒰.f j)

Tactic:
simp [gluedLiftPullbackMap]

Premises used: AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap
-- 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
f₁ :
  (x : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀) →
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).X x ⟶ (gluing 𝒰 f g).glued
hf :
  ∀ (x y : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀),
    Eq (α :=
      pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f x)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f y) ⟶
        (gluing 𝒰 f g).glued)
      (pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f x)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f y) ≫
        Iso.hom (pullbackSymmetry s.fst (𝒰.f x)) ≫
          CategoryStruct.comp (Y := pullback (𝒰.f x ≫ f) g)
            (pullback.map (𝒰.f x) s.fst (𝒰.f x ≫ f) g (𝟙 (𝒰.X x)) s.snd f ⋯ ⋯) ((gluing 𝒰 f g).ι x))
      (pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f x)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f y) ≫
        Iso.hom (pullbackSymmetry s.fst (𝒰.f y)) ≫
          CategoryStruct.comp (Y := pullback (𝒰.f y ≫ f) g)
            (pullback.map (𝒰.f y) s.fst (𝒰.f y ≫ f) g (𝟙 (𝒰.X y)) s.snd f ⋯ ⋯) ((gluing 𝒰 f g).ι y))
⊢ s.pt ⟶ (gluing 𝒰 f g).glued

Tactic:
fapply Cover.glueMorphisms (𝒰.pullback₁ s.fst)

Premises used: CategoryTheory.Limits.PullbackCone.fst, AlgebraicGeometry.Scheme.Cover.glueMorphisms, CategoryTheory.Precoverage.ZeroHypercover.pullback₁
-- 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
⊢ (x : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀) →
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).X x ⟶ (gluing 𝒰 f g).glued

Tactic:
exact fun i ↦ (pullbackSymmetry _ _).hom ≫
      pullback.map _ _ _ _ (𝟙 _) s.snd f (Category.id_comp _).symm s.condition ≫ (gluing 𝒰 f g).ι i

Premises used: CategoryTheory.Limits.pullbackSymmetry, AlgebraicGeometry.Scheme.GlueData.ι, CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.PullbackCone.condition, AlgebraicGeometry.Scheme.Pullback.gluing, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.PreZeroHypercover.X, CategoryTheory.Limits.pullback.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.PullbackCone.snd, Eq.symm, CategoryTheory.Iso.hom, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, CategoryTheory.Category.id_comp
-- 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
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
hf :
  Eq (α :=
    pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
      (gluing 𝒰 f g).glued)
    (CategoryStruct.comp (Y := (gluing 𝒰 f g).V (i, j)) (gluedLiftPullbackMap 𝒰 f g s i j)
      (t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ (gluing 𝒰 f g).ι j))
    (pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫
        CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
          (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) ((gluing 𝒰 f g).ι j))
⊢ Eq (α :=
    pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
      (gluing 𝒰 f g).glued)
    (pullback.fst ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      Iso.hom (pullbackSymmetry s.fst (𝒰.f i)) ≫
        CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
          (pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯) ((gluing 𝒰 f g).ι i))
    (pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫
        CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
          (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) ((gluing 𝒰 f g).ι j))

Tactic:
rw [← gluedLiftPullbackMap_fst_assoc, ← gluing_f, ← (gluing 𝒰 f g).glue_condition i j,
    gluing_t, gluing_f]

Premises used: AlgebraicGeometry.Scheme.Pullback.gluing_t, AlgebraicGeometry.Scheme.Pullback.gluing, AlgebraicGeometry.Scheme.GlueData.glue_condition, AlgebraicGeometry.Scheme.Pullback.gluing_f, AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc
-- 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
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
hf :
  Eq (α :=
    pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
      (gluing 𝒰 f g).glued)
    (CategoryStruct.comp (Y := (gluing 𝒰 f g).U j)
      ((gluedLiftPullbackMap 𝒰 f g s i j ≫ t 𝒰 f g i j) ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
      ((gluing 𝒰 f g).ι j))
    (CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
      ((pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
            ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
          Iso.hom (pullbackSymmetry s.fst (𝒰.f j))) ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯)
      ((gluing 𝒰 f g).ι j))
⊢ Eq (α :=
    pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
      (gluing 𝒰 f g).glued)
    (CategoryStruct.comp (Y := (gluing 𝒰 f g).V (i, j)) (gluedLiftPullbackMap 𝒰 f g s i j)
      (t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ (gluing 𝒰 f g).ι j))
    (pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
      Iso.hom (pullbackSymmetry s.fst (𝒰.f j)) ≫
        CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
          (pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) ((gluing 𝒰 f g).ι j))

Tactic:
simp_rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
hf :
  Eq (α :=
    pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
      (gluing 𝒰 f g).U j)
    ((gluedLiftPullbackMap 𝒰 f g s i j ≫ t 𝒰 f g i j) ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
    ((pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
          ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
        Iso.hom (pullbackSymmetry s.fst (𝒰.f j))) ≫
      pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯)
⊢ Eq (α :=
    pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
      (gluing 𝒰 f g).glued)
    (CategoryStruct.comp (Y := (gluing 𝒰 f g).U j)
      ((gluedLiftPullbackMap 𝒰 f g s i j ≫ t 𝒰 f g i j) ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i))
      ((gluing 𝒰 f g).ι j))
    (CategoryStruct.comp (Y := pullback (𝒰.f j ≫ f) g)
      ((pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
            ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
          Iso.hom (pullbackSymmetry s.fst (𝒰.f j))) ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯)
      ((gluing 𝒰 f g).ι j))

Tactic:
congr 1