-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
i j : D.J
x : (↑(D.U i) : Type u)
y : (↑(D.U j) : Type u)
z :
  (↑(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)) j y))) :
    Type u)
e₁ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f i j) :
        (a : (↑(D.V (i, j)) : Type u)) → (↑(D.U i) : Type u))
      z =
    x
e₂ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f j i) :
        (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U j) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (D.t i j) :
            (a : (↑(D.V (i, j)) : Type u)) → (↑(D.V (j, i)) : Type u))
          z :
        (↑(D.V (j, i)) : Type u)) =
    y
⊢ 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.ι j) :
          (a : (↑(D.U j) : Type u)) → (↑D.glued : Type u))
        y :
      (↑D.glued : Type u))
have mpr : ∀
  (e₁ :
    Eq (α := (↑(D.U i) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (D.f i j) :
            (a : (↑(D.V (i, j)) : Type u)) → (↑(D.U i) : Type u))
          z :
        (↑(D.U i) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (D.f i j) :
            (a : (↑(D.V (i, j)) : Type u)) → (↑(D.U i) : Type u))
          z :
        (↑(D.U i) : Type u)))
  (e₂ :
    Eq (α := (↑(D.U j) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (D.f j i) :
            (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U j) : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (D.t i j) :
                (a : (↑(D.V (i, j)) : Type u)) → (↑(D.V (j, i)) : Type u))
              z :
            (↑(D.V (j, i)) : Type u)) :
        (↑(D.U j) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (D.f j i) :
            (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U j) : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (D.t i j) :
                (a : (↑(D.V (i, j)) : Type u)) → (↑(D.V (j, i)) : Type u))
              z :
            (↑(D.V (j, i)) : Type u)) :
        (↑(D.U j) : Type u))),
  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))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (D.f i j) :
              (a : (↑(D.V (i, j)) : Type u)) → (↑(D.U i) : Type u))
            z :
          (↑(D.U i) : Type u)) :
      (↑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.ι j) :
          (a : (↑(D.U j) : Type u)) → (↑D.glued : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (D.f j i) :
              (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U j) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (D.t i j) :
                  (a : (↑(D.V (i, j)) : Type u)) → (↑(D.V (j, i)) : Type u))
                z :
              (↑(D.V (j, i)) : Type u)) :
          (↑(D.U j) : Type u)) :
      (↑D.glued : Type u))
Tactic: rw [← e₁, ← e₂] at *
Cleared hypotheses: e₁, e₂