-- 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))
⊢ (gluedCover 𝒰).Rel (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x)
    (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y)
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))))
    (((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))) sorry).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)))
                  sorry).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))) sorry).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)))
                  sorry).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: use e.hom ⟨⟨x, y⟩, h⟩