-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
⊢ D.t'' i j k ≫ D.t'' j k i ≫ D.t'' k i j = 𝟙 (pullback (D.f' i j) (D.f' i k))
have delta : Eq.{v + 1} (α := pullback (D.f' i j) (D.f' i k) ⟶ pullback (D.f' i j) (D.f' i k))
  (CategoryStruct.comp (Y := pullback (D.f' j k) (D.f' j i))
    (if hij : i = j then
      Iso.hom (pullbackSymmetry (D.f' i j) (D.f' i k)) ≫
        pullback.map (D.f' i k) (D.f' i j) (D.f' j k) (D.f' j i) (eqToHom sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry
    else
      if hik : i = k then
        have this := sorry;
        pullback.fst (D.f' i j) (D.f' i k) ≫
          eqToHom sorry ≫ D.t i j hij ≫ eqToHom sorry ≫ inv (pullback.snd (D.f' j k) (D.f' j i))
      else
        if hjk : j = k then
          have this := sorry;
          pullback.fst (D.f' i j) (D.f' i k) ≫
            eqToHom sorry ≫ D.t i j hij ≫ eqToHom sorry ≫ inv (pullback.snd (D.f' j k) (D.f' j i))
        else
          pullback.map (D.f' i j) (D.f' i k) (D.f i j hij) (D.f i k hik) (eqToHom sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry ≫
            D.t' i j k hij hik hjk ≫
              pullback.map (D.f j k hjk) (D.f j i sorry) (D.f' j k) (D.f' j i) (eqToHom sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry)
    (CategoryStruct.comp (Y := pullback (D.f' k i) (D.f' k j))
      (if hij : j = k then
        Iso.hom (pullbackSymmetry (D.f' j k) (D.f' j i)) ≫
          pullback.map (D.f' j i) (D.f' j k) (D.f' k i) (D.f' k j) (eqToHom sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry
      else
        if hik : j = i then
          have this := sorry;
          pullback.fst (D.f' j k) (D.f' j i) ≫
            eqToHom sorry ≫ D.t j k hij ≫ eqToHom sorry ≫ inv (pullback.snd (D.f' k i) (D.f' k j))
        else
          if hjk : k = i then
            have this := sorry;
            pullback.fst (D.f' j k) (D.f' j i) ≫
              eqToHom sorry ≫ D.t j k hij ≫ eqToHom sorry ≫ inv (pullback.snd (D.f' k i) (D.f' k j))
          else
            pullback.map (D.f' j k) (D.f' j i) (D.f j k hij) (D.f j i hik) (eqToHom sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry ≫
              D.t' j k i hij hik hjk ≫
                pullback.map (D.f k i hjk) (D.f k j sorry) (D.f' k i) (D.f' k j) (eqToHom sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry)
      (if hij : k = i then
        Iso.hom (pullbackSymmetry (D.f' k i) (D.f' k j)) ≫
          pullback.map (D.f' k j) (D.f' k i) (D.f' i j) (D.f' i k) (eqToHom sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry
      else
        if hik : k = j then
          have this := sorry;
          pullback.fst (D.f' k i) (D.f' k j) ≫
            eqToHom sorry ≫ D.t k i hij ≫ eqToHom sorry ≫ inv (pullback.snd (D.f' i j) (D.f' i k))
        else
          if hjk : i = j then
            have this := sorry;
            pullback.fst (D.f' k i) (D.f' k j) ≫
              eqToHom sorry ≫ D.t k i hij ≫ eqToHom sorry ≫ inv (pullback.snd (D.f' i j) (D.f' i k))
          else
            pullback.map (D.f' k i) (D.f' k j) (D.f k i hij) (D.f k j hik) (eqToHom sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry ≫
              D.t' k i j hij hik hjk ≫
                pullback.map (D.f i j hjk) (D.f i k sorry) (D.f' i j) (D.f' i k) (eqToHom sorry) (eqToHom sorry) (eqToHom sorry) sorry sorry)))
  (𝟙 (pullback (D.f' i j) (D.f' i k)))
Tactic: delta GlueData'.t''