-- 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
n : ℕ
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 ⋯)) ≫
            (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)
          (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 ⋯ 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 ⋯))) ≫
          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)
⊢ 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 ⋯))))

Tactic:
apply Limits.Pi.hom_ext

Premises used: CategoryTheory.Limits.Pi.hom_ext