-- 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))
h₁ :
  Eq (α :=
    ↥((gluedCover 𝒰).U
        (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
          (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x))))
    (((gluedCover 𝒰).f
          (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
            (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x))
          (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
            (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y)))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                e.hom :
              (a : (↑(TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt : Type u)) →
                (↑(PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.f i) (𝒰.f j)))
                        (forgetToTop.map (pullback.snd (𝒰.f i) (𝒰.f j))) ⋯).pt :
                  Type u))
            (Subtype.mk (p := fun (p : (↑(forgetToTop.obj (𝒰.X i)) : Type u) × (↑(forgetToTop.obj (𝒰.X j)) : Type u)) ↦
              Eq (α := (↑(forgetToTop.obj X) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        TopCat.carrier) (forgetToTop.map (𝒰.f i)) :
                      (a : (↑(forgetToTop.obj (𝒰.X i)) : Type u)) → (↑(forgetToTop.obj X) : Type u))
                    p.1 :
                  (↑(forgetToTop.obj X) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        TopCat.carrier) (forgetToTop.map (𝒰.f j)) :
                      (a : (↑(forgetToTop.obj (𝒰.X j)) : Type u)) → (↑(forgetToTop.obj X) : Type u))
                    p.2 :
                  (↑(forgetToTop.obj X) : Type u)))
              (x, y) h) :
          (↑(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 :
            Type u)) :
      ↥((gluedCover 𝒰).U
          (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
            (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x))))
    (Sigma.snd (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
        (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x) :
      ↥((gluedCover 𝒰).U
          (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
            (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x))))
h₂ :
  Eq (α :=
    ↥((gluedCover 𝒰).U
        (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
          (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y))))
    (((gluedCover 𝒰).t
            (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
              (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x))
            (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
              (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y)) ≫
          (gluedCover 𝒰).f
            (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
              (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y))
            (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
              (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x)))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                e.hom :
              (a : (↑(TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt : Type u)) →
                (↑(PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.f i) (𝒰.f j)))
                        (forgetToTop.map (pullback.snd (𝒰.f i) (𝒰.f j))) ⋯).pt :
                  Type u))
            (Subtype.mk (p := fun (p : (↑(forgetToTop.obj (𝒰.X i)) : Type u) × (↑(forgetToTop.obj (𝒰.X j)) : Type u)) ↦
              Eq (α := (↑(forgetToTop.obj X) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        TopCat.carrier) (forgetToTop.map (𝒰.f i)) :
                      (a : (↑(forgetToTop.obj (𝒰.X i)) : Type u)) → (↑(forgetToTop.obj X) : Type u))
                    p.1 :
                  (↑(forgetToTop.obj X) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        TopCat.carrier) (forgetToTop.map (𝒰.f j)) :
                      (a : (↑(forgetToTop.obj (𝒰.X j)) : Type u)) → (↑(forgetToTop.obj X) : Type u))
                    p.2 :
                  (↑(forgetToTop.obj X) : Type u)))
              (x, y) h) :
          (↑(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 :
            Type u)) :
      ↥((gluedCover 𝒰).U
          (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
            (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y))))
    (Sigma.snd (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
        (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y) :
      ↥((gluedCover 𝒰).U
          (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
            (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y))))
⊢ Eq (α :=
      ↥((gluedCover 𝒰).U
          (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
            (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x))))
      (((gluedCover 𝒰).f
            (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
              (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x))
            (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
              (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y)))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  e.hom :
                (a : (↑(TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt : Type u)) →
                  (↑(PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.f i) (𝒰.f j)))
                          (forgetToTop.map (pullback.snd (𝒰.f i) (𝒰.f j))) ⋯).pt :
                    Type u))
              (Subtype.mk (p :=
                fun (p : (↑(forgetToTop.obj (𝒰.X i)) : Type u) × (↑(forgetToTop.obj (𝒰.X j)) : Type u)) ↦
                Eq (α := (↑(forgetToTop.obj X) : Type u))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          TopCat.carrier) (forgetToTop.map (𝒰.f i)) :
                        (a : (↑(forgetToTop.obj (𝒰.X i)) : Type u)) → (↑(forgetToTop.obj X) : Type u))
                      p.1 :
                    (↑(forgetToTop.obj X) : Type u))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          TopCat.carrier) (forgetToTop.map (𝒰.f j)) :
                        (a : (↑(forgetToTop.obj (𝒰.X j)) : Type u)) → (↑(forgetToTop.obj X) : Type u))
                      p.2 :
                    (↑(forgetToTop.obj X) : Type u)))
                (x, y) h) :
            (↑(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 :
              Type u)) :
        ↥((gluedCover 𝒰).U
            (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
              (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x))))
      (Sigma.snd (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
          (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x) :
        ↥((gluedCover 𝒰).U
            (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
              (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x)))) ∧
    Eq (α :=
      ↥((gluedCover 𝒰).U
          (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
            (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y))))
      (((gluedCover 𝒰).t
              (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
                (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x))
              (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
                (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y)) ≫
            (gluedCover 𝒰).f
              (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
                (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y))
              (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
                (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x)))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  e.hom :
                (a : (↑(TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt : Type u)) →
                  (↑(PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.f i) (𝒰.f j)))
                          (forgetToTop.map (pullback.snd (𝒰.f i) (𝒰.f j))) ⋯).pt :
                    Type u))
              (Subtype.mk (p :=
                fun (p : (↑(forgetToTop.obj (𝒰.X i)) : Type u) × (↑(forgetToTop.obj (𝒰.X j)) : Type u)) ↦
                Eq (α := (↑(forgetToTop.obj X) : Type u))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          TopCat.carrier) (forgetToTop.map (𝒰.f i)) :
                        (a : (↑(forgetToTop.obj (𝒰.X i)) : Type u)) → (↑(forgetToTop.obj X) : Type u))
                      p.1 :
                    (↑(forgetToTop.obj X) : Type u))
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          TopCat.carrier) (forgetToTop.map (𝒰.f j)) :
                        (a : (↑(forgetToTop.obj (𝒰.X j)) : Type u)) → (↑(forgetToTop.obj X) : Type u))
                      p.2 :
                    (↑(forgetToTop.obj X) : Type u)))
                (x, y) h) :
            (↑(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 :
              Type u)) :
        ↥((gluedCover 𝒰).U
            (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
              (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y))))
      (Sigma.snd (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
          (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y) :
        ↥((gluedCover 𝒰).U
            (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
              (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y))))

Tactic:
constructor