-- 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 : D.J
hij : ¬i = j
⊢ CategoryStruct.comp (Y := pullback (D.f' i j) (D.f' i i))
      (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 ⋯) ⋯ ⋯)
        (CategoryStruct.comp (Y := pullback (D.f' i i) (D.f' i j))
          (if hij : j = i then
            Iso.hom (pullbackSymmetry (D.f' j i) (D.f' j i)) ≫
              pullback.map (D.f' j i) (D.f' j i) (D.f' i i) (D.f' i j) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
          else
            if hik : j = i then
              have this := ⋯;
              pullback.fst (D.f' j i) (D.f' j i) ≫
                eqToHom ⋯ ≫ D.t j i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i j))
            else
              if hjk : i = i then
                have this := ⋯;
                pullback.fst (D.f' j i) (D.f' j i) ≫
                  eqToHom ⋯ ≫ D.t j i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i i) (D.f' i j))
              else
                pullback.map (D.f' j i) (D.f' j i) (D.f j i hij) (D.f j i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                  D.t' j i i hij hik hjk ≫
                    pullback.map (D.f i i hjk) (D.f i j ⋯) (D.f' i i) (D.f' i j) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                      ⋯)
          (if hij : i = i then
            Iso.hom (pullbackSymmetry (D.f' i i) (D.f' i j)) ≫
              pullback.map (D.f' i j) (D.f' i i) (D.f' i j) (D.f' i i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
          else
            if hik : i = j then
              have this := ⋯;
              pullback.fst (D.f' i i) (D.f' i j) ≫
                eqToHom ⋯ ≫ D.t i i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i j) (D.f' i i))
            else
              if hjk : i = j then
                have this := ⋯;
                pullback.fst (D.f' i i) (D.f' i j) ≫
                  eqToHom ⋯ ≫ D.t i i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i j) (D.f' i i))
              else
                pullback.map (D.f' i i) (D.f' i j) (D.f i i hij) (D.f i j hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                  D.t' i i j hij hik hjk ≫
                    pullback.map (D.f i j hjk) (D.f i i ⋯) (D.f' i j) (D.f' i i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                      ⋯)))
      (pullback.fst (D.f' i j) (D.f' i i)) =
    𝟙 (pullback (D.f' i j) (D.f' i i)) ≫ pullback.fst (D.f' i j) (D.f' i i)

Tactic:
simp [hij, Ne.symm hij, fst_eq_snd_of_mono_eq, pullback.condition_assoc]

Premises used: Ne.symm, CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.Limits.fst_eq_snd_of_mono_eq