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