-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : 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) ⋯ ⋯)
refine_1 : f ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))
refine_1₁ : g ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))
refine_1₂ : diagonal i ≫ 𝟙 (diagonalObj i) = 𝟙 T ≫ diagonal i
refine_1₃ :
  Eq (α := pullback (f ≫ i) (g ≫ i) ⟶ diagonalObj i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj i))
    (CategoryStruct.comp (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))))
      (Iso.hom (congrHom ⋯ ⋯))
      (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) ⋯ ⋯))
refine_1₄ :
  IsIso (X :=
    pullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯))
    (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) ⋯ ⋯))
    (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) ⋯ ⋯)

Tactic:
refine @asIso _ _ _ _ (pullback.map _ _ _ _ (𝟙 T) ((pullback.congrHom ?_ ?_).hom) (𝟙 _) ?_ ?_)
      ?_

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.pullback.map, CategoryTheory.Limits.pullback.congrHom, CategoryTheory.Iso.hom, CategoryTheory.asIso