-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst_2 : HasPullback i i
inst_3 : HasPullback f g
inst_4 : HasPullback (f ≫ i) (g ≫ i)
inst_5 :
  HasPullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
delta :
  Eq (α :=
    pullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ⟶
      X)
    (CategoryStruct.comp (Y := pullback f g)
      (Iso.hom
        (Iso.trans (Y :=
          pullback (Y :=
            pullback (CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S)))
              (CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))))
            (Z := diagonalObj i) (diagonal i)
            (map (CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S)))
              (CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))) i i
              (CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)))
              (CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S))) (𝟙 S) ⋯ ⋯))
          (asIso
              (map (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) (diagonal i)
                (map (CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S)))
                  (CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))) i i
                  (CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)))
                  (CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S))) (𝟙 S) ⋯ ⋯)
                (𝟙 T) (Iso.hom (congrHom ⋯ ⋯)) (𝟙 (diagonalObj i)) ⋯ ⋯) :
            pullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i)
                (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≅
              pullback (Y :=
                pullback (CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S)))
                  (CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))))
                (Z := diagonalObj i) (diagonal i)
                (map (CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S)))
                  (CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))) i i
                  (CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)))
                  (CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S))) (𝟙 S) ⋯ ⋯))
          (Iso.trans (Y := pullback (Z := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))))
              (pullbackDiagonalMapIso i (𝟙 S) (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) :
                pullback (Y :=
                    pullback (CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S)))
                      (CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))))
                    (Z := diagonalObj i) (diagonal i)
                    (map (CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S)))
                      (CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))) i i
                      (CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)))
                      (CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S))) (𝟙 S) ⋯ ⋯) ≅
                  pullback (Z := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))))
              (asIso (map (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) f g (𝟙 X) (𝟙 Y) (fst i (𝟙 S)) ⋯ ⋯) :
                pullback (Z := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) ≅ pullback f g) :
            pullback (Y :=
                pullback (CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S)))
                  (CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))))
                (Z := diagonalObj i) (diagonal i)
                (map (CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S)))
                  (CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))) i i
                  (CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)))
                  (CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S))) (𝟙 S) ⋯ ⋯) ≅
              pullback f g)))
      (fst f g))
    (snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i))
⊢ Eq (α :=
    pullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ⟶
      X)
    (CategoryStruct.comp (Y := pullback f g) (Iso.hom (pullbackDiagonalMapIdIso f g i)) (fst f g))
    (snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i))

Tactic:
delta pullbackDiagonalMapIdIso

Premises used: CategoryTheory.Limits.pullbackDiagonalMapIdIso