-- 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 : PreservesLimitsOfShape (Discrete WalkingPair) F
inst_3 : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst_4 : HasFiniteProducts.{v, u} C
n : ℕ
this_1 : ∀ (f : Fin n → C), PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit.{0, v', 0, u'} (J := Discrete (Fin (n + 1))) (F := Discrete.functor fun (i : Fin (n + 1)) ↦ F.obj (f i))
  (extendFan
    (Fan.mk (F.obj (piObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)) fun (j : Fin n) ↦
      F.map (Pi.π (fun (i : Fin n) ↦ f i.succ) j))
    (BinaryFan.mk (P := F.obj (Limits.prod.{v, u} (f 0) (piObj.{0, v, u} fun (i : Fin n) ↦ f i.succ))) (F.map prod.fst)
      (F.map prod.snd))) :=
  extendFanIsLimit (fun (i : Fin (n + 1)) ↦ F.obj (f i))
    (isLimitOfHasProductOfPreservesLimit F fun (i : Fin n) ↦ f i.succ)
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (piObj.{0, v, u} fun (i : Fin n) ↦ f i.succ))
apply :
  Cone.pt.{0, v', 0, u'} (J := Discrete (Fin (n + 1))) (F := Discrete.functor fun (i : Fin (n + 1)) ↦ F.obj (f i))
      (extendFan
        (Fan.mk (F.obj (piObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)) fun (j : Fin n) ↦
          F.map (Pi.π (fun (i : Fin n) ↦ f i.succ) j))
        (BinaryFan.mk (P := F.obj (Limits.prod.{v, u} (f 0) (piObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)))
          (F.map prod.fst) (F.map prod.snd))) ≅
    Cone.pt.{0, v', 0, u'} (J := Discrete (Fin (n + 1))) (F := Discrete.functor fun (i : Fin (n + 1)) ↦ F.obj (f i))
      (Fan.mk
        (F.obj
          (Cone.pt.{0, v, 0, u} (F :=
            pair (f 0)
              (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))
            (limit.cone
              (pair (f 0)
                (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                  (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ)))))))
        fun (j : Fin (n + 1)) ↦
        F.map
          (Fin.cases (motive := fun (x : Fin (n + 1)) ↦
            Cone.pt.{0, v, 0, u} (F :=
                pair (f 0)
                  (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                    (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))
                (limit.cone
                  (pair (f 0)
                    (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                      (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))) ⟶
              f x)
            (BinaryFan.fst
              (limit.cone
                (pair (f 0)
                  (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                    (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))))
            (fun (i : Fin n) ↦
              BinaryFan.snd
                  (limit.cone
                    (pair (f 0)
                      (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                        (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))) ≫
                NatTrans.app (Cone.π (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))) { as := i })
            j))
apply₁ :
  ∀ (j : Discrete (Fin (n + 1))),
    Eq.{v' + 1} (α :=
      Functor.obj.{0, v', 0, u'}
          (Functor.obj (Functor.const (Discrete (Fin (n + 1))))
            (Cone.pt.{0, v', 0, u'} (J := Discrete (Fin (n + 1))) (F :=
              Discrete.functor fun (i : Fin (n + 1)) ↦ F.obj (f i))
              (extendFan
                (Fan.mk (F.obj (piObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)) fun (j : Fin n) ↦
                  F.map (Pi.π (fun (i : Fin n) ↦ f i.succ) j))
                (BinaryFan.mk (P := F.obj (Limits.prod.{v, u} (f 0) (piObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)))
                  (F.map prod.fst) (F.map prod.snd)))))
          j ⟶
        Functor.obj.{0, v', 0, u'} (Discrete.functor fun (i : Fin (n + 1)) ↦ F.obj (f i)) j)
      (NatTrans.app
        (Cone.π
          (extendFan
            (Fan.mk (F.obj (piObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)) fun (j : Fin n) ↦
              F.map (Pi.π (fun (i : Fin n) ↦ f i.succ) j))
            (BinaryFan.mk (P := F.obj (Limits.prod.{v, u} (f 0) (piObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)))
              (F.map prod.fst) (F.map prod.snd))))
        j)
      (Iso.hom
          (Iso.refl
            (Cone.pt.{0, v', 0, u'} (J := Discrete (Fin (n + 1))) (F :=
              Discrete.functor fun (i : Fin (n + 1)) ↦ F.obj (f i))
              (extendFan
                (Fan.mk (F.obj (piObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)) fun (j : Fin n) ↦
                  F.map (Pi.π (fun (i : Fin n) ↦ f i.succ) j))
                (BinaryFan.mk (P := F.obj (Limits.prod.{v, u} (f 0) (piObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)))
                  (F.map prod.fst) (F.map prod.snd))))) ≫
        NatTrans.app
          (Cone.π
            (Fan.mk
              (F.obj
                (Cone.pt.{0, v, 0, u} (F :=
                  pair (f 0)
                    (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                      (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))
                  (limit.cone
                    (pair (f 0)
                      (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                        (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ)))))))
              fun (j : Fin (n + 1)) ↦
              F.map
                (Fin.cases (motive := fun (x : Fin (n + 1)) ↦
                  Cone.pt.{0, v, 0, u} (F :=
                      pair (f 0)
                        (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                          (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))
                      (limit.cone
                        (pair (f 0)
                          (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F :=
                            Discrete.functor fun (i : Fin n) ↦ f i.succ)
                            (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))) ⟶
                    f x)
                  (BinaryFan.fst
                    (limit.cone
                      (pair (f 0)
                        (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                          (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))))
                  (fun (i : Fin n) ↦
                    BinaryFan.snd
                        (limit.cone
                          (pair (f 0)
                            (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F :=
                              Discrete.functor fun (i : Fin n) ↦ f i.succ)
                              (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))) ≫
                      NatTrans.app (Cone.π (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))) { as := i })
                  j)))
          j)
⊢ Iso (C :=
    Cone.{0, v', 0, u'} (J := Discrete (Fin (n + 1))) (C := D) (Discrete.functor fun (j : Fin (n + 1)) ↦ F.obj (f j)))
    (extendFan
      (Fan.mk (F.obj (piObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)) fun (j : Fin n) ↦
        F.map (Pi.π (fun (i : Fin n) ↦ f i.succ) j))
      (BinaryFan.mk (P := F.obj (Limits.prod.{v, u} (f 0) (piObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)))
        (F.map prod.fst) (F.map prod.snd)))
    (Fan.mk
      (F.obj
        (Cone.pt.{0, v, 0, u} (F :=
          pair (f 0)
            (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
              (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))
          (limit.cone
            (pair (f 0)
              (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ)))))))
      fun (j : Fin (n + 1)) ↦
      F.map
        (Fin.cases (motive := fun (x : Fin (n + 1)) ↦
          Cone.pt.{0, v, 0, u} (F :=
              pair (f 0)
                (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                  (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))
              (limit.cone
                (pair (f 0)
                  (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                    (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))) ⟶
            f x)
          (BinaryFan.fst
            (limit.cone
              (pair (f 0)
                (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                  (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))))
          (fun (i : Fin n) ↦
            BinaryFan.snd
                (limit.cone
                  (pair (f 0)
                    (Cone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                      (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))))) ≫
              NatTrans.app (Cone.π (limit.cone (Discrete.functor fun (i : Fin n) ↦ f i.succ))) { as := i })
          j))

Tactic:
apply Cone.ext _ _

Premises used: CategoryTheory.Limits.Cone.ext