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 : ℕ
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 ⋯))
            (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)
⊢ 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))

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))
n m : ℕ
h : m < n
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 ⋯))
      (Pi.π M m ≫ eqToHom ⋯) =
    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, cone_π_app_comp_Pi_π_pos f _ _ h]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_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 m : ℕ
h : m < n
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 ⋯))
    (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 ≫ 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, eqToHom_trans]

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

Tactic:
have hh : m + 1 ≤ n := 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 m : ℕ
h : m < n
hh : m + 1 ≤ n
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 ⋯ =
    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 ⋯))
    (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]

Premises used: Quiver.Hom.op, CategoryTheory.Limits.Cone.w, CategoryTheory.homOfLE
-- 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 :
  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 ⋯ =
    s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m
⊢ (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 ⋯ =
    s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.ofOpSequence_obj, CategoryTheory.homOfLE_leOfHom
-- 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 :
  (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
⊢ 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 ⋯ =
    s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m

Tactic:
congr
-- 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 < 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)

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_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
⊢ homOfLE ⋯ = homOfLE hh ≫ 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
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
⊢ homOfLE ⋯ = homOfLE hh ≫ homOfLE ⋯

Tactic:
have : homOfLE (Nat.le_succ_of_le hh) = homOfLE hh ≫ homOfLE (Nat.le_succ n) := 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
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 ⋯
pos :
  ((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 hh).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 ⋯).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

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
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 ⋯
pos :
  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 ⋯)
    (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 ⋯).op ≫
        (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 + 1 then M m else N m) m

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

Premises used: CategoryTheory.Category.assoc, Nat.succ_eq_add_one, 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
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 ⋯
⊢ 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
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 ⋯
⊢ m < 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
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 ⋯
rw : M m = if x : m < n then M m else N m
rw₁ rw₂ : M m = M m
⊢ 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)

Tactic:
rw [dif_pos (by lia), 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 ⋯
⊢ 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)

Tactic:
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)]
-- 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)
⊢ m < 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
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)
rw : (if x : m < n then M m else N m) = M m
rw₁ rw₂ : M m = M m
⊢ 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)

Tactic:
rw [dif_pos h, 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)
⊢ 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)

Tactic:
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)]
-- 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 ≫
      (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)
⊢ 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 ⋯)
    (Pi.π (fun (m : ℕ) ↦ if m < n + 1 then M m else N m) m)

Tactic:
rw [← eqToHom_trans h₁ h₂]

Premises used: CategoryTheory.eqToHom_trans
-- 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)
⊢ m < 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
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)
a : Pi.π (fun (m : ℕ) ↦ if m < n 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 h₁

Tactic:
rw [ih (by lia)]