-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst_1 : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_2 : HasCountableProducts.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
inst_5 : ∀ (n : ℕ), Epi (f n)
n : ℕ
inst :
  Epi.{v_1, u_1} (C := C) (X :=
    Cone.pt.{0, v_1, 0, u_1} (F :=
      pair
        (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
        (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
          if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ)))
      (BinaryFan.mk (P :=
        prod.{v_1, u_1}
          (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦
            if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
          (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
            if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ)))
        prod.fst prod.snd))
    (Y := functorObj.{v_1, u_1} M N n)
    (CategoryStruct.comp (Y :=
        prod.{v_1, u_1}
          (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
          (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ)))
        (prod.map
          (Pi.map fun (i : { x : ℕ // x < n + 1 }) ↦
            if h : (↑i : ℕ) < n then eqToHom ⋯
            else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯)
          (Pi.map fun (i : { x : ℕ // ¬x < n + 1 }) ↦
            if h : (↑i : ℕ) < n then eqToHom ⋯
            else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯))
        (Iso.inv
          (IsLimit.conePointUniqueUpToIso
            (Pi.binaryFanOfPropIsLimit (fun (m : ℕ) ↦ if x : m < n then M m else N m) fun (m : ℕ) ↦ m < n + 1)
            (prodIsProd
              (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦
                if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
              (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
                if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))))) :
      Quiver.Hom.{v_1, u_1} (V := C)
        (Cone.pt.{0, v_1, 0, u_1} (F :=
          pair
            (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦
              if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
            (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
              if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ)))
          (BinaryFan.mk (P :=
            prod.{v_1, u_1}
              (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦
                if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
              (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
                if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ)))
            prod.fst prod.snd))
        (Cone.pt.{0, v_1, 0, u_1} (F :=
          pair
            (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
            (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
              if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ)))
          (Pi.binaryFanOfProp.{v_1, u_1, 0} (C := C) (fun (m : ℕ) ↦ if x : m < n then M m else N m) fun (m : ℕ) ↦
              m < n + 1 :
            BinaryFan.{v_1, u_1} (C := C)
              (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦
                if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
              (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
                if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ)))))
⊢ Epi.{v_1, u_1} (C := C) (X := functorObj.{v_1, u_1} M N (n + 1)) (Y := functorObj.{v_1, u_1} M N n)
    (CategoryStruct.comp (Y :=
        Cone.pt.{0, v_1, 0, u_1} (F :=
          pair
            (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦
              if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
            (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
              if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ)))
          (BinaryFan.mk (P :=
            prod.{v_1, u_1}
              (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦
                if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
              (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
                if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ)))
            prod.fst prod.snd))
        (Iso.hom
          (IsLimit.conePointUniqueUpToIso
            (Pi.binaryFanOfPropIsLimit (fun (m : ℕ) ↦ if x : m < n + 1 then M m else N m) fun (m : ℕ) ↦ m < n + 1)
            (prodIsProd
              (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦
                if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
              (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
                if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ)))))
        (CategoryStruct.comp (Y :=
          prod.{v_1, u_1}
            (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
            (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
              if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ)))
          (prod.map
            (Pi.map fun (i : { x : ℕ // x < n + 1 }) ↦
              if h : (↑i : ℕ) < n then eqToHom ⋯
              else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯)
            (Pi.map fun (i : { x : ℕ // ¬x < n + 1 }) ↦
              if h : (↑i : ℕ) < n then eqToHom ⋯
              else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯))
          (Iso.inv
            (IsLimit.conePointUniqueUpToIso
              (Pi.binaryFanOfPropIsLimit (fun (m : ℕ) ↦ if x : m < n then M m else N m) fun (m : ℕ) ↦ m < n + 1)
              (prodIsProd
                (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦
                  if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
                (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
                  if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ)))))) :
      Quiver.Hom.{v_1, u_1} (V := C)
        (Cone.pt.{0, v_1, 0, u_1} (F :=
          pair
            (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦
              if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
            (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
              if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ)))
          (Pi.binaryFanOfProp.{v_1, u_1, 0} (C := C) (fun (m : ℕ) ↦ if x : m < n + 1 then M m else N m) fun (m : ℕ) ↦
              m < n + 1 :
            BinaryFan.{v_1, u_1} (C := C)
              (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦
                if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
              (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
                if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))))
        (Cone.pt.{0, v_1, 0, u_1} (F :=
          pair
            (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
            (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
              if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ)))
          (Pi.binaryFanOfProp.{v_1, u_1, 0} (C := C) (fun (m : ℕ) ↦ if x : m < n then M m else N m) fun (m : ℕ) ↦
              m < n + 1 :
            BinaryFan.{v_1, u_1} (C := C)
              (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦
                if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
              (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
                if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ)))))

Tactic:
apply +allowSynthFailures epi_comp

Premises used: CategoryTheory.epi_comp