-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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
⊢ (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
have 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))
Tactic: substs eq₁ eq₂ e₁ e₃ e₄
Cleared hypotheses: a, b, c, x, e₁, e₂, y, e₃, e₄, eq₁, eq₂