awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (hypothesis)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
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 + 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 ⋯)
have 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 sorry)
  (Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) k ≫ eqToHom sorry)
Tactic: specialize ih (by lia)
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (hypothesis)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
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 ⋯)
⊢ 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 ⋯)
have this : homOfLE sorry = homOfLE sorry ≫ homOfLE sorry
Tactic: have : homOfLE (by lia : n ≤ m + 1) =
        homOfLE (by lia : n ≤ m) ≫ homOfLE (by lia : m ≤ m + 1) := by simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m_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 (α := (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 ⋯)
have 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 sorry).op ≫
      (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE sorry).op) ≫
    Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom sorry)
  (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) k ≫ eqToHom sorry)
Tactic: rw [this, op_comp, Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m_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 ⋯
| (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 ⋯
have a : Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) k ≫ eqToHom sorry
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m_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 (α := (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 ⋯)
have 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 sorry).op ≫
    Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) k ≫ eqToHom sorry)
  (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) k ≫ eqToHom sorry)
Tactic: slice_lhs 2 4 => rw [ih]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m_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 (α := (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 ⋯)
have 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 sorry else if h_1 : k < m + 1 then eqToHom sorry ≫ f k ≫ eqToHom sorry else eqToHom sorry) (eqToHom sorry))
  (Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) k ≫ eqToHom sorry)
Tactic: simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, Functor.ofOpSequence_map_homOfLE_succ,
      functorMap, dite_eq_ite, Pi.map_π_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m_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 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 ⋯)
have 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 sorry else eqToHom sorry) (eqToHom sorry))
  (Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) k ≫ eqToHom sorry)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m k : ℕ
h : n ≤ m
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 ⋯)
have 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 sorry).op ≫
      Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom sorry)
    (Pi.π (fun (i : ℕ) ↦ if x : i < n then M i else N i) k ≫ eqToHom sorry)
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))]
Cleared hypotheses: h, hh
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m 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 ⋯)
⊢ 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 ⋯)
have 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 sorry)
        (Pi.π (fun (i : ℕ) ↦ if x : i < m then M i else N i) k ≫ eqToHom sorry))
  (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 sorry).op ≫
      Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) k ≫ eqToHom sorry)
    (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) k ≫ eqToHom sorry)
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))]
Cleared hypotheses: h, hh
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (hypothesis)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n : ℕ
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)
have this : n = 0
Tactic: have : n = 0 := by lia
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n : ℕ
h : ¬0 < n
this : n = 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)
have 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 sorry).op ≫
      Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op 0) then M m else N m) 0 ≫ eqToHom sorry)
    (Pi.π (fun (i : ℕ) ↦ if x : i < HAdd.hAdd (α := ℕ) 0 1 then M i else N i) 0 ≫ eqToHom sorry ≫ f 0)
Tactic: subst this
Cleared hypotheses: n, h, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : ¬m + 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))
have 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 sorry).op ≫
    Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) (m + 1) ≫ eqToHom sorry)
  ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (Quiver.Hom.op (homOfLE sorry)) ≫
    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 sorry)
Tactic: rw [← functorMap_commSq_succ f (m + 1)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : ¬m + 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 ⋯)
    ((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 ⋯)
have 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 sorry).op ≫
    Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom sorry)
  (functorMap f (m + 1) ≫ Pi.π (fun (m_1 : ℕ) ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom sorry)
Tactic: simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, dite_eq_ite,
        Functor.ofOpSequence_map_homOfLE_succ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (hypothesis)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : ¬m + 1 < n
⊢ 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 ⋯)
have this : homOfLE sorry = homOfLE sorry ≫ homOfLE sorry
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
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ 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 ⋯)
have 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 sorry).op ≫
      (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE sorry).op) ≫
    Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom sorry)
  (functorMap f (m + 1) ≫ Pi.π (fun (m_1 : ℕ) ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom sorry)
Tactic: rw [this, op_comp, Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ 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 ⋯)
have 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 sorry).op ≫
      Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom sorry)
  (functorMap f (m + 1) ≫ Pi.π (fun (m_1 : ℕ) ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom sorry)
Tactic: simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, Functor.ofOpSequence_map_homOfLE_succ,
        Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : ¬m + 1 < n
this : homOfLE ⋯ = homOfLE ⋯ ≫ homOfLE ⋯
⊢ 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 ⋯)
have 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 sorry).op ≫
    Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) (m + 1) ≫ eqToHom sorry)
  (Pi.π (fun (m_1 : ℕ) ↦ if m_1 < m + 1 then M m_1 else N m_1) (m + 1) ≫ eqToHom sorry)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : ¬m < n
⊢ Eq (α := (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (m + 1)) ⟶ N m)
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) m ≫ eqToHom ⋯)
    (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯ ≫ f m)
have 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 sorry).op ≫
      Pi.π (fun (m : ℕ) ↦ if x : m < Opposite.unop (Opposite.op n) then M m else N m) 0 ≫ eqToHom sorry)
    (Pi.π (fun (i : ℕ) ↦ if x : i < HAdd.hAdd (α := ℕ) 0 1 then M i else N i) 0 ≫ eqToHom sorry ≫ f 0)
Tactic: cases m with
  | zero =>
      have : n = 0 := by lia
      subst this
      simp [functorMap]
  | succ m =>
      rw [← functorMap_commSq_succ f (m + 1)]
      simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, dite_eq_ite,
        Functor.ofOpSequence_map_homOfLE_succ]
      have : homOfLE (by lia : n ≤ m + 1 + 1) =
          homOfLE (by lia : n ≤ m + 1) ≫ homOfLE (by lia : m + 1 ≤ m + 1 + 1) := by simp
      rw [this, op_comp, Functor.map_comp]
      simp only [Functor.ofOpSequence_obj, homOfLE_leOfHom, Functor.ofOpSequence_map_homOfLE_succ,
        Category.assoc]
      congr 1
      exact functorMap_commSq_aux f (by lia) (by lia)
Cleared hypotheses: m, h