awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
⊢ CategoryStruct.comp (Y :=
        pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
          (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)))
        (pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
            pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯)
        (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) =
    (𝟙
          (pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
            (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
        pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)
have h₀ : ((CategoryStruct.comp (Y :=
          pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
            (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)))
          (pullback.lift (I.glueDataT'Aux i j k k sorry) (I.glueDataT'Aux i j k i sorry) sorry ≫
            pullback.lift (I.glueDataT'Aux j k i i sorry) (I.glueDataT'Aux j k i j sorry) sorry ≫
              pullback.lift (I.glueDataT'Aux k i j j sorry) (I.glueDataT'Aux k i j k sorry) sorry)
          (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))
            (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))) ≫
        pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
      I.glueDataObjι i) ≫
    (↑i : X.Opens).ι =
  (((𝟙
            (pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
              (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))) ≫
          pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))
            (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))) ≫
        pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
      I.glueDataObjι i) ≫
    (↑i : X.Opens).ι
Tactic: rw [← cancel_mono (glueDataObjι _ _), ← cancel_mono (Scheme.Opens.ι _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
⊢ ((CategoryStruct.comp (Y :=
            pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
              (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)))
            (pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
              pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
                pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯)
            (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))
              (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
          pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
        I.glueDataObjι i) ≫
      (↑i : X.Opens).ι =
    (((𝟙
              (pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
                (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
            pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))
              (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
          pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
        I.glueDataObjι i) ≫
      (↑i : X.Opens).ι
have h₀ : Eq (α :=
  pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
      (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ⟶
    X)
  (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.snd (I.glueDataObjι i) (X.homOfLE sorry) ≫ ((↑i : X.Opens) ⊓ (↑j : X.Opens)).ι)
  (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.fst (I.glueDataObjι i) (X.homOfLE sorry) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
Tactic: simp only [Category.assoc, limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app,
          glueDataT'Aux_fst, limit.lift_π_assoc, cospan_left, glueDataT_fst, Scheme.homOfLE_ι,
          glueDataT'Aux_snd_ι, glueDataT'Aux_fst_assoc, glueDataT_fst_assoc, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
⊢ Eq (α :=
    pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ⟶
      X)
    (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑j : X.Opens)).ι)
    (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
have h₀ : Eq (α :=
  pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
      (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ⟶
    X)
  (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.snd (I.glueDataObjι i) (X.homOfLE sorry) ≫ ((↑i : X.Opens) ⊓ (↑j : X.Opens)).ι)
  (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.snd (I.glueDataObjι i) (X.homOfLE sorry) ≫ X.homOfLE sorry ≫ (↑i : X.Opens).ι)
Tactic: rw [pullback.condition_assoc (f := I.glueDataObjι i)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
⊢ CategoryStruct.comp (Y :=
        pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
          (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)))
        (pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
            pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯)
        (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) =
    (𝟙
          (pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
            (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
        pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯)
have h₀ : (CategoryStruct.comp (Y :=
        pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
          (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)))
        (pullback.lift (I.glueDataT'Aux i j k k sorry) (I.glueDataT'Aux i j k i sorry) sorry ≫
          pullback.lift (I.glueDataT'Aux j k i i sorry) (I.glueDataT'Aux j k i j sorry) sorry ≫
            pullback.lift (I.glueDataT'Aux k i j j sorry) (I.glueDataT'Aux k i j k sorry) sorry)
        (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    ((↑i : X.Opens) ⊓ (↑j : X.Opens)).ι =
  ((𝟙
          (pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
            (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))) ≫
        pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    ((↑i : X.Opens) ⊓ (↑j : X.Opens)).ι
Tactic: rw [← cancel_mono (Scheme.Opens.ι _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
⊢ CategoryStruct.comp (Y :=
      pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)))
      (pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
        pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯)
      (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) =
    𝟙
        (pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
          (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))
have h₁ : CategoryStruct.comp (Y :=
      pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)))
      (pullback.lift (I.glueDataT'Aux i j k k sorry) (I.glueDataT'Aux i j k i sorry) sorry ≫
        pullback.lift (I.glueDataT'Aux j k i i sorry) (I.glueDataT'Aux j k i j sorry) sorry ≫
          pullback.lift (I.glueDataT'Aux k i j j sorry) (I.glueDataT'Aux k i j k sorry) sorry)
      (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))) ≫
    pullback.fst (I.glueDataObjι i) (X.homOfLE sorry) =
  (𝟙
        (pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
          (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))) ≫
      pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))) ≫
    pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
h₁ :
  CategoryStruct.comp (Y :=
        pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
          (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)))
        (pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
            pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯)
        (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) =
    (𝟙
          (pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
            (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
        pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)
⊢ CategoryStruct.comp (Y :=
      pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)))
      (pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
        pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯)
      (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) =
    𝟙
        (pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
          (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))
have h₂ : CategoryStruct.comp (Y :=
      pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)))
      (pullback.lift (I.glueDataT'Aux i j k k sorry) (I.glueDataT'Aux i j k i sorry) sorry ≫
        pullback.lift (I.glueDataT'Aux j k i i sorry) (I.glueDataT'Aux j k i j sorry) sorry ≫
          pullback.lift (I.glueDataT'Aux k i j j sorry) (I.glueDataT'Aux k i j k sorry) sorry)
      (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))) ≫
    pullback.snd (I.glueDataObjι i) (X.homOfLE sorry) =
  (𝟙
        (pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
          (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))) ≫
      pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))) ≫
    pullback.snd (I.glueDataObjι i) (X.homOfLE sorry)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
⊢ CategoryStruct.comp (Y :=
        pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
          (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)))
        (pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
          pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
            pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯)
        (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) =
    (𝟙
          (pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
            (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
        pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)
have h₁ : ((CategoryStruct.comp (Y :=
          pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
            (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)))
          (pullback.lift (I.glueDataT'Aux i j k k sorry) (I.glueDataT'Aux i j k i sorry) sorry ≫
            pullback.lift (I.glueDataT'Aux j k i i sorry) (I.glueDataT'Aux j k i j sorry) sorry ≫
              pullback.lift (I.glueDataT'Aux k i j j sorry) (I.glueDataT'Aux k i j k sorry) sorry)
          (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))
            (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))) ≫
        pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
      I.glueDataObjι i) ≫
    (↑i : X.Opens).ι =
  (((𝟙
            (pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
              (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))) ≫
          pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))
            (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry))) ≫
        pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
      I.glueDataObjι i) ≫
    (↑i : X.Opens).ι
Tactic: rw [← cancel_mono (glueDataObjι _ _), ← cancel_mono (Scheme.Opens.ι _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
⊢ ((CategoryStruct.comp (Y :=
            pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
              (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)))
            (pullback.lift (I.glueDataT'Aux i j k k ⋯) (I.glueDataT'Aux i j k i ⋯) ⋯ ≫
              pullback.lift (I.glueDataT'Aux j k i i ⋯) (I.glueDataT'Aux j k i j ⋯) ⋯ ≫
                pullback.lift (I.glueDataT'Aux k i j j ⋯) (I.glueDataT'Aux k i j k ⋯) ⋯)
            (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))
              (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
          pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
        I.glueDataObjι i) ≫
      (↑i : X.Opens).ι =
    (((𝟙
              (pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
                (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
            pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))
              (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
          pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
        I.glueDataObjι i) ≫
      (↑i : X.Opens).ι
have h₁ : Eq (α :=
  pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
      (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ⟶
    X)
  (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.snd (I.glueDataObjι i) (X.homOfLE sorry) ≫ ((↑i : X.Opens) ⊓ (↑j : X.Opens)).ι)
  (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.fst (I.glueDataObjι i) (X.homOfLE sorry) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
Tactic: simp only [Category.assoc, limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app,
          glueDataT'Aux_fst, limit.lift_π_assoc, cospan_left, glueDataT_fst, Scheme.homOfLE_ι,
          glueDataT'Aux_snd_ι, glueDataT'Aux_fst_assoc, glueDataT_fst_assoc, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
⊢ Eq (α :=
    pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ⟶
      X)
    (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑j : X.Opens)).ι)
    (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
have h₁ : Eq (α :=
  pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
      (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ⟶
    X)
  (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.snd (I.glueDataObjι i) (X.homOfLE sorry) ≫ ((↑i : X.Opens) ⊓ (↑j : X.Opens)).ι)
  (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.fst (I.glueDataObjι i) (X.homOfLE sorry) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
Tactic: rw [← pullback.condition_assoc, pullback.condition_assoc (f := I.glueDataObjι i),
          X.homOfLE_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
h₁ :
  Eq (α :=
    pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ⟶
      X)
    (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑j : X.Opens)).ι)
    (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
⊢ Eq (α :=
    pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ⟶
      X)
    (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑j : X.Opens)).ι)
    (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
have h₂ : Eq (α :=
  pullback (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
      (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ⟶
    X)
  (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.snd (I.glueDataObjι i) (X.homOfLE sorry) ≫ ((↑i : X.Opens) ⊓ (↑j : X.Opens)).ι)
  (pullback.fst (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫
    pullback.snd (I.glueDataObjι i) (X.homOfLE sorry) ≫ X.homOfLE sorry ≫ (↑i : X.Opens).ι)
Tactic: rw [← pullback.condition_assoc, pullback.condition_assoc (f := I.glueDataObjι i),
          X.homOfLE_ι]