-- 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
s : Cone (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f))
n m : ℕ
pos :
  ∀ (h : m < n),
    Eq.{v_1 + 1} (α := s.pt ⟶ if x : m < Opposite.unop (Opposite.op n) then M m else N m)
      (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)
          (CategoryStruct.comp (Y :=
            Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f))
            (Pi.lift fun (m : ℕ) ↦
              CategoryStruct.comp (Y :=
                (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (m + 1)))
                (s.π.app (Opposite.op (m + 1))) (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯))
            (NatTrans.app (Cone.π (cone f)) (Opposite.op n)))
          (Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m) :
        s.pt ⟶ if x : m < Opposite.unop (Opposite.op n) then M m else N m)
      (s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m :
        s.pt ⟶ if x : m < Opposite.unop (Opposite.op n) then M m else N m)
⊢ Eq.{v_1 + 1} (α := s.pt ⟶ if x : m < Opposite.unop (Opposite.op n) then M m else N m)
    (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)
        (CategoryStruct.comp (Y :=
          Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f))
          (Pi.lift fun (m : ℕ) ↦
            CategoryStruct.comp (Y :=
              (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (m + 1)))
              (s.π.app (Opposite.op (m + 1))) (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯))
          (NatTrans.app (Cone.π (cone f)) (Opposite.op n)))
        (Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m) :
      s.pt ⟶ if x : m < Opposite.unop (Opposite.op n) then M m else N m)
    (s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m :
      s.pt ⟶ if x : m < Opposite.unop (Opposite.op n) then M m else N m)
have neg : ∀ (h : ¬m < n),
  Eq.{v_1 + 1} (α := s.pt ⟶ if x : m < Opposite.unop (Opposite.op n) then M m else N m)
    (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)
        (CategoryStruct.comp (Y :=
          Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f))
          (Pi.lift fun (m : ℕ) ↦
            CategoryStruct.comp (Y :=
              (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (m + 1)))
              (s.π.app (Opposite.op (m + 1))) (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom sorry))
          (NatTrans.app (Cone.π (cone f)) (Opposite.op n)))
        (Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m) :
      s.pt ⟶ if x : m < Opposite.unop (Opposite.op n) then M m else N m)
    (s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m :
      s.pt ⟶ if x : m < Opposite.unop (Opposite.op n) then M m else N m)
Tactic: by_cases h : m < n