-- Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
Goal:
J : Type v
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Fan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryFan.{v, u} (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone.{0, v, 0, u} (Discrete.functor f)
x : Discrete (Fin (n + 1))
j : Fin (n + 1)
refine_1 :
  (↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 : Discrete (Fin (n + 1)) })
            (t₁.lift
              { pt := s.pt,
                π :=
                  Discrete.natTrans fun (x : Discrete (Fin n)) ↦
                    match (motive :=
                      (x : Discrete (Fin n)) →
                        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete (Fin n))) s.pt) x ⟶
                          Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) x)
                      x with
                    | { as := i } => s.π.app { as := i.succ : Discrete (Fin (n + 1)) } :
                Cone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
        ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 } ⟶ c₂.pt) ≫
      (extendFan c₁ c₂).π.app { as := 0 } =
    s.π.app { as := 0 : Discrete (Fin (n + 1)) }
refine_2 :
  ∀ (i : Fin n),
    (↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 : Discrete (Fin (n + 1)) })
                (t₁.lift
                  { pt := s.pt,
                    π :=
                      Discrete.natTrans fun (x : Discrete (Fin n)) ↦
                        match (motive :=
                          (x : Discrete (Fin n)) →
                            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete (Fin n))) s.pt) x ⟶
                              Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) x)
                          x with
                        | { as := i } => s.π.app { as := i.succ : Discrete (Fin (n + 1)) } :
                    Cone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C)
                      (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
            ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 } ⟶ c₂.pt) ≫
          (extendFan c₁ c₂).π.app { as := i.castSucc } =
        s.π.app { as := i.castSucc : Discrete (Fin (n + 1)) } →
      (↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 : Discrete (Fin (n + 1)) })
                (t₁.lift
                  { pt := s.pt,
                    π :=
                      Discrete.natTrans fun (x : Discrete (Fin n)) ↦
                        match (motive :=
                          (x : Discrete (Fin n)) →
                            Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete (Fin n))) s.pt) x ⟶
                              Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) x)
                          x with
                        | { as := i } => s.π.app { as := i.succ : Discrete (Fin (n + 1)) } :
                    Cone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C)
                      (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
            ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 } ⟶ c₂.pt) ≫
          (extendFan c₁ c₂).π.app { as := i.succ } =
        s.π.app { as := i.succ : Discrete (Fin (n + 1)) }
⊢ (↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 : Discrete (Fin (n + 1)) })
            (t₁.lift
              { pt := s.pt,
                π :=
                  Discrete.natTrans fun (x : Discrete (Fin n)) ↦
                    match (motive :=
                      (x : Discrete (Fin n)) →
                        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete (Fin n))) s.pt) x ⟶
                          Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : Fin n) ↦ f i.succ) x)
                      x with
                    | { as := i } => s.π.app { as := i.succ : Discrete (Fin (n + 1)) } :
                Cone.{0, v, 0, u} (J := Discrete (Fin n)) (C := C) (Discrete.functor fun (i : Fin n) ↦ f i.succ) })) :
        ((Functor.const (Discrete (Fin (n + 1)))).obj s.pt).obj { as := 0 } ⟶ c₂.pt) ≫
      (extendFan c₁ c₂).π.app { as := j } =
    s.π.app { as := j : Discrete (Fin (n + 1)) }

Tactic:
refine Fin.inductionOn j ?_ ?_