-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
h : MkCore
i j k : h.J
refine_1 :
  { p :
      (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u) ×
        (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i k)) : Type u) //
      Eq (α := (↑(h.U i) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (h.V i j).inclusion' :
              (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) → (↑(h.U i) : Type u))
            p.1 :
          (↑(h.U i) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (h.V i k).inclusion' :
              (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) → (↑(h.U i) : Type u))
            p.2 :
          (↑(h.U i) : Type u)) } →
    { p :
      (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j k)) : Type u) ×
        (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j i)) : Type u) //
      Eq (α := (↑(h.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (h.V j k).inclusion' :
              (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) → (↑(h.U j) : Type u))
            p.1 :
          (↑(h.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (h.V j i).inclusion' :
              (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u)) → (↑(h.U j) : Type u))
            p.2 :
          (↑(h.U j) : Type u)) }
refine_2 :
  Continuous (Y :=
    { p :
      (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j k)) : Type u) ×
        (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j i)) : Type u) //
      Eq (α := (↑(h.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (h.V j k).inclusion' :
              (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) → (↑(h.U j) : Type u))
            p.1 :
          (↑(h.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (h.V j i).inclusion' :
              (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u)) → (↑(h.U j) : Type u))
            p.2 :
          (↑(h.U j) : Type u)) })
    fun
      (x :
        { p :
          (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i j)) : Type u) ×
            (↑(Functor.obj (Opens.toTopCat (h.U i)) (h.V i k)) : Type u) //
          Eq (α := (↑(h.U i) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (h.V i j).inclusion' :
                  (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) → (↑(h.U i) : Type u))
                p.1 :
              (↑(h.U i) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (h.V i k).inclusion' :
                  (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)) → (↑(h.U i) : Type u))
                p.2 :
              (↑(h.U i) : Type u)) }) ↦
    Subtype.mk (p :=
      fun
        (p :
          (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j k)) : Type u) ×
            (↑(Functor.obj (Opens.toTopCat (h.U j)) (h.V j i)) : Type u)) ↦
      Eq (α := (↑(h.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (h.V j k).inclusion' :
              (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) → (↑(h.U j) : Type u))
            p.1 :
          (↑(h.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (h.V j i).inclusion' :
              (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u)) → (↑(h.U j) : Type u))
            p.2 :
          (↑(h.U j) : Type u)))
      (Subtype.mk (p := fun (x : (↑(h.U j) : Type u)) ↦ x ∈ h.V j k)
          (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (h.t i j) :
                  (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) →
                    (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u))
                (↑x :
                    (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u) ×
                      (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)).1) :
            (↑(h.U j) : Type u))
          ⋯,
        (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (h.t i j) :
            (a : (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u)) →
              (↑((Opens.toTopCat (h.U j)).obj (h.V j i)) : Type u))
          (↑x :
              (↑((Opens.toTopCat (h.U i)).obj (h.V i j)) : Type u) ×
                (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u)).1)
      ⋯
⊢ pullback (h.V i j).inclusion' (h.V i k).inclusion' ⟶ pullback (h.V j k).inclusion' (h.V j i).inclusion'

Tactic:
refine (pullbackIsoProdSubtype _ _).hom ≫ ofHom ⟨?_, ?_⟩ ≫ (pullbackIsoProdSubtype _ _).inv

Premises used: ContinuousMap.mk, TopCat.pullbackIsoProdSubtype, TopCat.ofHom, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv