awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ Eq (α :=
    pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
        (pullback.fst (𝒰.f x) (𝒰.f z)) ⟶
      𝒰.X y)
    (CategoryStruct.comp (Y :=
      pullback (X := pullback (𝒰.f y) (𝒰.f z)) (Y := pullback (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))
        (pullback.fst (𝒰.f y) (𝒰.f x)))
      (Iso.hom (pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))) ≫
          CategoryStruct.comp (Y :=
            pullback (X := pullback (𝒰.f y) (𝒰.f x)) (Y := pullback (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))
              (pullback.fst (𝒰.f y) (𝒰.f z)))
            (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
                (Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f y))) (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
              Iso.inv (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))))
            (Iso.hom (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z)))) :
        pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
            (pullback.fst (𝒰.f x) (𝒰.f z)) ⟶
          pullback (X := pullback (𝒰.f y) (𝒰.f z)) (Y := pullback (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))
            (pullback.fst (𝒰.f y) (𝒰.f x)))
      (pullback.fst (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.fst (𝒰.f y) (𝒰.f z) :
        pullback (X := pullback (𝒰.f y) (𝒰.f z)) (Y := pullback (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))
            (pullback.fst (𝒰.f y) (𝒰.f x)) ⟶
          𝒰.X y))
    (pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f y))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ Eq (α :=
    pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
        (pullback.fst (𝒰.f x) (𝒰.f z)) ⟶
      𝒰.X z)
    (CategoryStruct.comp (Y :=
      pullback (X := pullback (𝒰.f y) (𝒰.f z)) (Y := pullback (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))
        (pullback.fst (𝒰.f y) (𝒰.f x)))
      (Iso.hom (pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))) ≫
          CategoryStruct.comp (Y :=
            pullback (X := pullback (𝒰.f y) (𝒰.f x)) (Y := pullback (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))
              (pullback.fst (𝒰.f y) (𝒰.f z)))
            (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
                (Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f y))) (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
              Iso.inv (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))))
            (Iso.hom (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z)))) :
        pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
            (pullback.fst (𝒰.f x) (𝒰.f z)) ⟶
          pullback (X := pullback (𝒰.f y) (𝒰.f z)) (Y := pullback (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))
            (pullback.fst (𝒰.f y) (𝒰.f x)))
      (pullback.fst (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.snd (𝒰.f y) (𝒰.f z) :
        pullback (X := pullback (𝒰.f y) (𝒰.f z)) (Y := pullback (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))
            (pullback.fst (𝒰.f y) (𝒰.f x)) ⟶
          𝒰.X z))
    (pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f z))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ Eq (α :=
    pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
        (pullback.fst (𝒰.f x) (𝒰.f z)) ⟶
      𝒰.X y)
    (CategoryStruct.comp (Y :=
      pullback (X := pullback (𝒰.f y) (𝒰.f z)) (Y := pullback (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))
        (pullback.fst (𝒰.f y) (𝒰.f x)))
      (Iso.hom (pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))) ≫
          CategoryStruct.comp (Y :=
            pullback (X := pullback (𝒰.f y) (𝒰.f x)) (Y := pullback (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))
              (pullback.fst (𝒰.f y) (𝒰.f z)))
            (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
                (Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f y))) (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
              Iso.inv (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))))
            (Iso.hom (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z)))) :
        pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
            (pullback.fst (𝒰.f x) (𝒰.f z)) ⟶
          pullback (X := pullback (𝒰.f y) (𝒰.f z)) (Y := pullback (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))
            (pullback.fst (𝒰.f y) (𝒰.f x)))
      (pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.fst (𝒰.f y) (𝒰.f x) :
        pullback (X := pullback (𝒰.f y) (𝒰.f z)) (Y := pullback (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))
            (pullback.fst (𝒰.f y) (𝒰.f x)) ⟶
          𝒰.X y))
    (pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f y))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ Eq (α :=
    pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
        (pullback.fst (𝒰.f x) (𝒰.f z)) ⟶
      𝒰.X x)
    (CategoryStruct.comp (Y :=
      pullback (X := pullback (𝒰.f y) (𝒰.f z)) (Y := pullback (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))
        (pullback.fst (𝒰.f y) (𝒰.f x)))
      (Iso.hom (pullbackRightPullbackFstIso (𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f x) (𝒰.f y))) ≫
          CategoryStruct.comp (Y :=
            pullback (X := pullback (𝒰.f y) (𝒰.f x)) (Y := pullback (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))
              (pullback.fst (𝒰.f y) (𝒰.f z)))
            (pullback.map (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
                (Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f y))) (𝟙 (𝒰.X z)) (𝟙 X) ⋯ ⋯ ≫
              Iso.inv (pullbackRightPullbackFstIso (𝒰.f y) (𝒰.f z) (pullback.fst (𝒰.f y) (𝒰.f x))))
            (Iso.hom (pullbackSymmetry (pullback.fst (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z)))) :
        pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
            (pullback.fst (𝒰.f x) (𝒰.f z)) ⟶
          pullback (X := pullback (𝒰.f y) (𝒰.f z)) (Y := pullback (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))
            (pullback.fst (𝒰.f y) (𝒰.f x)))
      (pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) ≫ pullback.snd (𝒰.f y) (𝒰.f x) :
        pullback (X := pullback (𝒰.f y) (𝒰.f z)) (Y := pullback (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))
            (pullback.fst (𝒰.f y) (𝒰.f x)) ⟶
          𝒰.X x))
    (pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.fst (𝒰.f x) (𝒰.f y))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
h₀ :
  (gluedCoverT' 𝒰 x y z ≫
        gluedCoverT' 𝒰 y z x ≫
          gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.fst (𝒰.f x) (𝒰.f y) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.fst (𝒰.f x) (𝒰.f y)
h₁ :
  (gluedCoverT' 𝒰 x y z ≫
        gluedCoverT' 𝒰 y z x ≫
          gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.snd (𝒰.f x) (𝒰.f y) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f y)
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ (gluedCoverT' 𝒰 x y z ≫
        gluedCoverT' 𝒰 y z x ≫
          gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.fst (𝒰.f x) (𝒰.f y) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.fst (𝒰.f x) (𝒰.f y)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ (gluedCoverT' 𝒰 x y z ≫
        gluedCoverT' 𝒰 y z x ≫
          gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.snd (𝒰.f x) (𝒰.f y) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f y)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
h₀ :
  (gluedCoverT' 𝒰 x y z ≫
        gluedCoverT' 𝒰 y z x ≫
          gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.fst (𝒰.f x) (𝒰.f z) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.fst (𝒰.f x) (𝒰.f z)
h₁ :
  (gluedCoverT' 𝒰 x y z ≫
        gluedCoverT' 𝒰 y z x ≫
          gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.snd (𝒰.f x) (𝒰.f z) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f z)
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ (gluedCoverT' 𝒰 x y z ≫
        gluedCoverT' 𝒰 y z x ≫
          gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.fst (𝒰.f x) (𝒰.f z) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.fst (𝒰.f x) (𝒰.f z)

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ (gluedCoverT' 𝒰 x y z ≫
        gluedCoverT' 𝒰 y z x ≫
          gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.snd (𝒰.f x) (𝒰.f z) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f z)

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
h₀ :
  (gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y) ≫
      pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    𝟙
        (pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
          (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))
h₁ :
  (gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y) ≫
      pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    𝟙
        (pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
          (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))
⊢ gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y =
    𝟙
      (pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
        (pullback.fst (𝒰.f x) (𝒰.f z)))

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
h₀ :
  gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))
⊢ (gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y) ≫
      pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    𝟙
        (pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
          (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))

Tactic:
simp_rw [Category.id_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
h₁ :
  gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))
⊢ (gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y) ≫
      pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    𝟙
        (pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
          (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))

Tactic:
simp_rw [Category.id_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))

Tactic:
apply glued_cover_cocycle_fst

Premises used: AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_fst
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    pullback.snd (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))

Tactic:
apply glued_cover_cocycle_snd

Premises used: AlgebraicGeometry.Scheme.Cover.glued_cover_cocycle_snd
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x : 𝒰.I₀
⊢ Eq (α :=
    Quiver.Hom (V := Scheme)
      (match (motive := 𝒰.I₀ × 𝒰.I₀ → Scheme) (x, x) with
        | (x, y) => pullback (𝒰.f x) (𝒰.f y) :
        Scheme.{u})
      (match (motive := 𝒰.I₀ × 𝒰.I₀ → Scheme) (x, x) with
        | (x, y) => pullback (𝒰.f x) (𝒰.f y) :
        Scheme.{u}))
    (Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f x)))
    (𝟙
      (match (motive := 𝒰.I₀ × 𝒰.I₀ → Scheme) (x, x) with
      | (x, y) => pullback (𝒰.f x) (𝒰.f y)))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
h₀ :
  (gluedCoverT' 𝒰 x y z ≫ pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))) ≫
      pullback.fst (𝒰.f y) (𝒰.f x) =
    (pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫
        Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f y))) ≫
      pullback.fst (𝒰.f y) (𝒰.f x)
h₁ :
  (gluedCoverT' 𝒰 x y z ≫ pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))) ≫
      pullback.snd (𝒰.f y) (𝒰.f x) =
    (pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫
        Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f y))) ≫
      pullback.snd (𝒰.f y) (𝒰.f x)
⊢ gluedCoverT' 𝒰 x y z ≫ pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x)) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫
      Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f y))

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ (gluedCoverT' 𝒰 x y z ≫ pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))) ≫
      pullback.fst (𝒰.f y) (𝒰.f x) =
    (pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫
        Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f y))) ≫
      pullback.fst (𝒰.f y) (𝒰.f x)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ (gluedCoverT' 𝒰 x y z ≫ pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))) ≫
      pullback.snd (𝒰.f y) (𝒰.f x) =
    (pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫
        Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f y))) ≫
      pullback.snd (𝒰.f y) (𝒰.f x)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
k : (b : (MultispanShape.prod (gluedCover 𝒰).J).R) → (gluedCover 𝒰).diagram.right b ⟶ X
h :
  ∀ (a : (MultispanShape.prod (gluedCover 𝒰).J).L),
    (gluedCover 𝒰).diagram.fst a ≫ 𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).fst a) =
      (gluedCover 𝒰).diagram.snd a ≫ 𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).snd a)
⊢ (gluedCover 𝒰).glued ⟶ X

Tactic:
fapply Multicoequalizer.desc

Premises used: CategoryTheory.Limits.Multicoequalizer.desc
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
⊢ (b : (MultispanShape.prod (gluedCover 𝒰).J).R) → (gluedCover 𝒰).diagram.right b ⟶ X

Tactic:
exact fun x => 𝒰.f x

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y : (gluedCover 𝒰).J
h :
  Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ X)
    (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).fst (x, y)))
    ((Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f y)) ≫ pullback.fst (𝒰.f y) (𝒰.f x)) ≫
      𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).snd (x, y)))
⊢ Eq (α := (gluedCover 𝒰).diagram.left (x, y) ⟶ X)
    ((gluedCover 𝒰).diagram.fst (x, y) ≫ 𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).fst (x, y)))
    ((gluedCover 𝒰).diagram.snd (x, y) ≫ 𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).snd (x, y)))

Tactic:
change pullback.fst _ _ ≫ _ = ((pullbackSymmetry _ _).hom ≫ pullback.fst _ _) ≫ _

Premises used: CategoryTheory.Limits.pullbackSymmetry, CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y : (gluedCover 𝒰).J
⊢ Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ X)
    (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).fst (x, y)))
    ((Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f y)) ≫ pullback.fst (𝒰.f y) (𝒰.f x)) ≫
      𝒰.f ((MultispanShape.prod (gluedCover 𝒰).J).snd (x, y)))

Tactic:
simpa using pullback.condition

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x : 𝒰.I₀
⊢ (gluedCover 𝒰).ι x ≫ fromGlued 𝒰 = 𝒰.f x

Tactic:
Multicoequalizer.π_desc _ _ _ _ _

Premises used: CategoryTheory.Limits.Multicoequalizer.π_desc
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y : ↥(gluedCover 𝒰).glued
h : Eq (α := ↥X) ((fromGlued 𝒰) x : ↥X) ((fromGlued 𝒰) y : ↥X)
obtain :
  ∀ (i : (gluedCover 𝒰).J) (x : ↥((gluedCover 𝒰).U i))
    (h : Eq (α := ↥X) ((fromGlued 𝒰) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued) : ↥X) ((fromGlued 𝒰) y : ↥X)),
    ((gluedCover 𝒰).ι i) x = y
⊢ x = y

Tactic:
obtain ⟨i, x, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective x

Premises used: AlgebraicGeometry.Scheme.Cover.gluedCover, AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
y : ↥(gluedCover 𝒰).glued
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
h : Eq (α := ↥X) ((fromGlued 𝒰) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued) : ↥X) ((fromGlued 𝒰) y : ↥X)
obtain :
  ∀ (j : (gluedCover 𝒰).J) (y : ↥((gluedCover 𝒰).U j))
    (h :
      Eq (α := ↥X) ((fromGlued 𝒰) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued) : ↥X)
        ((fromGlued 𝒰) (((gluedCover 𝒰).ι j) y : ↥(gluedCover 𝒰).glued) : ↥X)),
    Eq (α := ↥(gluedCover 𝒰).glued) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued)
      (((gluedCover 𝒰).ι j) y : ↥(gluedCover 𝒰).glued)
⊢ ((gluedCover 𝒰).ι i) x = y

Tactic:
obtain ⟨j, y, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective y

Premises used: AlgebraicGeometry.Scheme.Cover.gluedCover, AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h :
  Eq (α := ↥X) ((fromGlued 𝒰) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued) : ↥X)
    ((fromGlued 𝒰) (((gluedCover 𝒰).ι j) y : ↥(gluedCover 𝒰).glued) : ↥X)
⊢ Eq (α := ↥X)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (((gluedCover 𝒰).ι i).base ≫ (fromGlued 𝒰).base) :
          (a : ↥((gluedCover 𝒰).U i)) → ↥X)
        x :
      ↥X)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (((gluedCover 𝒰).ι j).base ≫ (fromGlued 𝒰).base) :
          (a : ↥((gluedCover 𝒰).U j)) → ↥X)
        y :
      ↥X)

Tactic:
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply] at h

Premises used: CategoryTheory.ConcreteCategory.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : Eq (α := ↥X) (((gluedCover 𝒰).ι i ≫ fromGlued 𝒰) x : ↥X) (((gluedCover 𝒰).ι j ≫ fromGlued 𝒰) y : ↥X)
⊢ Eq (α := ↥X) ((𝒰.f i) x : ↥X) ((𝒰.f j) y : ↥X)

Tactic:
rw [ι_fromGlued, ι_fromGlued] at h

Premises used: AlgebraicGeometry.Scheme.Cover.ι_fromGlued
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : Eq (α := ↥X) ((𝒰.f i) x : ↥X) ((𝒰.f j) y : ↥X)
e : (TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt ≅
  (PullbackCone.mk (W := forgetToTop.obj (pullback (𝒰.f i) (𝒰.f j))) (forgetToTop.map (pullback.fst (𝒰.f i) (𝒰.f j)))
      (forgetToTop.map (pullback.snd (𝒰.f i) (𝒰.f j))) ⋯).pt :=
  (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).conePointUniqueUpToIso
    (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.f i) (𝒰.f j))
rw :
  (gluedCover 𝒰).Rel (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x)
    (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y)
⊢ Eq (α := ↥(gluedCover 𝒰).glued) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued)
    (((gluedCover 𝒰).ι j) y : ↥(gluedCover 𝒰).glued)

Tactic:
rw [𝒰.gluedCover.ι_eq_iff]

Premises used: AlgebraicGeometry.Scheme.GlueData.ι_eq_iff, AlgebraicGeometry.Scheme.Cover.gluedCover