-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i : D.J
x y : (↑(D.U i) : Type u)
h :
  Eq (α := (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued) (D.ι i) :
          (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u))
        x :
      (↑D.glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued) (D.ι i) :
          (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u))
        y :
      (↑D.glued : Type u))
rcases :
  ∀
    (w :
      (↑(D.V
            (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x),
              Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i y))) :
        Type u))
    (e₁ :
      Eq (α :=
        (↑(D.U
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x))) :
          Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                D.V
                  (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x),
                    Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i y)))
                (D.f
                  (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x))
                  (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i y))) :
              (a : (↑(D.V (⟨i, x⟩.fst, ⟨i, y⟩.fst)) : Type u)) → (↑(D.U ⟨i, x⟩.fst) : Type u))
            w :
          (↑(D.U
                (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x))) :
            Type u))
        (Sigma.snd (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
            (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x) :
          (↑(D.U
                (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x))) :
            Type u)))
    (e₂ :
      Eq (α :=
        (↑(D.U
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i y))) :
          Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                D.V
                  (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i y),
                    Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x)))
                (D.f
                  (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i y))
                  (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x))) :
              (a : (↑(D.V (⟨i, y⟩.fst, ⟨i, x⟩.fst)) : Type u)) → (↑(D.U ⟨i, y⟩.fst) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (X :=
                    D.V
                      (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                          (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x),
                        Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                          (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i y)))
                    (D.t
                      (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                        (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x))
                      (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                        (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i y))) :
                  (a : (↑(D.V (⟨i, x⟩.fst, ⟨i, y⟩.fst)) : Type u)) → (↑(D.V (⟨i, y⟩.fst, ⟨i, x⟩.fst)) : Type u))
                w :
              (↑(D.V
                    (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                        (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i y),
                      Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                        (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x))) :
                Type u)) :
          (↑(D.U
                (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i y))) :
            Type u))
        (Sigma.snd (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
            (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i y) :
          (↑(D.U
                (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i y))) :
            Type u))),
    x = y
⊢ x = y

Tactic:
rcases (D.ι_eq_iff_rel _ _ _ _).mp h with ⟨_, e₁, e₂⟩

Premises used: Iff.mp, TopCat.GlueData.ι_eq_iff_rel