-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_2 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteCoproducts.{v, u} C
n : ℕ
this_1 : ∀ (f : Fin n → C), PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsColimit.{0, v', 0, u'} (J := Discrete (Fin (n + 1))) (F :=
  Discrete.functor fun (i : Fin (n + 1)) ↦ F.obj (f i))
  (extendCofan
    (Cofan.mk (F.obj (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)) fun (j : Fin n) ↦
      F.map (Sigma.ι.{0, v, u} (C := C) (fun (i : Fin n) ↦ f i.succ) j))
    (BinaryCofan.mk (P := F.obj (coprod.{v, u} (f 0) (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)))
      (F.map coprod.inl) (F.map coprod.inr))) :=
  extendCofanIsColimit (fun (i : Fin (n + 1)) ↦ F.obj (f i))
    (isColimitOfHasCoproductOfPreservesColimit F fun (i : Fin n) ↦ f i.succ)
    (isColimitOfHasBinaryCoproductOfPreservesColimit F (f 0) (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ))
⊢ Cocone.pt.{0, v', 0, u'} (J := Discrete (Fin (n + 1))) (F := Discrete.functor fun (i : Fin (n + 1)) ↦ F.obj (f i))
      (extendCofan
        (Cofan.mk (F.obj (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)) fun (j : Fin n) ↦
          F.map (Sigma.ι.{0, v, u} (C := C) (fun (i : Fin n) ↦ f i.succ) j))
        (BinaryCofan.mk (P := F.obj (coprod.{v, u} (f 0) (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)))
          (F.map coprod.inl) (F.map coprod.inr))) ≅
    Cocone.pt.{0, v', 0, u'} (J := Discrete (Fin (n + 1))) (F := Discrete.functor fun (i : Fin (n + 1)) ↦ F.obj (f i))
      (Cofan.mk
        (F.obj
          (Cocone.pt.{0, v, 0, u} (F :=
            pair (f 0)
              (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))
            (colimit.cocone
              (pair (f 0)
                (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                  (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ)))))))
        fun (j : Fin (n + 1)) ↦
        F.map
          (Fin.cases (motive := fun (x : Fin (n + 1)) ↦
            f x ⟶
              Cocone.pt.{0, v, 0, u} (F :=
                pair (f 0)
                  (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                    (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))
                (colimit.cocone
                  (pair (f 0)
                    (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                      (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))))
            (BinaryCofan.inl
              (colimit.cocone
                (pair (f 0)
                  (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                    (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))))
            (fun (i : Fin n) ↦
              NatTrans.app (Cocone.ι (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))) { as := i } ≫
                BinaryCofan.inr
                  (colimit.cocone
                    (pair (f 0)
                      (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                        (colimit.cocone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))))
            j))

Tactic:
apply Iso.refl _

Premises used: CategoryTheory.Iso.refl