-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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))
⊢ x = y
have 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
Tactic: rcases (D.ι_eq_iff_rel _ _ _ _).mp h with ⟨_, e₁, e₂⟩