awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 m : ℕ
h : ¬m < n
zero :
  ∀ (h : ¬0 < n),
    Eq (α :=
      (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj
          (Opposite.op (HAdd.hAdd (α := ℕ) 0 1)) ⟶
        N 0)
      ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op ≫
        Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) 0 ≫ eqToHom ⋯)
      (Pi.π (fun (i : ℕ) ↦ if x : i < HAdd.hAdd (α := ℕ) 0 1 then M i else N i) 0 ≫ eqToHom ⋯ ≫ f 0)
⊢ Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (m + 1)) ⟶ N m)
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m ≫ eqToHom ⋯)
    (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯ ≫ f m)
have succ : ∀ (m : ℕ) (h : ¬m + 1 < n),
  Eq (α :=
    (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (m + 1 + 1)) ⟶ N (m + 1))
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE sorry).op ≫
      Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) (m + 1) ≫ eqToHom sorry)
    (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 + 1 then M i else N i) (m + 1) ≫ eqToHom sorry ≫ f (m + 1))
Tactic: cases m with
  | zero =>
      have : n = 0 := by lia
      subst this
      simp [functorMap]
  | succ m =>
      rw [← functorMap_commSq_succ f (m + 1)]
      simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, dite_eq_ite,
        Functor.ofOpSequence_map_homOfLE_succ]
      have : homOfLE (by lia : n ≤ m + 1 + 1) =
          homOfLE (by lia : n ≤ m + 1) ≫ homOfLE (by lia : m + 1 ≤ m + 1 + 1) := by simp
      rw [this, op_comp, Functor.map_comp]
      simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, Functor.ofOpSequence_map_homOfLE_succ,
        Category.assoc]
      congr 1
      exact functorMap_commSq_aux f (by lia) (by lia)
Cleared hypotheses: m, h
-- 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
⊢ Functor.obj (Functor.const ℕᵒᵖ) (piObj.{0, v_1, u_1} M) ⟶
    Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)
have refine : ∀ (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 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)
    (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))))
Tactic: refine NatTrans.ofOpSequence
      (fun n ↦ Limits.Pi.map fun m ↦ if h : m < n then eqToHom (functorObj_eq_pos h).symm else
        f m ≫ eqToHom (functorObj_eq_neg h).symm) (fun n ↦ ?_)
-- 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 m : ℕ
⊢ 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 : 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)
        (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) m) :
      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 : m < Opposite.unop (Opposite.op n) then M m else N m)
    (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) m :
      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 : m < Opposite.unop (Opposite.op n) then M m else N m)
have h : Eq.{v_1 + 1} (α := piObj.{0, v_1, u_1} M ⟶ if m < n then M m else N m)
  (Pi.π M m ≫ if h : m < n then eqToHom sorry else f m ≫ eqToHom sorry)
  (Pi.π M m ≫
    CategoryStruct.comp (Y := if m < n + 1 then M m else N m) (if h : m < n + 1 then eqToHom sorry else f m ≫ eqToHom sorry)
      (if h : m < n then eqToHom sorry else if h_1 : m < n + 1 then eqToHom sorry ≫ f m ≫ eqToHom sorry else eqToHom sorry))
Tactic: simp only [Functor.const_obj_obj, dite_eq_ite, Functor.ofOpSequence_obj, homOfLE_leOfHom,
      Functor.const_obj_map, Category.id_comp, Pi.map_π, Functor.ofOpSequence_map_homOfLE_succ,
      functorMap, Category.assoc, Pi.map_π_assoc]
-- 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 m : ℕ
⊢ Eq.{v_1 + 1} (α := piObj.{0, v_1, u_1} M ⟶ if m < n then M m else N m)
    (Pi.π M m ≫ if h : m < n then eqToHom ⋯ else f m ≫ eqToHom ⋯)
    (Pi.π M m ≫
      CategoryStruct.comp (Y := if m < n + 1 then M m else N m) (if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯)
        (if h : m < n then eqToHom ⋯ else if h_1 : m < n + 1 then eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ else eqToHom ⋯))
have h : ∀ (h : m < n),
  Eq.{v_1 + 1} (α := piObj.{0, v_1, u_1} M ⟶ if m < n then M m else N m) (Pi.π M m ≫ eqToHom sorry)
    (Pi.π M m ≫ (if h : m < n + 1 then eqToHom sorry else f m ≫ eqToHom sorry) ≫ eqToHom sorry)
Tactic: split
-- 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 m : ℕ
h :
  ∀ (h : m < n),
    Eq.{v_1 + 1} (α := piObj.{0, v_1, u_1} M ⟶ if m < n then M m else N m) (Pi.π M m ≫ eqToHom ⋯)
      (Pi.π M m ≫ (if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯) ≫ eqToHom ⋯)
⊢ Eq.{v_1 + 1} (α := piObj.{0, v_1, u_1} M ⟶ if m < n then M m else N m)
    (Pi.π M m ≫ if h : m < n then eqToHom ⋯ else f m ≫ eqToHom ⋯)
    (Pi.π M m ≫
      CategoryStruct.comp (Y := if m < n + 1 then M m else N m) (if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯)
        (if h : m < n then eqToHom ⋯ else if h_1 : m < n + 1 then eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ else eqToHom ⋯))
have h₁ : ∀ (h : ¬m < n),
  Eq (α := piObj.{0, v_1, u_1} M ⟶ if m < n then M m else N m) (Pi.π M m ≫ f m ≫ eqToHom sorry)
    (Pi.π M m ≫
      CategoryStruct.comp (Y := if m < n + 1 then M m else N m) (if h : m < n + 1 then eqToHom sorry else f m ≫ eqToHom sorry)
        (if h_1 : m < n + 1 then eqToHom sorry ≫ f m ≫ eqToHom sorry else eqToHom sorry))
Tactic: split
-- 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 m : ℕ
h : ¬m < n
⊢ Eq (α := piObj.{0, v_1, u_1} M ⟶ if m < n then M m else N m) (Pi.π M m ≫ f m ≫ eqToHom ⋯)
    (Pi.π M m ≫
      CategoryStruct.comp (Y := if m < n + 1 then M m else N m) (if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯)
        (if h_1 : m < n + 1 then eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ else eqToHom ⋯))
have h : ∀ (h_1 : m < n + 1),
  Eq (α := piObj.{0, v_1, u_1} M ⟶ if m < n then M m else N m) (Pi.π M m ≫ f m ≫ eqToHom sorry)
    (Pi.π M m ≫ CategoryStruct.comp (Y := if m < n + 1 then M m else N m) (eqToHom sorry) (eqToHom sorry ≫ f m ≫ eqToHom sorry))
Tactic: split
-- 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 m : ℕ
h_1 : ¬m < n
h :
  ∀ (h : m < n + 1),
    Eq (α := piObj.{0, v_1, u_1} M ⟶ if m < n then M m else N m) (Pi.π M m ≫ f m ≫ eqToHom ⋯)
      (Pi.π M m ≫ CategoryStruct.comp (Y := if m < n + 1 then M m else N m) (eqToHom ⋯) (eqToHom ⋯ ≫ f m ≫ eqToHom ⋯))
⊢ Eq (α := piObj.{0, v_1, u_1} M ⟶ if m < n then M m else N m) (Pi.π M m ≫ f m ≫ eqToHom ⋯)
    (Pi.π M m ≫
      CategoryStruct.comp (Y := if m < n + 1 then M m else N m) (if h : m < n + 1 then eqToHom ⋯ else f m ≫ eqToHom ⋯)
        (if h : m < n + 1 then eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ else eqToHom ⋯))
have h₁ : ∀ (h : ¬m < n + 1),
  Eq (α := piObj.{0, v_1, u_1} M ⟶ if m < n then M m else N m) (Pi.π M m ≫ f m ≫ eqToHom sorry)
    (Pi.π M m ≫ (f m ≫ eqToHom sorry) ≫ eqToHom sorry)
Tactic: split
-- 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
m n : ℕ
h : n < m
⊢ Eq (α :=
    Functor.obj.{0, v_1, 0, u_1}
        (Functor.obj (Functor.const ℕᵒᵖ)
          (Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f)))
        (Opposite.op m) ⟶
      if x : n < m then M n else N n)
    (NatTrans.app (Cone.π (cone f)) (Opposite.op m) ≫ Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) n)
    (Pi.π M n ≫ eqToHom ⋯)
have simp : Eq.{v_1 + 1} (α :=
  Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f) ⟶
    if n < m then M n else N n)
  (Pi.π (fun (m : ℕ) ↦ M m) n ≫ if h : n < m then eqToHom sorry else f n ≫ eqToHom sorry) (Pi.π M n ≫ eqToHom sorry)
Tactic: simp only [Functor.const_obj_obj, dite_eq_ite, Functor.ofOpSequence_obj, cone_π_app, Pi.map_π]
-- 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
m n : ℕ
h : n < m
⊢ Eq.{v_1 + 1} (α :=
    Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f) ⟶
      if n < m then M n else N n)
    (Pi.π (fun (m : ℕ) ↦ M m) n ≫ if h : n < m then eqToHom ⋯ else f n ≫ eqToHom ⋯) (Pi.π M n ≫ eqToHom ⋯)
have rw : Eq.{v_1 + 1} (α :=
  Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f) ⟶
    if n < m then M n else N n)
  (Pi.π (fun (m : ℕ) ↦ M m) n ≫ eqToHom sorry) (Pi.π M n ≫ eqToHom sorry)
Tactic: rw [dif_pos h]
-- 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
m n : ℕ
h : ¬n < m
⊢ Eq (α :=
    Functor.obj.{0, v_1, 0, u_1}
        (Functor.obj (Functor.const ℕᵒᵖ)
          (Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f)))
        (Opposite.op m) ⟶
      if x : n < Opposite.unop (Opposite.op m) then M n else N n)
    (NatTrans.app (Cone.π (cone f)) (Opposite.op m) ≫
      Pi.π (fun (m_1 : ℕ) ↦ if x : m_1 < Opposite.unop (Opposite.op m) then M m_1 else N m_1) n)
    (Pi.π M n ≫ f n ≫ eqToHom ⋯)
have simp : Eq (α :=
  Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f) ⟶
    if n < m then M n else N n)
  (Pi.π (fun (m : ℕ) ↦ M m) n ≫ if h : n < m then eqToHom sorry else f n ≫ eqToHom sorry) (Pi.π M n ≫ f n ≫ eqToHom sorry)
Tactic: simp only [Functor.const_obj_obj, dite_eq_ite, Functor.ofOpSequence_obj, cone_π_app, Pi.map_π]
-- 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
m n : ℕ
h : ¬n < m
⊢ Eq (α :=
    Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f) ⟶
      if n < m then M n else N n)
    (Pi.π (fun (m : ℕ) ↦ M m) n ≫ if h : n < m then eqToHom ⋯ else f n ≫ eqToHom ⋯) (Pi.π M n ≫ f n ≫ eqToHom ⋯)
have rw : Eq (α :=
  Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f) ⟶
    if n < m then M n else N n)
  (Pi.π (fun (m : ℕ) ↦ M m) n ≫ f n ≫ eqToHom sorry) (Pi.π M n ≫ f n ≫ eqToHom sorry)
Tactic: rw [dif_neg h]
-- 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 : ℕ
⊢ Eq (α := s.pt ⟶ (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op n))
    (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)))
    (s.π.app (Opposite.op n))
have h : ∀ (b : ℕ),
  Eq.{v_1 + 1} (α := s.pt ⟶ 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)
        (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) b) :
      s.pt ⟶ if x : b < Opposite.unop (Opposite.op n) then M b else N b)
    (s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) b :
      s.pt ⟶ if x : b < Opposite.unop (Opposite.op n) then M b else N b)
Tactic: apply Pi.hom_ext
-- 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 : ℕ
⊢ 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 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 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
-- 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 : ℕ
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)
have pos : 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))
    (Pi.π M m ≫ eqToHom sorry) =
  s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if x : m < n then M m else N m) m
Tactic: simp only [Category.assoc, cone_π_app_comp_Pi_π_pos f _ _ h]
-- 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 : ℕ
h : m < n
⊢ 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 ⋯))
      (Pi.π M m ≫ eqToHom ⋯) =
    s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if x : m < n then M m else N m) m
have pos : Eq (α := s.pt ⟶ if m < n then M m else N m)
  (CategoryStruct.comp (Y := functorObj.{v_1, u_1} M N (m + 1)) (s.π.app (Opposite.op (m + 1)))
    (Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) m ≫ eqToHom sorry))
  (s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m)
Tactic: simp only [dite_eq_ite, Functor.ofOpSequence_obj, limit.lift_π_assoc, Fan.mk_pt,
        Discrete.functor_obj_eq_as, Fan.mk_π_app, Category.assoc, eqToHom_trans]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (hypothesis)
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 : ℕ
h : m < n
⊢ Eq (α := s.pt ⟶ if m < n then M m else N m)
    (CategoryStruct.comp (Y := functorObj.{v_1, u_1} M N (m + 1)) (s.π.app (Opposite.op (m + 1)))
      (Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯))
    (s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m)
have hh : m + 1 ≤ n
Tactic: have hh : m + 1 ≤ n := by lia
-- 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 : ℕ
h : m < n
hh : m + 1 ≤ n
⊢ Eq (α := s.pt ⟶ if m < n then M m else N m)
    (CategoryStruct.comp (Y := functorObj.{v_1, u_1} M N (m + 1)) (s.π.app (Opposite.op (m + 1)))
      (Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯))
    (s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m)
have pos : (s.π.app (Opposite.op n) ≫ (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE hh).op) ≫
    Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) m ≫ eqToHom sorry =
  s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m
Tactic: rw [← s.w (homOfLE hh).op]