-- 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₁ :
  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))
have mpr : 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.ι 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))
Tactic: rw [D.glue_condition_apply]