-- 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
n : ℕ
⊢ Eq (α :=
    Functor.obj.{0, v_1, 0, u_1} (Functor.obj (Functor.const ℕᵒᵖ) (piObj.{0, v_1, u_1} M)) (Opposite.op (n + 1)) ⟶
      (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op n))
    (Functor.map (Functor.obj (Functor.const ℕᵒᵖ) (piObj.{0, v_1, u_1} M)) (Quiver.Hom.op (homOfLE ⋯)) ≫
      (fun (n : ℕ) ↦
          (Pi.map fun (m : ℕ) ↦ if h : m < n then eqToHom ⋯ else f m ≫ eqToHom ⋯ :
            piObj.{0, v_1, u_1} M ⟶
              piObj.{0, v_1, u_1} fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m))
        n)
    (CategoryStruct.comp (Y :=
      (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (n + 1)))
      ((fun (n : ℕ) ↦
          (Pi.map fun (m : ℕ) ↦ if h : m < n then eqToHom ⋯ else f m ≫ eqToHom ⋯ :
            piObj.{0, v_1, u_1} M ⟶
              piObj.{0, v_1, u_1} fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m))
        (n + 1))
      ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (Quiver.Hom.op (homOfLE ⋯))))
have h : ∀ (b : ℕ),
  Eq.{v_1 + 1} (α :=
    Functor.obj.{0, v_1, 0, u_1} (Functor.obj (Functor.const ℕᵒᵖ) (piObj.{0, v_1, u_1} M)) (Opposite.op (n + 1)) ⟶
      if x : b < Opposite.unop (Opposite.op n) then M b else N b)
    (CategoryStruct.comp (Y :=
        piObj.{0, v_1, u_1} fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m)
        (Functor.map (Functor.obj (Functor.const ℕᵒᵖ) (piObj.{0, v_1, u_1} M)) (Quiver.Hom.op (homOfLE sorry)) ≫
          (fun (n : ℕ) ↦
              (Pi.map fun (m : ℕ) ↦ if h : m < n then eqToHom sorry else f m ≫ eqToHom sorry :
                piObj.{0, v_1, u_1} M ⟶
                  piObj.{0, v_1, u_1} fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m))
            n)
        (Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) b) :
      Functor.obj.{0, v_1, 0, u_1} (Functor.obj (Functor.const ℕᵒᵖ) (piObj.{0, v_1, u_1} M)) (Opposite.op (n + 1)) ⟶
        if x : b < Opposite.unop (Opposite.op n) then M b else N b)
    (CategoryStruct.comp (Y :=
          (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (n + 1)))
          ((fun (n : ℕ) ↦
              (Pi.map fun (m : ℕ) ↦ if h : m < n then eqToHom sorry else f m ≫ eqToHom sorry :
                piObj.{0, v_1, u_1} M ⟶
                  piObj.{0, v_1, u_1} fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m))
            (n + 1))
          ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (Quiver.Hom.op (homOfLE sorry))) ≫
        Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) b :
      Functor.obj.{0, v_1, 0, u_1} (Functor.obj (Functor.const ℕᵒᵖ) (piObj.{0, v_1, u_1} M)) (Opposite.op (n + 1)) ⟶
        if x : b < Opposite.unop (Opposite.op n) then M b else N b)
Tactic: apply Limits.Pi.hom_ext