-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
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))
⊢ 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))))
have 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))))
Tactic: erw [← ConcreteCategory.comp_apply e.hom,
      IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.left]