awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
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 := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ 𝒰.X i)
    ((((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.fst (𝒰.f i ≫ f) g)
    ((pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.fst (𝒰.f i ≫ f) g)
⊢ Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ pullback (𝒰.f i ≫ f) g)
    (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k))
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k))
have h₂ : Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ Y)
  ((((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
    pullback.snd (𝒰.f i ≫ f) g)
  ((pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
    pullback.snd (𝒰.f i ≫ f) g)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
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 := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ 𝒰.X i)
    ((((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.fst (𝒰.f i ≫ f) g)
    ((pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.fst (𝒰.f i ≫ f) g)
have h₁ : Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ 𝒰.X i)
  (t' 𝒰 f g i j k ≫
    t' 𝒰 f g j k i ≫
      t' 𝒰 f g k i j ≫
        pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
          pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ≫ pullback.fst (𝒰.f i ≫ f) g)
  (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
    pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ≫ pullback.fst (𝒰.f i ≫ f) g)
Tactic: simp_rw [Category.assoc, cocycle_snd_fst_fst 𝒰 f g i j k]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
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 := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ Y)
    ((((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.snd (𝒰.f i ≫ f) g)
    ((pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k)) ≫
      pullback.snd (𝒰.f i ≫ f) g)
have h₁ : Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ Y)
  (t' 𝒰 f g i j k ≫
    t' 𝒰 f g j k i ≫
      t' 𝒰 f g k i j ≫
        pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
          pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ≫ pullback.snd (𝒰.f i ≫ f) g)
  (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
    pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k) ≫ pullback.snd (𝒰.f i ≫ f) g)
Tactic: simp_rw [Category.assoc, cocycle_snd_fst_snd 𝒰 f g i j k]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
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 := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ 𝒰.X k)
    (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k))
    (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k))
have h₁ : Eq (α := pullback (X := v 𝒰 f g i j) (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ 𝒰.X k)
  (t' 𝒰 f g i j k ≫
    t' 𝒰 f g j k i ≫
      t' 𝒰 f g k i j ≫
        pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k))
  (pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f k))
Tactic: simp_rw [Category.assoc, cocycle_snd_snd 𝒰 f g i j k]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
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)) ⟶
      match (motive := 𝒰.I₀ × 𝒰.I₀ → Scheme) (j, i) with
      | (i, j) => v 𝒰 f g i 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 (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)
have 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)) ⟶
    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: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
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)) ⟶
      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))
⊢ 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)) ⟶
      match (motive := 𝒰.I₀ × 𝒰.I₀ → Scheme) (j, i) with
      | (i, j) => v 𝒰 f g i 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 (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)
have 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 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: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
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)) ⟶
      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))
have 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)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
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)
⊢ 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))
have 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)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
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)) ⟶
      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))
have 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)
Tactic: on_goal 1 => apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
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)
⊢ 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))
have 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)
Tactic: on_goal 1 => apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
⊢ (gluing 𝒰 f g).glued ⟶ X
have 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)
Tactic: apply Multicoequalizer.desc (gluing 𝒰 f g).diagram _ fun i ↦ pullback.fst _ _ ≫ 𝒰.f i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
⊢ (gluing 𝒰 f g).glued ⟶ Y
have 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
Tactic: apply Multicoequalizer.desc _ _ fun i ↦ pullback.snd _ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
⊢ Eq (α := (gluing 𝒰 f g).glued ⟶ Z) (p1 𝒰 f g ≫ f) (p2 𝒰 f g ≫ g)
have 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
Tactic: apply Multicoequalizer.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
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₀
⊢ pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
    (gluing 𝒰 f g).V (i, j)
have refine : pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ s.fst) (𝒰.f j) ⟶ (gluing 𝒰 f g).V (i, j)
Tactic: refine (pullbackRightPullbackFstIso _ _ _).hom ≫ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
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₀
⊢ pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ s.fst) (𝒰.f j) ⟶ (gluing 𝒰 f g).V (i, j)
have refine_1 : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).X i ⟶ pullback (𝒰.f i ≫ f) g
Tactic: refine pullback.map _ _ _ _ ?_ (𝟙 _) (𝟙 _) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
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
⊢ pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ s.fst) (𝒰.f j) ⟶ (gluing 𝒰 f g).V (i, j)
have 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 sorry sorry)
    (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i)
Tactic: refine pullback.map _ _ _ _ ?_ (𝟙 _) (𝟙 _) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
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)
⊢ pullback ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ s.fst) (𝒰.f j) ⟶ (gluing 𝒰 f g).V (i, j)
have refine_3 : 𝒰.f j ≫ 𝟙 X = 𝟙 (𝒰.X j) ≫ 𝒰.f j
Tactic: refine pullback.map _ _ _ _ ?_ (𝟙 _) (𝟙 _) ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
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
⊢ s.pt ⟶ (gluing 𝒰 f g).glued
have f₁ : (x : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀) →
  (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).X x ⟶ (gluing 𝒰 f g).glued
Tactic: fapply Cover.glueMorphisms (𝒰.pullback₁ s.fst)