awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 m : ℕ
h : ¬m + 1 < n
succ :
  Eq (α := functorObj.{v_1, u_1} M N (m + 1 + 1) ⟶ N (m + 1))
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom ⋯)
    (functorMap f (m + 1) ≫ Pi.π (fun (m_1 : ℕ) ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯)
⊢ 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 ⋯).op ≫
      Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) (m + 1) ≫ eqToHom ⋯)
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (Quiver.Hom.op (homOfLE ⋯)) ≫
      Pi.π (fun (m_1 : ℕ) ↦ if x : m_1 < Opposite.unop (Opposite.op (m + 1)) then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯)

Tactic:
simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, dite_eq_ite,
        Functor.ofOpSequence_map_homOfLE_succ]

Premises used: CategoryTheory.Functor.ofOpSequence_obj, CategoryTheory.homOfLE_leOfHom, CategoryTheory.Functor.ofOpSequence_map_homOfLE_succ, dite_eq_ite
-- 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 m : ℕ
h : ¬m + 1 < n
⊢ n ≤ m + 1 + 1

Tactic:
lia
-- 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 m : ℕ
h : ¬m + 1 < n
⊢ n ≤ m + 1

Tactic:
lia
-- 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 m : ℕ
h : ¬m + 1 < n
⊢ m + 1 ≤ m + 1 + 1

Tactic:
lia
-- 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 m : ℕ
h : ¬m + 1 < n
⊢ homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯

Tactic:
simp
-- 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 m : ℕ
h : ¬m + 1 < n
⊢ homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯

Tactic:
have : homOfLE (by lia : n ≤ m + 1 + 1) =
          homOfLE (by lia : n ≤ m + 1) ≫ homOfLE (by lia : m + 1 ≤ m + 1 + 1) := by simp
-- 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 m : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
succ :
  Eq (α := functorObj.{v_1, u_1} M N (m + 1 + 1) ⟶ N (m + 1))
    (((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op ≫
        (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op) ≫
      Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom ⋯)
    (functorMap f (m + 1) ≫ Pi.π (fun (m_1 : ℕ) ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯)
⊢ Eq (α := functorObj.{v_1, u_1} M N (m + 1 + 1) ⟶ N (m + 1))
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom ⋯)
    (functorMap f (m + 1) ≫ Pi.π (fun (m_1 : ℕ) ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯)

Tactic:
rw [this, op_comp, Functor.map_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp
-- 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 m : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
succ :
  Eq (α := functorObj.{v_1, u_1} M N (m + 1 + 1) ⟶ N (m + 1))
    (functorMap f (m + 1) ≫
      (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op ≫
        Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom ⋯)
    (functorMap f (m + 1) ≫ Pi.π (fun (m_1 : ℕ) ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯)
⊢ Eq (α := functorObj.{v_1, u_1} M N (m + 1 + 1) ⟶ N (m + 1))
    (((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op ≫
        (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op) ≫
      Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom ⋯)
    (functorMap f (m + 1) ≫ Pi.π (fun (m_1 : ℕ) ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯)

Tactic:
simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, Functor.ofOpSequence_map_homOfLE_succ,
        Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.ofOpSequence_obj, CategoryTheory.homOfLE_leOfHom, CategoryTheory.Functor.ofOpSequence_map_homOfLE_succ
-- 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 m : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
succ :
  Eq (α := functorObj.{v_1, u_1} M N (m + 1) ⟶ N (m + 1))
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom ⋯)
    (Pi.π (fun (m_1 : ℕ) ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯)
⊢ Eq (α := functorObj.{v_1, u_1} M N (m + 1 + 1) ⟶ N (m + 1))
    (functorMap f (m + 1) ≫
      (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op ≫
        Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom ⋯)
    (functorMap f (m + 1) ≫ Pi.π (fun (m_1 : ℕ) ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯)

Tactic:
congr 1
-- 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 m : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ n ≤ m + 1

Tactic:
lia
-- 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 m : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ ¬m + 1 < m + 1

Tactic:
lia
-- 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 m : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ Eq (α := functorObj.{v_1, u_1} M N (m + 1) ⟶ N (m + 1))
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom ⋯)
    (Pi.π (fun (m_1 : ℕ) ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom ⋯)

Tactic:
exact functorMap_commSq_aux f (by lia) (by lia)

Premises used: CategoryTheory.Limits.SequentialProduct.functorMap_commSq_aux
-- 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 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)
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 ⋯).op ≫
        Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) (m + 1) ≫ eqToHom ⋯)
      (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 + 1 then M i else N i) (m + 1) ≫ eqToHom ⋯ ≫ f (m + 1))
⊢ 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)

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)

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Limits.SequentialProduct.functorMap_commSq_aux, CategoryTheory.Functor.ofOpSequence_obj, CategoryTheory.homOfLE_leOfHom, CategoryTheory.Functor.ofOpSequence_map_homOfLE_succ, HAdd.hAdd, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.SequentialProduct.functorMap, dite_eq_ite, CategoryTheory.Limits.SequentialProduct.functorMap_commSq_succ, OfNat.ofNat
-- 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
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 ⋯)) ≫
        (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 ⋯))))
⊢ Functor.obj (Functor.const ℕᵒᵖ) (piObj.{0, v_1, u_1} M) ⟶
    Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)

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 ↦ ?_)

Premises used: CategoryTheory.NatTrans.ofOpSequence
-- 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 m : ℕ
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 ⋯ 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 ⋯))
⊢ 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)

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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.ofOpSequence_obj, CategoryTheory.homOfLE_leOfHom, CategoryTheory.Functor.ofOpSequence_map_homOfLE_succ, CategoryTheory.Limits.Pi.map_π_assoc, CategoryTheory.Limits.SequentialProduct.functorMap, CategoryTheory.Functor.const_obj_obj, dite_eq_ite, CategoryTheory.Functor.const_obj_map, CategoryTheory.Limits.Pi.map_π, CategoryTheory.Category.id_comp
-- 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 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 ⋯)
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 ⋯)
      (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 ⋯))
⊢ 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 ⋯))

Tactic:
split
-- 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 m : ℕ
h : m < n
⊢ m < n + 1

Tactic:
lia
-- 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 m : ℕ
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 ⋯)

Tactic:
simp [dif_pos (by lia : m < n + 1)]

Premises used: dif_pos
-- 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 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 ⋯))
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 ≫ (f m ≫ eqToHom ⋯) ≫ 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 ⋯))

Tactic:
split
-- 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 m : ℕ
h : ¬m < n
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 ⋯)
    (Pi.π M m ≫ CategoryStruct.comp (Y := if m < n + 1 then M m else N m) (eqToHom ⋯) (eqToHom ⋯ ≫ f m ≫ eqToHom ⋯))

Tactic:
simp
-- 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 m : ℕ
h : ¬m < n
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 ⋯)
    (Pi.π M m ≫ (f m ≫ eqToHom ⋯) ≫ eqToHom ⋯)

Tactic:
simp
-- 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 : ℕ
⊢ 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 n) ⟶
      (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op n))
    (NatTrans.app (Cone.π (cone f)) (Opposite.op n))
    (Pi.map fun (m : ℕ) ↦ if h : m < n then eqToHom ⋯ else f m ≫ eqToHom ⋯)

Tactic:
rfl

Premises used: CategoryTheory.Limits.IsLimit.map, CategoryTheory.Limits.limMap, rfl, CategoryTheory.Limits.Pi.map
-- 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
m n : ℕ
h : n < m
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 ⋯ else f n ≫ eqToHom ⋯) (Pi.π M n ≫ eqToHom ⋯)
⊢ 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 ⋯)

Tactic:
simp only [Functor.const_obj_obj, dite_eq_ite, Functor.ofOpSequence_obj, cone_π_app, Pi.map_π]

Premises used: CategoryTheory.Functor.ofOpSequence_obj, CategoryTheory.Functor.const_obj_obj, dite_eq_ite, CategoryTheory.Limits.SequentialProduct.cone_π_app, CategoryTheory.Limits.Pi.map_π
-- 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
m n : ℕ
h : n < m
rw 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 ⋯) (Pi.π M n ≫ eqToHom ⋯)
⊢ 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 ⋯)

Tactic:
rw [dif_pos h]

Premises used: dif_pos
-- 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
m n : ℕ
h : ¬n < m
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 ⋯ else f n ≫ eqToHom ⋯) (Pi.π M n ≫ f n ≫ eqToHom ⋯)
⊢ 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 ⋯)

Tactic:
simp only [Functor.const_obj_obj, dite_eq_ite, Functor.ofOpSequence_obj, cone_π_app, Pi.map_π]

Premises used: CategoryTheory.Functor.ofOpSequence_obj, CategoryTheory.Functor.const_obj_obj, dite_eq_ite, CategoryTheory.Limits.SequentialProduct.cone_π_app, CategoryTheory.Limits.Pi.map_π
-- 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
m n : ℕ
h : ¬n < m
rw 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 ⋯) (Pi.π M n ≫ f n ≫ eqToHom ⋯)
⊢ 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 ⋯)

Tactic:
rw [dif_neg h]

Premises used: dif_neg
-- 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
s : Cone (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f))
m : ℕ
⊢ m < m + 1

Tactic:
lia