-- Module: Mathlib.Topology.Gluing
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))
mpr 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))
⊢ 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 [D.glue_condition_apply]

Premises used: TopCat.GlueData.toGlueData, CategoryTheory.GlueData.glue_condition_apply