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 < n
h' : ¬m < n + 1
refine_4 : N m = N m
⊢ Eq.{u_1 + 1} (α := C) (if x : m < n + 1 then M m else N m) (if x : m < n then M m else N 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
n m : ℕ
h : ¬m < n
h' : ¬m < n + 1
⊢ N m = N m

Tactic:
rfl
-- 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' : ¬m < n + 1
⊢ N m = N m

Tactic:
try rfl; try 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 : ℕ
⊢ 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
n : ℕ
⊢ ¬n < n

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 : ℕ
⊢ 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
n : ℕ
⊢ Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (n + 1)) ⟶ N n)
    ((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) n ≫ eqToHom ⋯)
    (Pi.π (fun (i : ℕ) ↦ if x : i < n + 1 then M i else N i) n ≫ eqToHom ⋯ ≫ f n)

Tactic:
simp [functorMap]

Premises used: CategoryTheory.Limits.SequentialProduct.functorMap
-- 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 k : ℕ
h : n ≤ m
hh : ¬k < m
⊢ ¬k < n

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 k : ℕ
hh : ¬k < n
⊢ Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op n) ⟶ N k)
    ((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) k ≫ eqToHom ⋯)
    (Pi.π (fun (i : ℕ) ↦ if x : i < n then M i else N i) k ≫ 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_1 k m : ℕ
h : n ≤ m
ih :
  ∀ (hh : ¬k < m),
    Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op m) ⟶ N k)
      ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE h).op ≫
        Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯)
      (Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯)
hh : ¬k < m + 1
⊢ ¬k < m

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_1 k m : ℕ
h : n ≤ m
ih :
  ∀ (hh : ¬k < m),
    Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op m) ⟶ N k)
      ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE h).op ≫
        Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯)
      (Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯)
hh : ¬k < m + 1
⊢ Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op m) ⟶ N k)
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯)
    (Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯)

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

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_1 k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op m) ⟶ N k)
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯)
    (Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯)
⊢ m ≤ 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_1 k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op m) ⟶ N k)
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯)
    (Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯)
⊢ 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_1 k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op m) ⟶ N k)
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯)
    (Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯)
⊢ homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯

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

Tactic:
rw [ih]
-- 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_1 k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op m) ⟶ N k)
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯)
    (Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯)
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
le_succ_of_le :
  Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (m + 1)) ⟶ N k)
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯)
    (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) k ≫ eqToHom ⋯)
⊢ Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (m + 1)) ⟶ N k)
    (((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 x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯)
    (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) k ≫ eqToHom ⋯)

Tactic:
slice_lhs 2 4 => rw [ih]
-- 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_1 k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op m) ⟶ N k)
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯)
    (Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯)
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
le_succ_of_le :
  Eq.{v_1 + 1} (α := functorObj.{v_1, u_1} M N (m + 1) ⟶ N k)
    (Pi.π (fun (m_2 : ℕ) ↦ if m_2 < m + 1 then M m_2 else N m_2) k ≫
      CategoryStruct.comp (Y := if k < m then M k else N k)
        (if h : k < m then eqToHom ⋯ else if h_1 : k < m + 1 then eqToHom ⋯ ≫ f k ≫ eqToHom ⋯ else eqToHom ⋯)
        (eqToHom ⋯))
    (Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) k ≫ eqToHom ⋯)
⊢ Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (m + 1)) ⟶ N k)
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯)
    (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) k ≫ eqToHom ⋯)

Tactic:
simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, Functor.ofOpSequence_map_homOfLE_succ,
      functorMap, dite_eq_ite, Pi.map_π_assoc]

Premises used: CategoryTheory.Functor.ofOpSequence_obj, CategoryTheory.homOfLE_leOfHom, CategoryTheory.Functor.ofOpSequence_map_homOfLE_succ, 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
n m_1 k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op m) ⟶ N k)
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯)
    (Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯)
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
le_succ_of_le :
  Eq.{v_1 + 1} (α := functorObj.{v_1, u_1} M N (m + 1) ⟶ N k)
    (Pi.π (fun (m_2 : ℕ) ↦ if m_2 < m + 1 then M m_2 else N m_2) k ≫
      CategoryStruct.comp (Y := if k < m then M k else N k) (if h : k < m then eqToHom ⋯ else eqToHom ⋯) (eqToHom ⋯))
    (Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) k ≫ eqToHom ⋯)
⊢ Eq.{v_1 + 1} (α := functorObj.{v_1, u_1} M N (m + 1) ⟶ N k)
    (Pi.π (fun (m_2 : ℕ) ↦ if m_2 < m + 1 then M m_2 else N m_2) k ≫
      CategoryStruct.comp (Y := if k < m then M k else N k)
        (if h : k < m then eqToHom ⋯ else if h_1 : k < m + 1 then eqToHom ⋯ ≫ f k ≫ eqToHom ⋯ else eqToHom ⋯)
        (eqToHom ⋯))
    (Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) k ≫ eqToHom ⋯)

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

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_1 k m : ℕ
h : n ≤ m
hh : ¬k < m + 1
ih :
  Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op m) ⟶ N k)
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯)
    (Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯)
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ Eq.{v_1 + 1} (α := functorObj.{v_1, u_1} M N (m + 1) ⟶ N k)
    (Pi.π (fun (m_2 : ℕ) ↦ if m_2 < m + 1 then M m_2 else N m_2) k ≫
      CategoryStruct.comp (Y := if k < m then M k else N k) (if h : k < m then eqToHom ⋯ else eqToHom ⋯) (eqToHom ⋯))
    (Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) k ≫ eqToHom ⋯)

Tactic:
simp [dif_neg (by lia : ¬(k < m))]

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
n m k : ℕ
h : n ≤ m
hh : ¬k < m
refl :
  ∀ (hh : ¬k < n),
    Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op n) ⟶ N k)
      ((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) k ≫ eqToHom ⋯)
      (Pi.π (fun (i : ℕ) ↦ if x : i < n then M i else N i) k ≫ eqToHom ⋯)
le_succ_of_le :
  ∀ ⦃m : ℕ⦄ (h : n ≤ m)
    (ih :
      ∀ (hh : ¬k < m),
        Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op m) ⟶ N k)
          ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE h).op ≫
            Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯)
          (Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯))
    (hh : ¬k < m + 1),
    Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (m + 1)) ⟶ N k)
      ((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) k ≫ eqToHom ⋯)
      (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) k ≫ eqToHom ⋯)
⊢ Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op m) ⟶ N k)
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE h).op ≫
      Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom ⋯)
    (Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) k ≫ eqToHom ⋯)

Tactic:
induction h using Nat.leRec with
  | refl => simp
  | @le_succ_of_le m h ih =>
    specialize ih (by lia)
    have : homOfLE (by lia : n ≤ m + 1) =
        homOfLE (by lia : n ≤ m) ≫ homOfLE (by lia : m ≤ m + 1) := by simp
    rw [this, op_comp, Functor.map_comp]
    slice_lhs 2 4 => rw [ih]
    simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, Functor.ofOpSequence_map_homOfLE_succ,
      functorMap, dite_eq_ite, Pi.map_π_assoc]
    split_ifs
    simp [dif_neg (by lia : ¬(k < m))]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.ofOpSequence_obj, CategoryTheory.homOfLE_leOfHom, dif_neg, 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
n m : ℕ
h : ¬m < 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 < n
⊢ m < 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 : ℕ
h : ¬0 < n
⊢ n = 0

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 : ℕ
h : ¬0 < n
⊢ n = 0

Tactic:
have : n = 0 := 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
n : ℕ
h : ¬0 < n
this : n = 0
zero :
  ∀ (h : ¬LT.lt (α := ℕ) 0 0),
    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 0) 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 (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)

Tactic:
subst this
-- 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
h : ¬LT.lt (α := ℕ) 0 0
⊢ 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 0) 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)

Tactic:
simp [functorMap]

Premises used: CategoryTheory.Limits.SequentialProduct.functorMap
-- 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 (α :=
    (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 ⋯)
⊢ 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))

Tactic:
rw [← functorMap_commSq_succ f (m + 1)]

Premises used: HAdd.hAdd, CategoryTheory.Limits.SequentialProduct.functorMap_commSq_succ, OfNat.ofNat