Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: case h₀
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
⊢ ((if hij : i = j then
          (pullbackSymmetry (D.f' i j) (D.f' i k)).hom ≫
            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 ⋯) ⋯
                    ⋯) ≫
        (if hij : j = k then
            (pullbackSymmetry (D.f' j k) (D.f' j i)).hom ≫
              pullback.map (D.f' j i) (D.f' j k) (D.f' k i) (D.f' k j) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
          else
            if hik : j = i then
              have this := ⋯;
              pullback.fst (D.f' j k) (D.f' j i) ≫
                eqToHom ⋯ ≫ D.t j k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k j))
            else
              if hjk : k = i then
                have this := ⋯;
                pullback.fst (D.f' j k) (D.f' j i) ≫
                  eqToHom ⋯ ≫ D.t j k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k j))
              else
                pullback.map (D.f' j k) (D.f' j i) (D.f j k hij) (D.f j i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                  D.t' j k i hij hik hjk ≫
                    pullback.map (D.f k i hjk) (D.f k j ⋯) (D.f' k i) (D.f' k j) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                      ⋯) ≫
          if hij : k = i then
            (pullbackSymmetry (D.f' k i) (D.f' k j)).hom ≫
              pullback.map (D.f' k j) (D.f' k i) (D.f' i j) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
          else
            if hik : k = j then
              have this := ⋯;
              pullback.fst (D.f' k i) (D.f' k j) ≫
                eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i j) (D.f' i k))
            else
              if hjk : i = j then
                have this := ⋯;
                pullback.fst (D.f' k i) (D.f' k j) ≫
                  eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i j) (D.f' i k))
              else
                pullback.map (D.f' k i) (D.f' k j) (D.f k i hij) (D.f k j hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                  D.t' k i j hij hik hjk ≫
                    pullback.map (D.f i j hjk) (D.f i k ⋯) (D.f' i j) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                      ⋯) ≫
      pullback.fst (D.f' i j) (D.f' i k) =
    𝟙 (pullback (D.f' i j) (D.f' i k)) ≫ pullback.fst (D.f' i j) (D.f' i k)

pp: case h₁
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
⊢ ((if hij : i = j then
          (pullbackSymmetry (D.f' i j) (D.f' i k)).hom ≫
            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 ⋯) ⋯
                    ⋯) ≫
        (if hij : j = k then
            (pullbackSymmetry (D.f' j k) (D.f' j i)).hom ≫
              pullback.map (D.f' j i) (D.f' j k) (D.f' k i) (D.f' k j) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
          else
            if hik : j = i then
              have this := ⋯;
              pullback.fst (D.f' j k) (D.f' j i) ≫
                eqToHom ⋯ ≫ D.t j k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k j))
            else
              if hjk : k = i then
                have this := ⋯;
                pullback.fst (D.f' j k) (D.f' j i) ≫
                  eqToHom ⋯ ≫ D.t j k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k j))
              else
                pullback.map (D.f' j k) (D.f' j i) (D.f j k hij) (D.f j i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                  D.t' j k i hij hik hjk ≫
                    pullback.map (D.f k i hjk) (D.f k j ⋯) (D.f' k i) (D.f' k j) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                      ⋯) ≫
          if hij : k = i then
            (pullbackSymmetry (D.f' k i) (D.f' k j)).hom ≫
              pullback.map (D.f' k j) (D.f' k i) (D.f' i j) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
          else
            if hik : k = j then
              have this := ⋯;
              pullback.fst (D.f' k i) (D.f' k j) ≫
                eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i j) (D.f' i k))
            else
              if hjk : i = j then
                have this := ⋯;
                pullback.fst (D.f' k i) (D.f' k j) ≫
                  eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i j) (D.f' i k))
              else
                pullback.map (D.f' k i) (D.f' k j) (D.f k i hij) (D.f k j hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                  D.t' k i j hij hik hjk ≫
                    pullback.map (D.f i j hjk) (D.f i k ⋯) (D.f' i j) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                      ⋯) ≫
      pullback.snd (D.f' i j) (D.f' i k) =
    𝟙 (pullback (D.f' i j) (D.f' i k)) ≫ pullback.snd (D.f' i j) (D.f' i k)

Tactic:
<;>

Goal state after:
case h₀
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
⊢ ((if hij : i = j then
          (pullbackSymmetry (D.f' i j) (D.f' i k)).hom ≫
            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 ⋯) ⋯
                    ⋯) ≫
        (if hij : j = k then
            (pullbackSymmetry (D.f' j k) (D.f' j i)).hom ≫
              pullback.map (D.f' j i) (D.f' j k) (D.f' k i) (D.f' k j) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
          else
            if hik : j = i then
              have this := ⋯;
              pullback.fst (D.f' j k) (D.f' j i) ≫
                eqToHom ⋯ ≫ D.t j k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k j))
            else
              if hjk : k = i then
                have this := ⋯;
                pullback.fst (D.f' j k) (D.f' j i) ≫
                  eqToHom ⋯ ≫ D.t j k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k j))
              else
                pullback.map (D.f' j k) (D.f' j i) (D.f j k hij) (D.f j i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                  D.t' j k i hij hik hjk ≫
                    pullback.map (D.f k i hjk) (D.f k j ⋯) (D.f' k i) (D.f' k j) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                      ⋯) ≫
          if hij : k = i then
            (pullbackSymmetry (D.f' k i) (D.f' k j)).hom ≫
              pullback.map (D.f' k j) (D.f' k i) (D.f' i j) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
          else
            if hik : k = j then
              have this := ⋯;
              pullback.fst (D.f' k i) (D.f' k j) ≫
                eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i j) (D.f' i k))
            else
              if hjk : i = j then
                have this := ⋯;
                pullback.fst (D.f' k i) (D.f' k j) ≫
                  eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i j) (D.f' i k))
              else
                pullback.map (D.f' k i) (D.f' k j) (D.f k i hij) (D.f k j hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                  D.t' k i j hij hik hjk ≫
                    pullback.map (D.f i j hjk) (D.f i k ⋯) (D.f' i j) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                      ⋯) ≫
      pullback.fst (D.f' i j) (D.f' i k) =
    𝟙 (pullback (D.f' i j) (D.f' i k)) ≫ pullback.fst (D.f' i j) (D.f' i k)

case h₁
C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
⊢ ((if hij : i = j then
          (pullbackSymmetry (D.f' i j) (D.f' i k)).hom ≫
            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 ⋯) ⋯
                    ⋯) ≫
        (if hij : j = k then
            (pullbackSymmetry (D.f' j k) (D.f' j i)).hom ≫
              pullback.map (D.f' j i) (D.f' j k) (D.f' k i) (D.f' k j) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
          else
            if hik : j = i then
              have this := ⋯;
              pullback.fst (D.f' j k) (D.f' j i) ≫
                eqToHom ⋯ ≫ D.t j k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k j))
            else
              if hjk : k = i then
                have this := ⋯;
                pullback.fst (D.f' j k) (D.f' j i) ≫
                  eqToHom ⋯ ≫ D.t j k hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' k i) (D.f' k j))
              else
                pullback.map (D.f' j k) (D.f' j i) (D.f j k hij) (D.f j i hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                  D.t' j k i hij hik hjk ≫
                    pullback.map (D.f k i hjk) (D.f k j ⋯) (D.f' k i) (D.f' k j) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                      ⋯) ≫
          if hij : k = i then
            (pullbackSymmetry (D.f' k i) (D.f' k j)).hom ≫
              pullback.map (D.f' k j) (D.f' k i) (D.f' i j) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
          else
            if hik : k = j then
              have this := ⋯;
              pullback.fst (D.f' k i) (D.f' k j) ≫
                eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i j) (D.f' i k))
            else
              if hjk : i = j then
                have this := ⋯;
                pullback.fst (D.f' k i) (D.f' k j) ≫
                  eqToHom ⋯ ≫ D.t k i hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' i j) (D.f' i k))
              else
                pullback.map (D.f' k i) (D.f' k j) (D.f k i hij) (D.f k j hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
                  D.t' k i j hij hik hjk ≫
                    pullback.map (D.f i j hjk) (D.f i k ⋯) (D.f' i j) (D.f' i k) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯
                      ⋯) ≫
      pullback.snd (D.f' i j) (D.f' i k) =
    𝟙 (pullback (D.f' i j) (D.f' i k)) ≫ pullback.snd (D.f' i j) (D.f' i k)