-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
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 : ℕ
⊢ Epi (X := functorObj.{v_1, u_1} M N (n + 1)) (functorMap f n)
have 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 sorry
            else if h' : (↑i : ℕ) < n + 1 then eqToHom sorry ≫ f (↑i : ℕ) ≫ eqToHom sorry else eqToHom sorry)
          (Pi.map fun (i : { x : ℕ // ¬x < n + 1 }) ↦
            if h : (↑i : ℕ) < n then eqToHom sorry
            else if h' : (↑i : ℕ) < n + 1 then eqToHom sorry ≫ f (↑i : ℕ) ≫ eqToHom sorry else eqToHom sorry))
        (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: rw [functorMap, Pi.map_eq_prod_map (P := fun m : ℕ ↦ m < n + 1)]