-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
h : MkCore
i j k : h.J
⊢ ((pullbackIsoProdSubtype (h.V i j).inclusion' (h.V i k).inclusion').hom ≫
        ofHom
            {
              toFun :=
                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)
                  ⋯,
              continuous_toFun := ⋯ :
              C({ 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)) }) } ≫
          (pullbackIsoProdSubtype (h.V j k).inclusion' (h.V j i).inclusion').inv) ≫
      pullback.snd (h.V j k).inclusion' (h.V j i).inclusion' =
    pullback.fst (h.V i j).inclusion' (h.V i k).inclusion' ≫ h.t i j
have rw : ofHom
      {
        toFun :=
          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,
        continuous_toFun := sorry :
        C({ 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)) }) } ≫
    pullbackSnd (h.V j k).inclusion' (h.V j i).inclusion' =
  pullbackFst (h.V i j).inclusion' (h.V i k).inclusion' ≫ h.t i j
Tactic: rw [Category.assoc, Category.assoc, pullbackIsoProdSubtype_inv_snd, ← Iso.eq_inv_comp,
      pullbackIsoProdSubtype_inv_fst_assoc]