-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
h : MkCore
i j k : h.J
x : (↑(h.U i) : Type u)
hx : x ∈ h.V i j
hx' : x ∈ h.V i k
⊢ Eq (α :=
    { 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) //
      (↑p.1 : (↑(h.U i) : Type u)) = (↑p.2 : (↑(h.U i) : Type u)) })
    (Subtype.mk (p :=
        fun
          (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)) ↦
        (↑p.1 : (↑(h.U i) : Type u)) = (↑p.2 : (↑(h.U i) : Type u)))
        (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j)
            (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (h.t k i) :
                    (a : (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u)) →
                      (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u))
                  (Subtype.mk (p := fun (x : (↑(h.U k) : Type u)) ↦ x ∈ h.V k i)
                    (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              carrier) (h.t j k) :
                            (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) →
                              (↑((Opens.toTopCat (h.U k)).obj (h.V k 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))
                                  (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx)) :
                              (↑(h.U j) : Type u))
                            ⋯)) :
                      (↑(h.U k) : Type u))
                    ⋯)) :
              (↑(h.U i) : Type u))
            ⋯,
          (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (h.t k i) :
              (a : (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u)) →
                (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u))
            (Subtype.mk (p := fun (x : (↑(h.U k) : Type u)) ↦ x ∈ h.V k i)
              (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (h.t j k) :
                      (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) →
                        (↑((Opens.toTopCat (h.U k)).obj (h.V k 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))
                            (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx)) :
                        (↑(h.U j) : Type u))
                      ⋯)) :
                (↑(h.U k) : Type u))
              ⋯))
        ⋯ :
      { 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) //
        (↑p.1 : (↑(h.U i) : Type u)) = (↑p.2 : (↑(h.U i) : Type u)) })
    (Subtype.mk (p :=
        fun
          (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)) ↦
        (↑p.1 : (↑(h.U i) : Type u)) = (↑p.2 : (↑(h.U i) : Type u)))
        (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx,
          Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i k) x hx')
        ⋯ :
      { 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) //
        (↑p.1 : (↑(h.U i) : Type u)) = (↑p.2 : (↑(h.U i) : Type u)) })
have w : (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (h.t k i) :
          (a : (↑((Opens.toTopCat (h.U k)).obj (h.V k i)) : Type u)) →
            (↑((Opens.toTopCat (h.U i)).obj (h.V i k)) : Type u))
        (Subtype.mk (p := fun (x : (↑(h.U k) : Type u)) ↦ x ∈ h.V k i)
          (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (h.t j k) :
                  (a : (↑((Opens.toTopCat (h.U j)).obj (h.V j k)) : Type u)) →
                    (↑((Opens.toTopCat (h.U k)).obj (h.V k 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))
                        (Subtype.mk (p := fun (x : (↑(h.U i) : Type u)) ↦ x ∈ h.V i j) x hx)) :
                    (↑(h.U j) : Type u))
                  sorry)) :
            (↑(h.U k) : Type u))
          sorry)) :
    (↑(h.U i) : Type u)) =
  x
Tactic: rw [Subtype.mk_eq_mk, Prod.mk_inj, Subtype.mk_eq_mk, Subtype.ext_iff, and_self_iff]