-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i : D.J
a : (↑(D.U i) : Type u)
j : D.J
b : (↑(D.U j) : Type u)
k : D.J
c : (↑(D.U k) : Type u)
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 a),
          Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
            (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b))) :
    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))
      x =
    a
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))
          x :
        (↑(D.V (j, i)) : Type u)) =
    b
y :
  (↑(D.V
        (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j b),
          Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
            (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) k c))) :
    Type u)
e₃ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f j k) :
        (a : (↑(D.V (j, k)) : Type u)) → (↑(D.U j) : Type u))
      y =
    b
e₄ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f k j) :
        (a : (↑(D.V (k, j)) : Type u)) → (↑(D.U k) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (D.t j k) :
            (a : (↑(D.V (j, k)) : Type u)) → (↑(D.V (k, j)) : Type u))
          y :
        (↑(D.V (k, j)) : Type u)) =
    c
z : (↑(pullback (D.f j i) (D.f j k)) : Type u)
eq₁ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.t j i) :
        (a : (↑(D.V (j, i)) : Type u)) → (↑(D.V (i, j)) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              pullback (D.f j i) (D.f j k)) (pullback.fst (D.f j i) (D.f j k)) :
            (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, i)) : Type u))
          z :
        (↑(D.V (j, i)) : Type u)) =
    x
eq₂ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback (D.f j i) (D.f j k)) (pullback.snd (D.f j i) (D.f j k)) :
        (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, k)) : Type u))
      z =
    y
h :
  ∀
    (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))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (D.t j i) :
                      (a : (↑(D.V (j, i)) : Type u)) → (↑(D.V (i, j)) : Type u))
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            carrier) (X := pullback (D.f j i) (D.f j k)) (pullback.fst (D.f j i) (D.f j k)) :
                          (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, i)) : Type u))
                        z :
                      (↑(D.V (j, i)) : Type u)) :
                  (↑(D.V (i, j)) : Type u)) :
              (↑(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 k) :
              (a : (↑(D.V (j, k)) : Type u)) → (↑(D.U j) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (X := pullback (D.f j i) (D.f j k)) (pullback.snd (D.f j i) (D.f j k)) :
                  (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, k)) : Type u))
                z :
              (↑(D.V (j, k)) : Type u)) :
          (↑(D.U j) : Type u))),
    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 k) :
              (a : (↑(D.V (i, k)) : Type u)) → (↑(D.U i) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (X := pullback (D.f i k) (D.f i j)) (pullback.fst (D.f i k) (D.f i j)) :
                  (a : (↑(pullback (D.f i k) (D.f i j)) : Type u)) → (↑(D.V (i, k)) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (D.t' j i k) :
                      (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(pullback (D.f i k) (D.f i j)) : Type u))
                    z :
                  (↑(pullback (D.f i k) (D.f i j)) : Type u)) :
              (↑(D.V (i, k)) : Type u)) :
          (↑(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))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (D.t j i) :
                  (a : (↑(D.V (j, i)) : Type u)) → (↑(D.V (i, j)) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (X := pullback (D.f j i) (D.f j k)) (pullback.fst (D.f j i) (D.f j k)) :
                      (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, i)) : Type u))
                    z :
                  (↑(D.V (j, i)) : Type u)) :
              (↑(D.V (i, j)) : Type u)) :
          (↑(D.U i) : Type u)) ∧
      Eq (α := (↑(D.U k) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (D.f k i) :
              (a : (↑(D.V (k, i)) : Type u)) → (↑(D.U k) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (D.t i k) :
                  (a : (↑(D.V (i, k)) : Type u)) → (↑(D.V (k, i)) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (X := pullback (D.f i k) (D.f i j)) (pullback.fst (D.f i k) (D.f i j)) :
                      (a : (↑(pullback (D.f i k) (D.f i j)) : Type u)) → (↑(D.V (i, k)) : Type u))
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            carrier) (D.t' j i k) :
                          (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(pullback (D.f i k) (D.f i j)) : Type u))
                        z :
                      (↑(pullback (D.f i k) (D.f i j)) : Type u)) :
                  (↑(D.V (i, k)) : Type u)) :
              (↑(D.V (k, i)) : Type u)) :
          (↑(D.U k) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (D.f k j) :
              (a : (↑(D.V (k, j)) : Type u)) → (↑(D.U k) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (D.t j k) :
                  (a : (↑(D.V (j, k)) : Type u)) → (↑(D.V (k, j)) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (X := pullback (D.f j i) (D.f j k)) (pullback.snd (D.f j i) (D.f j k)) :
                      (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, k)) : Type u))
                    z :
                  (↑(D.V (j, k)) : Type u)) :
              (↑(D.V (k, j)) : Type u)) :
          (↑(D.U k) : Type u))
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f i k) :
          (a : (↑(D.V (i, k)) : Type u)) → (↑(D.U i) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback (D.f i k) (D.f i j)) (pullback.fst (D.f i k) (D.f i j)) :
              (a : (↑(pullback (D.f i k) (D.f i j)) : Type u)) → (↑(D.V (i, k)) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (D.t' j i k) :
                  (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(pullback (D.f i k) (D.f i j)) : Type u))
                z :
              (↑(pullback (D.f i k) (D.f i j)) : Type u)) :
          (↑(D.V (i, k)) : Type u)) =
      a ∧
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f k i) :
          (a : (↑(D.V (k, i)) : Type u)) → (↑(D.U k) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (D.t i k) :
              (a : (↑(D.V (i, k)) : Type u)) → (↑(D.V (k, i)) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (X := pullback (D.f i k) (D.f i j)) (pullback.fst (D.f i k) (D.f i j)) :
                  (a : (↑(pullback (D.f i k) (D.f i j)) : Type u)) → (↑(D.V (i, k)) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (D.t' j i k) :
                      (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(pullback (D.f i k) (D.f i j)) : Type u))
                    z :
                  (↑(pullback (D.f i k) (D.f i j)) : Type u)) :
              (↑(D.V (i, k)) : Type u)) :
          (↑(D.V (k, i)) : Type u)) =
      c

Tactic:
substs eq₁ eq₂ e₁ e₃ e₄