awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V W U₀ : (↑X.affineOpens : Type u)
hU₀ : (↑U : X.Opens) ⊓ (↑W : X.Opens) ≤ (↑U₀ : X.Opens)
⊢ Set.range (ι :=
      ↥(pullback (X := pullback (I.glueDataObjι U) (X.homOfLE ⋯)) (Y := pullback (I.glueDataObjι U) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))))
      ⇑(pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
          pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueDataObjι U ≫ (↑U : X.Opens).ι) ⊆
    (↑(↑U₀ : X.Opens) : Set ↥X)
have right : Set.range (ι :=
    ↥(pullback (X := pullback (I.glueDataObjι U) (X.homOfLE sorry)) (Y := pullback (I.glueDataObjι U) (X.homOfLE sorry))
        (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry))))
    (Function.comp (β := ↥(↑((↑U : X.Opens) ⊓ (↑W : X.Opens)) : Scheme)) ⇑((↑U : X.Opens) ⊓ (↑W : X.Opens)).ι
      ⇑(pullback.snd (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) ≫
          pullback.snd (I.glueDataObjι U) (X.homOfLE sorry))) ⊆
  (↑(↑U₀ : X.Opens) : Set ↥X)
Tactic: rw [pullback.condition_assoc, pullback.condition_assoc, X.homOfLE_ι,
          ← Category.assoc, Scheme.Hom.comp_base, TopCat.coe_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V W U₀ : (↑X.affineOpens : Type u)
hU₀ : (↑U : X.Opens) ⊓ (↑W : X.Opens) ≤ (↑U₀ : X.Opens)
⊢ (pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
        I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) ≫
      I.glueDataObjι V =
    IsOpenImmersion.lift ((↑V : X.Opens) ⊓ (↑U₀ : X.Opens)).ι
        (pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
          pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueDataObjι U ≫ (↑U : X.Opens).ι)
        ⋯ ≫
      X.homOfLE ⋯
have rw : ((pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) ≫
        I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE sorry)) ≫
      I.glueDataObjι V) ≫
    (↑V : X.Opens).ι =
  (IsOpenImmersion.lift ((↑V : X.Opens) ⊓ (↑U₀ : X.Opens)).ι
        (pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) ≫
          pullback.fst (I.glueDataObjι U) (X.homOfLE sorry) ≫ I.glueDataObjι U ≫ (↑U : X.Opens).ι)
        sorry ≫
      X.homOfLE sorry) ≫
    (↑V : 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 : (↑X.affineOpens : Type u)
⊢ I.glueDataT i i = 𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2)
have h₀ : I.glueDataT i i ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE sorry) =
  𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ 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 : (↑X.affineOpens : Type u)
h₀ :
  I.glueDataT i i ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) =
    𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)
⊢ I.glueDataT i i = 𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2)
have h₁ : I.glueDataT i i ≫ pullback.snd (I.glueDataObjι i) (X.homOfLE sorry) =
  𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ 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 : (↑X.affineOpens : Type u)
⊢ I.glueDataT i i ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) =
    𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)
have h₀ : (I.glueDataT i i ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫ I.glueDataObjι i =
  (𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE sorry)) ≫ I.glueDataObjι i
Tactic: rw [← cancel_mono (glueDataObjι _ _)]
-- 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 (j, k).1 (j, k).2) (Y := I.glueDataObjPullback (j, i).1 (j, i).2)
        (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)))
      (pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
        (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯)
      (pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
        (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯))) =
    pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯))
        (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)) ≫
      I.glueDataT i j
have h₀ : CategoryStruct.comp (Y :=
      pullback (X := I.glueDataObjPullback (j, k).1 (j, k).2) (Y := I.glueDataObjPullback (j, i).1 (j, i).2)
        (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE sorry)))
      (pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 sorry)
        (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 sorry) sorry)
      (pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE sorry))
        (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE sorry))) ≫
    pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE sorry) =
  (pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE sorry))
        (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE sorry)) ≫
      I.glueDataT i j) ≫
    pullback.fst (I.glueDataObjι (j, i).1) (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 (j, k).1 (j, k).2) (Y := I.glueDataObjPullback (j, i).1 (j, i).2)
          (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)))
        (pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
          (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯)
        (pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯) =
    (pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)) ≫
        I.glueDataT i j) ≫
      pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)
⊢ CategoryStruct.comp (Y :=
      pullback (X := I.glueDataObjPullback (j, k).1 (j, k).2) (Y := I.glueDataObjPullback (j, i).1 (j, i).2)
        (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)))
      (pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
        (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯)
      (pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
        (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯))) =
    pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯))
        (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)) ≫
      I.glueDataT i j
have h₁ : CategoryStruct.comp (Y :=
      pullback (X := I.glueDataObjPullback (j, k).1 (j, k).2) (Y := I.glueDataObjPullback (j, i).1 (j, i).2)
        (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE sorry)))
      (pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 sorry)
        (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 sorry) sorry)
      (pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE sorry))
        (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE sorry))) ≫
    pullback.snd (I.glueDataObjι (j, i).1) (X.homOfLE sorry) =
  (pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE sorry))
        (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE sorry)) ≫
      I.glueDataT i j) ≫
    pullback.snd (I.glueDataObjι (j, i).1) (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 (j, k).1 (j, k).2) (Y := I.glueDataObjPullback (j, i).1 (j, i).2)
          (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)))
        (pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
          (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯)
        (pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯))) ≫
      pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯) =
    (pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)) ≫
        I.glueDataT i j) ≫
      pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)
have h₀ : (CategoryStruct.comp (Y :=
        pullback (X := I.glueDataObjPullback (j, k).1 (j, k).2) (Y := I.glueDataObjPullback (j, i).1 (j, i).2)
          (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE sorry)))
        (pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 sorry)
          (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 sorry) sorry)
        (pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE sorry))
          (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE sorry))) ≫
      pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE sorry)) ≫
    I.glueDataObjι (j, i).1 =
  ((pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE sorry))
          (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE sorry)) ≫
        I.glueDataT i j) ≫
      pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE sorry)) ≫
    I.glueDataObjι (j, i).1
Tactic: rw [← cancel_mono (glueDataObjι _ _)]
-- 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 (j, k).1 (j, k).2) (Y := I.glueDataObjPullback (j, i).1 (j, i).2)
          (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)))
        (pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
          (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯)
        (pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯))) ≫
      pullback.snd (I.glueDataObjι (j, i).1) (X.homOfLE ⋯) =
    (pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)) ≫
        I.glueDataT i j) ≫
      pullback.snd (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)
have h₁ : (CategoryStruct.comp (Y :=
        pullback (X := I.glueDataObjPullback (j, k).1 (j, k).2) (Y := I.glueDataObjPullback (j, i).1 (j, i).2)
          (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE sorry)))
        (pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 sorry)
          (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 sorry) sorry)
        (pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE sorry))
          (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE sorry))) ≫
      pullback.snd (I.glueDataObjι (j, i).1) (X.homOfLE sorry)) ≫
    ((↑(j, i).1 : X.Opens) ⊓ (↑(j, i).2 : X.Opens)).ι =
  ((pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE sorry))
          (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE sorry)) ≫
        I.glueDataT i j) ≫
      pullback.snd (I.glueDataObjι (j, i).1) (X.homOfLE sorry)) ≫
    ((↑(j, i).1 : X.Opens) ⊓ (↑(j, i).2 : 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)
⊢ pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
        (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯ ≫
      pullback.lift (I.glueDataT'Aux (j, k).1 (j, k).2 (j, i).2 (k, i).2 ⋯)
          (I.glueDataT'Aux (j, k).1 (j, k).2 (j, i).2 (k, j).2 ⋯) ⋯ ≫
        pullback.lift (I.glueDataT'Aux (k, i).1 (k, i).2 (k, j).2 (i, j).2 ⋯)
          (I.glueDataT'Aux (k, i).1 (k, i).2 (k, j).2 (i, k).2 ⋯) ⋯ =
    𝟙
      (pullback (X := I.glueDataObjPullback (i, j).1 (i, j).2) (Y := I.glueDataObjPullback (i, k).1 (i, k).2)
        (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)))
have dsimp : 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 (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)))
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
⊢ 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 (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (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 (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))
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.fst (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.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 (X := I.glueDataObjPullback i j) (Y := I.glueDataObjPullback i k)
        (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 (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))
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.fst (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 ⋯))
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) =
  (𝟙
        (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)
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.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 ⋯)
⊢ 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 (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 ⋯))
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) =
  (𝟙
        (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)
Tactic: apply pullback.hom_ext