-- Lean 4 proof step from Mathlib.Topology.Gluing (hypothesis)
Goal:
D : GlueData
i j k : D.J
z : (↑(pullback (D.f j i) (D.f j k)) : 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))
            ((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))
h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ 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))
have h₂ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.t i k ≫ D.f k i = pullback.snd (D.f j i) (D.f j k) ≫ D.t j k ≫ D.f k j
Tactic: have h₂ : D.t' j i k ≫ pullback.fst _ _ ≫ D.t i k ≫ D.f k i =
        pullback.snd _ _ ≫ D.t j k ≫ D.f k j := by
      rw [← 𝖣.t_fac_assoc]
      apply @Epi.left_cancellation _ _ _ _ (D.t' k j i)
      rw [𝖣.cocycle_assoc, 𝖣.t_fac_assoc, 𝖣.t_inv_assoc]
      exact pullback.condition.symm