-- 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))))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            ((TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).π.app WalkingCospan.left) :
          (a : (↑(TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt : Type u)) →
            ↥((gluedCover 𝒰).U ⟨i, x⟩.fst))
        (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) :
      ↥((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)) 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))))

Tactic:
erw [← ConcreteCategory.comp_apply e.hom,
      IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.left]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.WalkingCospan.left, CategoryTheory.Iso.hom