-- 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 k : D.J
if :
  ∀ (hik : i = k),
    Eq.{v + 1} (α := pullback (D.f' i i) (D.f' i k) ⟶ pullback (D.f' i i) (D.f' i k))
      (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 ⋯) ⋯ ⋯)
        (CategoryStruct.comp (Y := pullback (D.f' k i) (D.f' k i))
          (if hij : i = k then
            Iso.hom (pullbackSymmetry (D.f' i k) (D.f' i i)) ≫
              pullback.map (D.f' i i) (D.f' i k) (D.f' k i) (D.f' k i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
          else
            if hik : i = i then
              have this := ⋯;
              pullback.fst (D.f' i k) (D.f' i i) ≫
                eqToHom ⋯ ≫ D.t i k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k i))
            else
              if hjk : k = i then
                have this := ⋯;
                pullback.fst (D.f' i k) (D.f' i i) ≫
                  eqToHom ⋯ ≫ D.t i k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k i))
              else
                pullback.map (D.f' i k) (D.f' i i) (D.f i k hij) (D.f i i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                  D.t' i k i hij hik hjk ≫
                    pullback.map (D.f k i hjk) (D.f k i ⋯) (D.f' k i) (D.f' k i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                      ⋯)
          (if hij : k = i then
            Iso.hom (pullbackSymmetry (D.f' k i) (D.f' k i)) ≫
              pullback.map (D.f' k i) (D.f' k i) (D.f' i i) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
          else
            if hik : k = i then
              have this := ⋯;
              pullback.fst (D.f' k i) (D.f' k i) ≫
                eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i k))
            else
              if hjk : i = i then
                have this := ⋯;
                pullback.fst (D.f' k i) (D.f' k i) ≫
                  eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i k))
              else
                pullback.map (D.f' k i) (D.f' k i) (D.f k i hij) (D.f k i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                  D.t' k i i hij hik hjk ≫
                    pullback.map (D.f i i hjk) (D.f i k ⋯) (D.f' i i) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                      ⋯)))
      (𝟙 (pullback (D.f' i i) (D.f' i k)))
if₁ :
  ∀ (hik : ¬i = k),
    Eq.{v + 1} (α := pullback (D.f' i i) (D.f' i k) ⟶ pullback (D.f' i i) (D.f' i k))
      (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 ⋯) ⋯ ⋯)
        (CategoryStruct.comp (Y := pullback (D.f' k i) (D.f' k i))
          (if hij : i = k then
            Iso.hom (pullbackSymmetry (D.f' i k) (D.f' i i)) ≫
              pullback.map (D.f' i i) (D.f' i k) (D.f' k i) (D.f' k i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
          else
            if hik : i = i then
              have this := ⋯;
              pullback.fst (D.f' i k) (D.f' i i) ≫
                eqToHom ⋯ ≫ D.t i k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k i))
            else
              if hjk : k = i then
                have this := ⋯;
                pullback.fst (D.f' i k) (D.f' i i) ≫
                  eqToHom ⋯ ≫ D.t i k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k i))
              else
                pullback.map (D.f' i k) (D.f' i i) (D.f i k hij) (D.f i i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                  D.t' i k i hij hik hjk ≫
                    pullback.map (D.f k i hjk) (D.f k i ⋯) (D.f' k i) (D.f' k i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                      ⋯)
          (if hij : k = i then
            Iso.hom (pullbackSymmetry (D.f' k i) (D.f' k i)) ≫
              pullback.map (D.f' k i) (D.f' k i) (D.f' i i) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
          else
            if hik : k = i then
              have this := ⋯;
              pullback.fst (D.f' k i) (D.f' k i) ≫
                eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i k))
            else
              if hjk : i = i then
                have this := ⋯;
                pullback.fst (D.f' k i) (D.f' k i) ≫
                  eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i k))
              else
                pullback.map (D.f' k i) (D.f' k i) (D.f k i hij) (D.f k i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                  D.t' k i i hij hik hjk ≫
                    pullback.map (D.f i i hjk) (D.f i k ⋯) (D.f' i i) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                      ⋯)))
      (𝟙 (pullback (D.f' i i) (D.f' i k)))
if₂ :
  ∀ (hik : i = k),
    Eq.{v + 1} (α := pullback (D.f' i i) (D.f' i k) ⟶ pullback (D.f' i i) (D.f' i k))
      (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 ⋯) ⋯ ⋯)
        (CategoryStruct.comp (Y := pullback (D.f' k i) (D.f' k i))
          (if hij : i = k then
            Iso.hom (pullbackSymmetry (D.f' i k) (D.f' i i)) ≫
              pullback.map (D.f' i i) (D.f' i k) (D.f' k i) (D.f' k i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
          else
            if hik : i = i then
              have this := ⋯;
              pullback.fst (D.f' i k) (D.f' i i) ≫
                eqToHom ⋯ ≫ D.t i k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k i))
            else
              if hjk : k = i then
                have this := ⋯;
                pullback.fst (D.f' i k) (D.f' i i) ≫
                  eqToHom ⋯ ≫ D.t i k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k i))
              else
                pullback.map (D.f' i k) (D.f' i i) (D.f i k hij) (D.f i i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                  D.t' i k i hij hik hjk ≫
                    pullback.map (D.f k i hjk) (D.f k i ⋯) (D.f' k i) (D.f' k i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                      ⋯)
          (if hij : k = i then
            Iso.hom (pullbackSymmetry (D.f' k i) (D.f' k i)) ≫
              pullback.map (D.f' k i) (D.f' k i) (D.f' i i) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
          else
            if hik : k = i then
              have this := ⋯;
              pullback.fst (D.f' k i) (D.f' k i) ≫
                eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i k))
            else
              if hjk : i = i then
                have this := ⋯;
                pullback.fst (D.f' k i) (D.f' k i) ≫
                  eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i k))
              else
                pullback.map (D.f' k i) (D.f' k i) (D.f k i hij) (D.f k i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                  D.t' k i i hij hik hjk ≫
                    pullback.map (D.f i i hjk) (D.f i k ⋯) (D.f' i i) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                      ⋯)))
      (𝟙 (pullback (D.f' i i) (D.f' i k)))
if₃ if₄ :
  ∀ (hik : ¬i = k),
    Eq.{v + 1} (α := pullback (D.f' i i) (D.f' i k) ⟶ pullback (D.f' i i) (D.f' i k))
      (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 ⋯) ⋯ ⋯)
        (CategoryStruct.comp (Y := pullback (D.f' k i) (D.f' k i))
          (if hij : i = k then
            Iso.hom (pullbackSymmetry (D.f' i k) (D.f' i i)) ≫
              pullback.map (D.f' i i) (D.f' i k) (D.f' k i) (D.f' k i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
          else
            if hik : i = i then
              have this := ⋯;
              pullback.fst (D.f' i k) (D.f' i i) ≫
                eqToHom ⋯ ≫ D.t i k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k i))
            else
              if hjk : k = i then
                have this := ⋯;
                pullback.fst (D.f' i k) (D.f' i i) ≫
                  eqToHom ⋯ ≫ D.t i k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k i))
              else
                pullback.map (D.f' i k) (D.f' i i) (D.f i k hij) (D.f i i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                  D.t' i k i hij hik hjk ≫
                    pullback.map (D.f k i hjk) (D.f k i ⋯) (D.f' k i) (D.f' k i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                      ⋯)
          (if hij : k = i then
            Iso.hom (pullbackSymmetry (D.f' k i) (D.f' k i)) ≫
              pullback.map (D.f' k i) (D.f' k i) (D.f' i i) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
          else
            if hik : k = i then
              have this := ⋯;
              pullback.fst (D.f' k i) (D.f' k i) ≫
                eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i k))
            else
              if hjk : i = i then
                have this := ⋯;
                pullback.fst (D.f' k i) (D.f' k i) ≫
                  eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i k))
              else
                pullback.map (D.f' k i) (D.f' k i) (D.f k i hij) (D.f k i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                  D.t' k i i hij hik hjk ≫
                    pullback.map (D.f i i hjk) (D.f i k ⋯) (D.f' i i) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                      ⋯)))
      (𝟙 (pullback (D.f' i i) (D.f' i k)))
⊢ Eq.{v + 1} (α := pullback (D.f' i i) (D.f' i k) ⟶ pullback (D.f' i i) (D.f' i k))
    (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 ⋯) ⋯ ⋯)
      (CategoryStruct.comp (Y := pullback (D.f' k i) (D.f' k i))
        (if hij : i = k then
          Iso.hom (pullbackSymmetry (D.f' i k) (D.f' i i)) ≫
            pullback.map (D.f' i i) (D.f' i k) (D.f' k i) (D.f' k i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
        else
          if hik : i = i then
            have this := ⋯;
            pullback.fst (D.f' i k) (D.f' i i) ≫
              eqToHom ⋯ ≫ D.t i k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k i))
          else
            if hjk : k = i then
              have this := ⋯;
              pullback.fst (D.f' i k) (D.f' i i) ≫
                eqToHom ⋯ ≫ D.t i k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k i))
            else
              pullback.map (D.f' i k) (D.f' i i) (D.f i k hij) (D.f i i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                D.t' i k i hij hik hjk ≫
                  pullback.map (D.f k i hjk) (D.f k i ⋯) (D.f' k i) (D.f' k i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯)
        (if hij : k = i then
          Iso.hom (pullbackSymmetry (D.f' k i) (D.f' k i)) ≫
            pullback.map (D.f' k i) (D.f' k i) (D.f' i i) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
        else
          if hik : k = i then
            have this := ⋯;
            pullback.fst (D.f' k i) (D.f' k i) ≫
              eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i k))
          else
            if hjk : i = i then
              have this := ⋯;
              pullback.fst (D.f' k i) (D.f' k i) ≫
                eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i k))
            else
              pullback.map (D.f' k i) (D.f' k i) (D.f k i hij) (D.f k i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                D.t' k i i hij hik hjk ≫
                  pullback.map (D.f i i hjk) (D.f i k ⋯) (D.f' i i) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                    ⋯)))
    (𝟙 (pullback (D.f' i i) (D.f' i k)))

Tactic:
if hik : i = k then
        subst hik
        ext <;> simp
      else
        simp [hik, Ne.symm hik, fst_eq_snd_of_mono_eq]

Premises used: CategoryTheory.Limits.fst_eq_snd_of_mono_eq