-- 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
h : i ≠ j
h_1 : i ≠ k
inr :
  i ≠ j →
    Eq (α := pullback (D.f' i j) (D.f' i j) ⟶ 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 j) (D.f' j i))
        (if hij : i = j then
          Iso.hom (pullbackSymmetry (D.f' i j) (D.f' i j)) ≫
            pullback.map (D.f' i j) (D.f' i j) (D.f' j j) (D.f' j i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
        else
          if hik : i = j then
            have this := ⋯;
            pullback.fst (D.f' i j) (D.f' i j) ≫
              eqToHom ⋯ ≫ D.t i j hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' j j) (D.f' j i))
          else
            if hjk : j = j then
              have this := ⋯;
              pullback.fst (D.f' i j) (D.f' i j) ≫
                eqToHom ⋯ ≫ D.t i j hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' j j) (D.f' j i))
            else
              pullback.map (D.f' i j) (D.f' i j) (D.f i j hij) (D.f i j hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                D.t' i j j hij hik hjk ≫
                  pullback.map (D.f j j hjk) (D.f j i ⋯) (D.f' j j) (D.f' j i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯)
        (pullback.snd (D.f' j j) (D.f' j i)))
      (pullback.fst (D.f' i j) (D.f' i j) ≫ 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 ⋯)
have inr₁ : j ≠ k →
  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 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)
      (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 sorry else eqToHom sorry ≫ D.t i j h ≫ eqToHom sorry)
Tactic: obtain rfl | _ := eq_or_ne j k