-- 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 :=
    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 : ℕ)))))
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 :=
  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))
Tactic: apply +allowSynthFailures epi_comp