-- 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.{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 : ℕ)))))
have 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 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 : ℕ)))
        (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 : ℕ)))))
Tactic: apply +allowSynthFailures epi_comp