-- Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u₁
inst_1 : Category.{v₁, u₁} A
X Y Z : FormalCoproduct.{w, u} C
f : X ⟶ Z
g : Y ⟶ Z
pb : (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i : X.I × Y.I).1 ≫ eqToHom ⋯) (g.φ (↑i : X.I × Y.I).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct.{w, u} C
i : I.{w, u} (C := C) { I := Function.Pullback f.f g.f, obj := fun (i : Function.Pullback f.f g.f) ↦ (pb i).pt }
⊢ Eq (α :=
    obj
        { I := Function.Pullback f.f g.f, obj := fun (i : Function.Pullback f.f g.f) ↦ (pb i).pt :
          FormalCoproduct.{w, u} C }
        i ⟶
      Z.obj
        (Hom.f
          ({
              f :=
                fun
                  (i :
                    I.{w, u} (C := C)
                      { I := Function.Pullback f.f g.f, obj := fun (i : Function.Pullback f.f g.f) ↦ (pb i).pt :
                        FormalCoproduct.{w, u} C }) ↦
                (↑i : X.I × Y.I).2,
              φ :=
                fun
                  (i :
                    I.{w, u} (C := C)
                      { I := Function.Pullback f.f g.f, obj := fun (i : Function.Pullback f.f g.f) ↦ (pb i).pt :
                        FormalCoproduct.{w, u} C }) ↦
                (pb i).snd :
              Hom.{w, v, u}
                { I := Function.Pullback f.f g.f, obj := fun (i : Function.Pullback f.f g.f) ↦ (pb i).pt :
                  FormalCoproduct.{w, u} C }
                Y } ≫
            g)
          i))
    (CategoryStruct.comp (Y :=
      Z.obj
        (Hom.f
          ({
              f :=
                fun
                  (i :
                    I.{w, u} (C := C)
                      { I := Function.Pullback f.f g.f, obj := fun (i : Function.Pullback f.f g.f) ↦ (pb i).pt :
                        FormalCoproduct.{w, u} C }) ↦
                (↑i : X.I × Y.I).1,
              φ :=
                fun
                  (i :
                    I.{w, u} (C := C)
                      { I := Function.Pullback f.f g.f, obj := fun (i : Function.Pullback f.f g.f) ↦ (pb i).pt :
                        FormalCoproduct.{w, u} C }) ↦
                (pb i).fst :
              Hom.{w, v, u}
                { I := Function.Pullback f.f g.f, obj := fun (i : Function.Pullback f.f g.f) ↦ (pb i).pt :
                  FormalCoproduct.{w, u} C }
                X } ≫
            f)
          i))
      (Hom.φ
        ({
            f :=
              fun
                (i :
                  I.{w, u} (C := C)
                    { I := Function.Pullback f.f g.f, obj := fun (i : Function.Pullback f.f g.f) ↦ (pb i).pt }) ↦
              (↑i : X.I × Y.I).1,
            φ :=
              fun
                (i :
                  I.{w, u} (C := C)
                    { I := Function.Pullback f.f g.f, obj := fun (i : Function.Pullback f.f g.f) ↦ (pb i).pt }) ↦
              (pb i).fst } ≫
          f)
        i)
      (eqToHom ⋯))
    (Hom.φ
      ({
          f :=
            fun
              (i :
                I.{w, u} (C := C)
                  { I := Function.Pullback f.f g.f, obj := fun (i : Function.Pullback f.f g.f) ↦ (pb i).pt }) ↦
            (↑i : X.I × Y.I).2,
          φ :=
            fun
              (i :
                I.{w, u} (C := C)
                  { I := Function.Pullback f.f g.f, obj := fun (i : Function.Pullback f.f g.f) ↦ (pb i).pt }) ↦
            (pb i).snd } ≫
        g)
      i)

Tactic:
simp [(pb i).condition]

Premises used: CategoryTheory.Limits.PullbackCone.condition