-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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)) }
⊢ pullback (h.V i j).inclusion' (h.V i k).inclusion' ⟶ pullback (h.V j k).inclusion' (h.V j i).inclusion'
have 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))
        sorry,
      (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)
    sorry
Tactic: refine (pullbackIsoProdSubtype _ _).hom ≫ ofHom ⟨?_, ?_⟩ ≫ (pullbackIsoProdSubtype _ _).inv