awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
i : (↑X.affineOpens : Type u)
⊢ (I.glueDataT i i ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫ I.glueDataObjι i =
    (𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫ I.glueDataObjι i

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
i : (↑X.affineOpens : Type u)
⊢ I.glueDataT i i ≫ pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) =
    𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
⊢ Eq (α :=
    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 ⋯)) ⟶
      I.glueDataObj j)
    (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯ ≫ pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
    (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯ ≫ pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 ⋯)
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.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 ⋯)
⊢ 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

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 ⋯)) ≫
      I.glueDataObjι (j, i).1 =
    ((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 ⋯)) ≫
      I.glueDataObjι (j, i).1
⊢ 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 ⋯)

Tactic:
rw [← cancel_mono (glueDataObjι _ _)]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι, CategoryTheory.cancel_mono
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 ⋯)) ≫
      I.glueDataObjι (j, i).1 =
    ((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 ⋯)) ≫
      I.glueDataObjι (j, i).1

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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.snd (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)) ≫
      ((↑(j, i).1 : X.Opens) ⊓ (↑(j, i).2 : X.Opens)).ι =
    ((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 ⋯)) ≫
      ((↑(j, i).1 : X.Opens) ⊓ (↑(j, i).2 : X.Opens)).ι
⊢ 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 ⋯)

Tactic:
rw [← cancel_mono (Scheme.Opens.ι _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 ⋯)) ≫
      ((↑(j, i).1 : X.Opens) ⊓ (↑(j, i).2 : X.Opens)).ι =
    ((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 ⋯)) ≫
      ((↑(j, i).1 : X.Opens) ⊓ (↑(j, i).2 : X.Opens)).ι

Tactic:
simp [pullback.condition_assoc]

Premises used: CategoryTheory.Limits.pullback.condition_assoc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
i j k : (↑X.affineOpens : Type u)
dsimp :
  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 ⋯)))
⊢ 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 ⋯)))

Tactic:
dsimp only
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 ⋯))
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 (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.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 ⋯)))

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 ⋯)
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.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 ⋯)
⊢ 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 ⋯))

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 ⋯)) ≫
        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).ι
⊢ 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 ⋯)

Tactic:
rw [← cancel_mono (glueDataObjι _ _), ← cancel_mono (Scheme.Opens.ι _)]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι, CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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).ι)
⊢ ((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).ι

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]

Premises used: CategoryTheory.Category.assoc, _private.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux_fst, _private.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataT_fst_assoc, CategoryTheory.Limits.PullbackCone.mk_π_app, _private.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux_snd_ι, AlgebraicGeometry.Scheme.homOfLE_ι, CategoryTheory.Limits.cospan_left, _private.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataT_fst, _private.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux_fst_assoc, CategoryTheory.Limits.PullbackCone.mk_pt, CategoryTheory.Limits.limit.lift_π_assoc, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (↑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.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).ι)

Tactic:
rw [pullback.condition_assoc (f := I.glueDataObjι i)]

Premises used: CategoryTheory.Limits.pullback.condition_assoc