awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) (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).ι)

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 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 ⋯)) ≫
      ((↑i : X.Opens) ⊓ (↑j : 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.snd (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      ((↑i : X.Opens) ⊓ (↑j : 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.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 ⋯)

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 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 ⋯)) ≫
      ((↑i : X.Opens) ⊓ (↑j : 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.snd (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      ((↑i : X.Opens) ⊓ (↑j : 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)
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 ⋯)
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.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.snd (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.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 ⋯))

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.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).ι
⊢ 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 ⋯)

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.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).ι)
⊢ ((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).ι

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.fst (I.glueDataObjι i) (X.homOfLE ⋯) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
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).ι)
h₃ 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 ⋯) ≫ ((↑i : X.Opens) ⊓ (↑j : 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).ι)

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

Premises used: AlgebraicGeometry.Scheme.homOfLE_ι, CategoryTheory.Limits.pullback.condition_assoc
-- 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.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))
            (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
        pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      ((↑i : X.Opens) ⊓ (↑k : 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.snd (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      ((↑i : X.Opens) ⊓ (↑k : 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.snd (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.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
      pullback.snd (I.glueDataObjι i) (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)
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.fst (I.glueDataObjι i) (X.homOfLE ⋯) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
    (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑k : 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.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))
            (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯))) ≫
        pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      ((↑i : X.Opens) ⊓ (↑k : 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.snd (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι

Tactic:
simp only [Category.assoc, limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app,
          glueDataT'Aux_snd_ι, limit.lift_π_assoc, cospan_left, glueDataT'Aux_fst_assoc,
          glueDataT_fst_assoc, Scheme.homOfLE_ι, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, _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'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.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.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι)
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.snd (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).ι)
    (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι)
h₃ 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.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι)
    (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑k : 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.fst (I.glueDataObjι i) (X.homOfLE ⋯) ≫ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
    (pullback.snd (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫
      pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) ≫ ((↑i : X.Opens) ⊓ (↑k : X.Opens)).ι)

Tactic:
rw [pullback.condition_assoc, pullback.condition_assoc, X.homOfLE_ι]

Premises used: AlgebraicGeometry.Scheme.homOfLE_ι, CategoryTheory.Limits.pullback.condition_assoc