awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
s : Cone (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f))
n m : ℕ
h : m < n
hh : m + 1 ≤ n
⊢ (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
have 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 sorry =
  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]
-- 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
s : Cone (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f))
n m : ℕ
h : m < n
hh : m + 1 ≤ n
⊢ 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
have 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 sorry =
  Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m
Tactic: congr
-- 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
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
⊢ (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
have this : homOfLE sorry = homOfLE hh ≫ homOfLE sorry
Tactic: have : homOfLE (Nat.le_succ_of_le hh) = homOfLE hh ≫ homOfLE (Nat.le_succ n) := 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
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 ⋯
⊢ (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
have pos : ((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 hh).op) ≫
    Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) m ≫ eqToHom sorry =
  Pi.π (fun (m : ℕ) ↦ if m < n + 1 then M m else N m) m
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
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 ⋯
⊢ ((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
have 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 sorry)
  (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]
-- 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
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)
have rw : M m = if x : m < n then M m else N m
Tactic: rw [dif_pos (by lia), dif_pos (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
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
⊢ 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)
have rw₁ : M m = M m
Tactic: rw [dif_pos (by lia), dif_pos (by lia)]
-- 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
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 (α := 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)
have 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)
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)]
-- 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
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)
have rw : (if x : m < n then M m else N m) = M m
Tactic: rw [dif_pos h, dif_pos (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
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
⊢ 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)
have rw₁ : M m = M m
Tactic: rw [dif_pos h, dif_pos (by lia)]
-- 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
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 (α := 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)
have 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)
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)]
-- 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
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 (α := 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)
have 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)
Tactic: rw [← eqToHom_trans h₁ h₂]
-- 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
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)
| (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₁
have a : Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m
Tactic: rw [ih (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
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 (α := 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)
have 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)
Tactic: slice_lhs 2 4 => rw [ih (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
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 (α := 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)
have 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 sorry else if h_1 : m < n + 1 then eqToHom sorry ≫ f m ≫ eqToHom sorry else eqToHom sorry) ≫ eqToHom h₂)
  (limit.π (Discrete.functor fun (m : ℕ) ↦ if m < n + 1 then M m else N m) { as := m })
Tactic: simp only [functorMap, dite_eq_ite, Pi.π, 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
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 ℕ } ≫
      (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 })
have 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 sorry else eqToHom sorry ≫ f m ≫ eqToHom sorry) ≫ eqToHom h₂)
  (limit.π (Discrete.functor fun (m : ℕ) ↦ if m < n + 1 then M m else N m) { as := m })
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
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 ℕ } ≫
      (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 })
have 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 sorry ≫ 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)]
-- 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
s : Cone (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f))
n m : ℕ
h : m < n
hh : m + 1 ≤ 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
have 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 sorry)) ≫
      Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) m ≫ eqToHom sorry)
    (Pi.π (fun (m_1 : ℕ) ↦ if m_1 < m + 1 then M m_1 else N m_1) 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
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
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)
⊢ (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
have 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 sorry =
        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 sorry).op ≫
      Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) m ≫ eqToHom sorry =
    Pi.π (fun (m : ℕ) ↦ if m < n + 1 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
Cleared hypotheses: h, hh