-- Module: Mathlib.CategoryTheory.GlueData
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
inl :
  Eq (α := pullback (D.f' i i) (D.f' i k) ⟶ if h : (i, i).1 = (i, i).2 then D.U (i, i).1 else D.V (i, i).1 (i, i).2 h)
    (CategoryStruct.comp (Y := pullback (D.f' i k) (D.f' i i))
      (if hij : i = i then
        Iso.hom (pullbackSymmetry (D.f' i i) (D.f' i k)) ≫
          pullback.map (D.f' i k) (D.f' i i) (D.f' i k) (D.f' i i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
      else
        if hik : i = k then
          have this := ⋯;
          pullback.fst (D.f' i i) (D.f' i k) ≫
            eqToHom ⋯ ≫ D.t i i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i k) (D.f' i i))
        else
          if hjk : i = k then
            have this := ⋯;
            pullback.fst (D.f' i i) (D.f' i k) ≫
              eqToHom ⋯ ≫ D.t i i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i k) (D.f' i i))
          else
            pullback.map (D.f' i i) (D.f' i k) (D.f i i hij) (D.f i k hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
              D.t' i i k hij hik hjk ≫
                pullback.map (D.f i k hjk) (D.f i i ⋯) (D.f' i k) (D.f' i i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯)
      (pullback.snd (D.f' i k) (D.f' i i)))
    (pullback.fst (D.f' i i) (D.f' i k) ≫ if h : i = i then eqToHom ⋯ else eqToHom ⋯ ≫ D.t i i h ≫ eqToHom ⋯)
inr :
  i ≠ j →
    Eq (α := pullback (D.f' i j) (D.f' i k) ⟶ if h : (j, i).1 = (j, i).2 then D.U (j, i).1 else D.V (j, i).1 (j, i).2 h)
      (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 ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
        else
          if hik : i = k then
            have this := ⋯;
            pullback.fst (D.f' i j) (D.f' i k) ≫
              eqToHom ⋯ ≫ D.t i j hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' j k) (D.f' j i))
          else
            if hjk : j = k then
              have this := ⋯;
              pullback.fst (D.f' i j) (D.f' i k) ≫
                eqToHom ⋯ ≫ D.t i j hij ≫ eqToHom ⋯ ≫ 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 ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                D.t' i j k hij hik hjk ≫
                  pullback.map (D.f j k hjk) (D.f j i ⋯) (D.f' j k) (D.f' j i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯)
        (pullback.snd (D.f' j k) (D.f' j i)))
      (pullback.fst (D.f' i j) (D.f' i k) ≫ if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.t i j h ≫ eqToHom ⋯)
⊢ Eq (α := pullback (D.f' i j) (D.f' i k) ⟶ if h : (j, i).1 = (j, i).2 then D.U (j, i).1 else D.V (j, i).1 (j, i).2 h)
    (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 ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
      else
        if hik : i = k then
          have this := ⋯;
          pullback.fst (D.f' i j) (D.f' i k) ≫
            eqToHom ⋯ ≫ D.t i j hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' j k) (D.f' j i))
        else
          if hjk : j = k then
            have this := ⋯;
            pullback.fst (D.f' i j) (D.f' i k) ≫
              eqToHom ⋯ ≫ D.t i j hij ≫ eqToHom ⋯ ≫ 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 ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
              D.t' i j k hij hik hjk ≫
                pullback.map (D.f j k hjk) (D.f j i ⋯) (D.f' j k) (D.f' j i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯)
      (pullback.snd (D.f' j k) (D.f' j i)))
    (pullback.fst (D.f' i j) (D.f' i k) ≫ if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.t i j h ≫ eqToHom ⋯)

Tactic:
obtain rfl | _ := eq_or_ne i j

Premises used: eq_or_ne, rfl