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
s : Cone (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f))
n_1 m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < 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 ⋯ =
      Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : Eq.{u_1 + 1} (α := C) (if x : m < m + 1 then M m else N m) (if x : m < n then M m else N m)
h₂ : Eq.{u_1 + 1} (α := C) (if x : m < n then M m else N m) (if x : m < n + 1 then M m else N m)
pos :
  Eq (α := functorObj.{v_1, u_1} M N (n + 1) ⟶ if m < n + 1 then M m else N m)
    (functorMap f n ≫ Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m ≫ eqToHom h₂)
    (Pi.π (fun (m : ℕ) ↦ if m < n + 1 then M m else N m) m)
⊢ Eq (α := functorObj.{v_1, u_1} M N (n + 1) ⟶ if m < n + 1 then M m else N m)
    (functorMap f 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 h₁ ≫ eqToHom h₂)
    (Pi.π (fun (m : ℕ) ↦ if m < n + 1 then M m else N m) m)

Tactic:
slice_lhs 2 4 => rw [ih (by 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
s : Cone (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f))
n_1 m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < 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 ⋯ =
      Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : Eq.{u_1 + 1} (α := C) (if x : m < m + 1 then M m else N m) (if x : m < n then M m else N m)
h₂ : Eq.{u_1 + 1} (α := C) (if x : m < n then M m else N m) (if x : m < n + 1 then M m else N m)
pos :
  Eq.{v_1 + 1} (α := functorObj.{v_1, u_1} M N (n + 1) ⟶ if m < n + 1 then M m else N m)
    (limit.π (Discrete.functor fun (m : ℕ) ↦ if m < n + 1 then M m else N m) { as := m : Discrete ℕ } ≫
      (if h : m < n then eqToHom ⋯ else if h_1 : m < n + 1 then eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ else eqToHom ⋯) ≫
        eqToHom h₂)
    (limit.π (Discrete.functor fun (m : ℕ) ↦ if m < n + 1 then M m else N m) { as := m })
⊢ Eq (α := functorObj.{v_1, u_1} M N (n + 1) ⟶ if m < n + 1 then M m else N m)
    (functorMap f n ≫ Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m ≫ eqToHom h₂)
    (Pi.π (fun (m : ℕ) ↦ if m < n + 1 then M m else N m) m)

Tactic:
simp only [functorMap, dite_eq_ite, Pi.π, Pi.map_π_assoc]

Premises used: CategoryTheory.Limits.Pi.π, CategoryTheory.Limits.Pi.map_π_assoc, CategoryTheory.Limits.SequentialProduct.functorMap, 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
s : Cone (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f))
n_1 m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < 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 ⋯ =
      Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : Eq.{u_1 + 1} (α := C) (if x : m < m + 1 then M m else N m) (if x : m < n then M m else N m)
h₂ : Eq.{u_1 + 1} (α := C) (if x : m < n then M m else N m) (if x : m < n + 1 then M m else N m)
pos :
  Eq.{v_1 + 1} (α := functorObj.{v_1, u_1} M N (n + 1) ⟶ if m < n + 1 then M m else N m)
    (limit.π (Discrete.functor fun (m : ℕ) ↦ if m < n + 1 then M m else N m) { as := m : Discrete ℕ } ≫
      (if h : m < n then eqToHom ⋯ else eqToHom ⋯ ≫ f m ≫ eqToHom ⋯) ≫ eqToHom h₂)
    (limit.π (Discrete.functor fun (m : ℕ) ↦ if m < n + 1 then M m else N m) { as := m })
⊢ Eq.{v_1 + 1} (α := functorObj.{v_1, u_1} M N (n + 1) ⟶ if m < n + 1 then M m else N m)
    (limit.π (Discrete.functor fun (m : ℕ) ↦ if m < n + 1 then M m else N m) { as := m : Discrete ℕ } ≫
      (if h : m < n then eqToHom ⋯ else if h_1 : m < n + 1 then eqToHom ⋯ ≫ f m ≫ eqToHom ⋯ else eqToHom ⋯) ≫
        eqToHom h₂)
    (limit.π (Discrete.functor fun (m : ℕ) ↦ if m < n + 1 then M m else N m) { as := m })

Tactic:
split_ifs
-- 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))
n_1 m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < 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 ⋯ =
      Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : Eq.{u_1 + 1} (α := C) (if x : m < m + 1 then M m else N m) (if x : m < n then M m else N m)
h₂ : Eq.{u_1 + 1} (α := C) (if x : m < n then M m else N m) (if x : m < n + 1 then M m else N m)
pos :
  Eq.{v_1 + 1} (α := functorObj.{v_1, u_1} M N (n + 1) ⟶ if m < n + 1 then M m else N m)
    (limit.π (Discrete.functor fun (m : ℕ) ↦ if m < n + 1 then M m else N m) { as := m : Discrete ℕ } ≫
      eqToHom ⋯ ≫ eqToHom h₂)
    (limit.π (Discrete.functor fun (m : ℕ) ↦ if m < n + 1 then M m else N m) { as := m })
⊢ Eq.{v_1 + 1} (α := functorObj.{v_1, u_1} M N (n + 1) ⟶ if m < n + 1 then M m else N m)
    (limit.π (Discrete.functor fun (m : ℕ) ↦ if m < n + 1 then M m else N m) { as := m : Discrete ℕ } ≫
      (if h : m < n then eqToHom ⋯ else eqToHom ⋯ ≫ f m ≫ eqToHom ⋯) ≫ eqToHom h₂)
    (limit.π (Discrete.functor fun (m : ℕ) ↦ if m < n + 1 then M m else N m) { as := m })

Tactic:
rw [dif_pos (by lia)]

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
s : Cone (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f))
n_1 m n : ℕ
hh : m + 1 ≤ n
ih :
  ∀ (h : m < 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 ⋯ =
      Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m
h : m < n + 1
this : homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯
h₁ : Eq.{u_1 + 1} (α := C) (if x : m < m + 1 then M m else N m) (if x : m < n then M m else N m)
h₂ : Eq.{u_1 + 1} (α := C) (if x : m < n then M m else N m) (if x : m < n + 1 then M m else N m)
⊢ Eq.{v_1 + 1} (α := functorObj.{v_1, u_1} M N (n + 1) ⟶ if m < n + 1 then M m else N m)
    (limit.π (Discrete.functor fun (m : ℕ) ↦ if m < n + 1 then M m else N m) { as := m : Discrete ℕ } ≫
      eqToHom ⋯ ≫ eqToHom h₂)
    (limit.π (Discrete.functor fun (m : ℕ) ↦ if m < n + 1 then M m else N m) { as := m })

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
s : Cone (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f))
n m : ℕ
h : m < n
hh : m + 1 ≤ n
pos :
  ∀ (h : m < m + 1),
    Eq (α := functorObj.{v_1, u_1} M N (m + 1) ⟶ if m < m + 1 then M m else N m)
      ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (Quiver.Hom.op (homOfLE ⋯)) ≫
        Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯)
      (Pi.π (fun (m_1 : ℕ) ↦ if m_1 < m + 1 then M m_1 else N m_1) m)
pos₁ :
  ∀ ⦃n : ℕ⦄ (hh : m + 1 ≤ n)
    (ih :
      ∀ (h : m < 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 ⋯ =
          Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m)
    (h : m < n + 1),
    (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op ≫
        Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ =
      Pi.π (fun (m : ℕ) ↦ if m < n + 1 then M m else N m) m
⊢ (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 ⋯ =
    Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m

Tactic:
induction hh using Nat.leRec with
      | refl => simp
      | @le_succ_of_le n hh ih =>
        have : homOfLE (Nat.le_succ_of_le hh) = homOfLE hh ≫ homOfLE (Nat.le_succ n) := by simp
        rw [this, op_comp, Functor.map_comp]
        simp only [Functor.ofOpSequence_obj, Nat.succ_eq_add_one, homOfLE_leOfHom,
          Functor.ofOpSequence_map_homOfLE_succ, Category.assoc]
        have h₁ : (if _ : m < m + 1 then M m else N m) = if _ : m < n then M m else N m := by
          rw [dif_pos (by lia), dif_pos (by lia)]
        have h₂ : (if _ : m < n then M m else N m) = if _ : m < n + 1 then M m else N m := by
          rw [dif_pos h, dif_pos (by lia)]
        rw [← eqToHom_trans h₁ h₂]
        slice_lhs 2 4 => rw [ih (by lia)]
        simp only [functorMap, dite_eq_ite, Pi.π, Pi.map_π_assoc]
        split_ifs
        rw [dif_pos (by lia)]
        simp

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, Nat.succ_eq_add_one, CategoryTheory.Limits.Pi.π, CategoryTheory.Functor.ofOpSequence_obj, dif_pos, CategoryTheory.homOfLE_leOfHom, CategoryTheory.Functor.ofOpSequence_map_homOfLE_succ, CategoryTheory.Limits.Pi.map_π_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.SequentialProduct.functorMap, dite_eq_ite, refl
-- 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))
n m : ℕ
h : ¬m < n
neg :
  Eq (α := s.pt ⟶ if x : m < 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 ⋯))
      (CategoryStruct.comp (Y := piObj.{0, v_1, u_1} fun (m : ℕ) ↦ if x : m < n then M m else N m)
        (NatTrans.app (Cone.π (cone f)) (Opposite.op n)) (Pi.π (fun (m : ℕ) ↦ if x : m < n then M m else N m) m)))
    (s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if x : m < n then M m else N m) 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)

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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))
n m : ℕ
h : ¬m < n
neg :
  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 ≫ f m ≫ eqToHom ⋯) =
    s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if x : m < n then M m else N m) m
⊢ Eq (α := s.pt ⟶ if x : m < 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 ⋯))
      (CategoryStruct.comp (Y := piObj.{0, v_1, u_1} fun (m : ℕ) ↦ if x : m < n then M m else N m)
        (NatTrans.app (Cone.π (cone f)) (Opposite.op n)) (Pi.π (fun (m : ℕ) ↦ if x : m < n then M m else N m) m)))
    (s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if x : m < n then M m else N m) m)

Tactic:
rw [cone_π_app_comp_Pi_π_neg f _ _ h]

Premises used: CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_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))
n m : ℕ
h : ¬m < n
neg :
  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 ⋯ ≫ f m ≫ eqToHom ⋯))
    (s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) 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 ⋯))
      (Pi.π M m ≫ f m ≫ eqToHom ⋯) =
    s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if x : 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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.ofOpSequence_obj, CategoryTheory.Discrete.functor_obj_eq_as, CategoryTheory.Limits.Fan.mk_pt, CategoryTheory.Limits.limit.lift_π_assoc, dite_eq_ite, CategoryTheory.Limits.Fan.mk_π_app
-- 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))
n m : ℕ
h : ¬m < n
a :
  (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op ≫
    Pi.π (fun (m : ℕ) ↦ if x : m < n then M m else N m) m ≫ eqToHom ⋯
| Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ ≫ f m

Tactic:
simp only [← dite_eq_ite, ← functorMap_commSq f h]

Premises used: dite_eq_ite, CategoryTheory.Limits.SequentialProduct.functorMap_commSq
-- 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))
n m : ℕ
h : ¬m < n
neg :
  Eq (α := s.pt ⟶ if m < n then M m else N m)
    (s.π.app (Opposite.op (m + 1)) ≫
      ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op ≫
          Pi.π (fun (m : ℕ) ↦ if x : m < n then M m else N m) m ≫ eqToHom ⋯) ≫
        eqToHom ⋯)
    (s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m)
⊢ 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 ⋯ ≫ f m ≫ eqToHom ⋯))
    (s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m)

Tactic:
slice_lhs 2 4 => simp only [← dite_eq_ite, ← functorMap_commSq f h]

Premises used: dite_eq_ite, CategoryTheory.Limits.SequentialProduct.functorMap_commSq
-- 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))
n m : ℕ
h : ¬m < n
⊢ Eq (α := s.pt ⟶ if m < n then M m else N m)
    (s.π.app (Opposite.op (m + 1)) ≫
      ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op ≫
          Pi.π (fun (m : ℕ) ↦ if x : m < n then M m else N m) m ≫ eqToHom ⋯) ≫
        eqToHom ⋯)
    (s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m)

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
s : Cone (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f))
m : s.pt ⟶ Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f)
h : ∀ (j : ℕᵒᵖ), m ≫ NatTrans.app (Cone.π (cone f)) j = s.π.app j
h₁ :
  ∀ (b : ℕ),
    m ≫ Pi.π M b =
      CategoryStruct.comp (Y := piObj.{0, v_1, u_1} M)
        (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 b)
⊢ m =
    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 ⋯)

Tactic:
apply Pi.hom_ext

Premises used: CategoryTheory.Limits.Pi.hom_ext
-- 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 : s.pt ⟶ Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f)
h : ∀ (j : ℕᵒᵖ), m ≫ NatTrans.app (Cone.π (cone f)) j = s.π.app j
n : ℕ
h₁ :
  m ≫ Pi.π M n =
    m ≫
      CategoryStruct.comp (Y := functorObj.{v_1, u_1} M N (n + 1))
        (NatTrans.app (Cone.π (cone f)) (Opposite.op (n + 1)))
        (Pi.π (fun (i : ℕ) ↦ if i < n + 1 then M i else N i) n ≫ eqToHom ⋯)
⊢ m ≫ Pi.π M n =
    CategoryStruct.comp (Y := piObj.{0, v_1, u_1} M)
      (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 n)

Tactic:
simp only [Functor.ofOpSequence_obj, dite_eq_ite, limit.lift_π, Fan.mk_pt,
      Fan.mk_π_app, ← h ⟨n + 1⟩, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.ofOpSequence_obj, CategoryTheory.Limits.Fan.mk_pt, HAdd.hAdd, Opposite.op, dite_eq_ite, OfNat.ofNat, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Limits.Fan.mk_π_app
-- 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 : s.pt ⟶ Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f)
h : ∀ (j : ℕᵒᵖ), m ≫ NatTrans.app (Cone.π (cone f)) j = s.π.app j
n : ℕ
⊢ n < 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
s : Cone (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f))
m : s.pt ⟶ Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f)
h : ∀ (j : ℕᵒᵖ), m ≫ NatTrans.app (Cone.π (cone f)) j = s.π.app j
n : ℕ
a : Pi.π M n ≫ eqToHom ⋯
| (CategoryStruct.comp (Y := functorObj.{v_1, u_1} M N (n + 1)) (NatTrans.app (Cone.π (cone f)) (Opposite.op (n + 1)))
      (Pi.π (fun (i : ℕ) ↦ if i < n + 1 then M i else N i) n) :
    Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f) ⟶
      if n < n + 1 then M n else N n)

Tactic:
simp only [← dite_eq_ite, cone_π_app_comp_Pi_π_pos f (n + 1) n (by lia)]

Premises used: CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_pos, HAdd.hAdd, dite_eq_ite, 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
s : Cone (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f))
m : s.pt ⟶ Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f)
h : ∀ (j : ℕᵒᵖ), m ≫ NatTrans.app (Cone.π (cone f)) j = s.π.app j
n : ℕ
h₁ : m ≫ Pi.π M n = m ≫ CategoryStruct.comp (Y := if n < n + 1 then M n else N n) (Pi.π M n ≫ eqToHom ⋯) (eqToHom ⋯)
⊢ m ≫ Pi.π M n =
    m ≫
      CategoryStruct.comp (Y := functorObj.{v_1, u_1} M N (n + 1))
        (NatTrans.app (Cone.π (cone f)) (Opposite.op (n + 1)))
        (Pi.π (fun (i : ℕ) ↦ if i < n + 1 then M i else N i) n ≫ eqToHom ⋯)

Tactic:
slice_rhs 2 3 => simp only [← dite_eq_ite, cone_π_app_comp_Pi_π_pos f (n + 1) n (by lia)]

Premises used: CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_pos, HAdd.hAdd, dite_eq_ite, 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
s : Cone (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f))
m : s.pt ⟶ Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f)
h : ∀ (j : ℕᵒᵖ), m ≫ NatTrans.app (Cone.π (cone f)) j = s.π.app j
n : ℕ
⊢ m ≫ Pi.π M n = m ≫ CategoryStruct.comp (Y := if n < n + 1 then M n else N n) (Pi.π M n ≫ eqToHom ⋯) (eqToHom ⋯)

Tactic:
simp