-- Module: Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasFiniteBiproducts.{v_1, u_1} C
inst_4 : ∀ (n : ℕ), Epi (f n)
n : ℕ
rw :
  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 : ℕ)))))
⊢ Epi (X := functorObj.{v_1, u_1} M N (n + 1)) (functorMap f n)

Tactic:
rw [functorMap, Pi.map_eq_prod_map (P := fun m : ℕ ↦ m < n + 1)]

Premises used: CategoryTheory.Limits.Pi.map_eq_prod_map, HAdd.hAdd, LT.lt, CategoryTheory.Limits.SequentialProduct.functorMap, OfNat.ofNat