-- 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))
j : Fin (n + 1)
refine_1 :
  Eq.{v' + 1} (α :=
    Functor.obj.{0, v', 0, u'} (C := Discrete (Fin (n + 1)))
        (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)))))
        { as := 0 : Discrete (Fin (n + 1)) } ⟶
      Functor.obj.{0, v', 0, u'} (C := Discrete (Fin (n + 1))) (Discrete.functor fun (i : Fin (n + 1)) ↦ F.obj (f i))
        { as := 0 })
    (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))))
      { as := 0 })
    (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)))
        { as := 0 })
refine_2 :
  ∀ (i : Fin n),
    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)))))
            { as := i.castSucc : Discrete (Fin (n + 1)) } ⟶
          Functor.obj.{0, v', 0, u'} (Discrete.functor fun (i : Fin (n + 1)) ↦ F.obj (f i))
            { as := i.castSucc : Discrete (Fin (n + 1)) })
        (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))))
          { as := i.castSucc })
        (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)))
            { as := i.castSucc }) →
      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)))))
            { as := i.succ : Discrete (Fin (n + 1)) } ⟶
          Functor.obj.{0, v', 0, u'} (Discrete.functor fun (i : Fin (n + 1)) ↦ F.obj (f i))
            { as := i.succ : Discrete (Fin (n + 1)) })
        (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))))
          { as := i.succ })
        (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)))
            { as := i.succ })
⊢ 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)))))
        { as := j : Discrete (Fin (n + 1)) } ⟶
      Functor.obj.{0, v', 0, u'} (Discrete.functor fun (i : Fin (n + 1)) ↦ F.obj (f i))
        { as := j : Discrete (Fin (n + 1)) })
    (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))))
      { as := 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)))
        { as := j })

Tactic:
refine Fin.inductionOn j ?_ ?_