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
⊢ 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)
have neg : Eq (α := s.pt ⟶ if x : m < n then M m else N m)
  (CategoryStruct.comp (Y :=
    Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f))
    (Pi.lift fun (m : ℕ) ↦
      CategoryStruct.comp (Y :=
        (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (m + 1)))
        (s.π.app (Opposite.op (m + 1))) (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom sorry))
    (CategoryStruct.comp (Y := piObj.{0, v_1, u_1} fun (m : ℕ) ↦ if x : m < n then M m else N m)
      (NatTrans.app (Cone.π (cone f)) (Opposite.op n)) (Pi.π (fun (m : ℕ) ↦ if x : m < n then M m else N m) m)))
  (s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if x : m < n then M m else N m) m)
Tactic: simp only [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
⊢ Eq (α := s.pt ⟶ if x : m < n then M m else N m)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f))
      (Pi.lift fun (m : ℕ) ↦
        CategoryStruct.comp (Y :=
          (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (m + 1)))
          (s.π.app (Opposite.op (m + 1))) (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯))
      (CategoryStruct.comp (Y := piObj.{0, v_1, u_1} fun (m : ℕ) ↦ if x : m < n then M m else N m)
        (NatTrans.app (Cone.π (cone f)) (Opposite.op n)) (Pi.π (fun (m : ℕ) ↦ if x : m < n then M m else N m) m)))
    (s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if x : m < n then M m else N m) m)
have neg : CategoryStruct.comp (Y := Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f))
    (Pi.lift fun (m : ℕ) ↦
      CategoryStruct.comp (Y :=
        (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (m + 1)))
        (s.π.app (Opposite.op (m + 1))) (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom sorry))
    (Pi.π M m ≫ f m ≫ eqToHom sorry) =
  s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if x : m < n then M m else N m) m
Tactic: rw [cone_π_app_comp_Pi_π_neg f _ _ h]
-- 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
⊢ CategoryStruct.comp (Y :=
      Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f))
      (Pi.lift fun (m : ℕ) ↦
        CategoryStruct.comp (Y :=
          (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (m + 1)))
          (s.π.app (Opposite.op (m + 1))) (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯))
      (Pi.π M m ≫ f m ≫ eqToHom ⋯) =
    s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if x : m < n then M m else N m) m
have neg : Eq (α := s.pt ⟶ if m < n then M m else N m)
  (CategoryStruct.comp (Y := functorObj.{v_1, u_1} M N (m + 1)) (s.π.app (Opposite.op (m + 1)))
    (Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) m ≫ eqToHom sorry ≫ f m ≫ eqToHom sorry))
  (s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if 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]
-- 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
| Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ ≫ f m
have a : (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE sorry).op ≫
  Pi.π (fun (m : ℕ) ↦ if x : m < n then M m else N m) m ≫ eqToHom sorry
Tactic: simp only [← dite_eq_ite, ← functorMap_commSq f 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 m : ℕ
h : ¬m < n
⊢ Eq (α := s.pt ⟶ if m < n then M m else N m)
    (CategoryStruct.comp (Y := functorObj.{v_1, u_1} M N (m + 1)) (s.π.app (Opposite.op (m + 1)))
      (Pi.π (fun (i : ℕ) ↦ if i < m + 1 then M i else N i) m ≫ eqToHom ⋯ ≫ f m ≫ eqToHom ⋯))
    (s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m)
have neg : Eq (α := s.pt ⟶ if m < n then M m else N m)
  (s.π.app (Opposite.op (m + 1)) ≫
    ((Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).map (homOfLE sorry).op ≫
        Pi.π (fun (m : ℕ) ↦ if x : m < n then M m else N m) m ≫ eqToHom sorry) ≫
      eqToHom sorry)
  (s.π.app (Opposite.op n) ≫ Pi.π (fun (m : ℕ) ↦ if m < n then M m else N m) m)
Tactic: slice_lhs 2 4 => simp only [← dite_eq_ite, ← functorMap_commSq f h]
-- 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))
m : s.pt ⟶ Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f)
h : ∀ (j : ℕᵒᵖ), m ≫ NatTrans.app (Cone.π (cone f)) j = s.π.app j
⊢ m =
    Pi.lift fun (m : ℕ) ↦
      CategoryStruct.comp (Y :=
        (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (m + 1)))
        (s.π.app (Opposite.op (m + 1))) (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯)
have h₁ : ∀ (b : ℕ),
  m ≫ Pi.π M b =
    CategoryStruct.comp (Y := piObj.{0, v_1, u_1} M)
      (Pi.lift fun (m : ℕ) ↦
        CategoryStruct.comp (Y :=
          (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (m + 1)))
          (s.π.app (Opposite.op (m + 1))) (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom sorry))
      (Pi.π M b)
Tactic: apply Pi.hom_ext
-- 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))
m : s.pt ⟶ Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f)
h : ∀ (j : ℕᵒᵖ), m ≫ NatTrans.app (Cone.π (cone f)) j = s.π.app j
n : ℕ
⊢ m ≫ Pi.π M n =
    CategoryStruct.comp (Y := piObj.{0, v_1, u_1} M)
      (Pi.lift fun (m : ℕ) ↦
        CategoryStruct.comp (Y :=
          (Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)).obj (Opposite.op (m + 1)))
          (s.π.app (Opposite.op (m + 1))) (Pi.π (fun (i : ℕ) ↦ if x : i < m + 1 then M i else N i) m ≫ eqToHom ⋯))
      (Pi.π M n)
have h₁ : m ≫ Pi.π M n =
  m ≫
    CategoryStruct.comp (Y := functorObj.{v_1, u_1} M N (n + 1)) (NatTrans.app (Cone.π (cone f)) (Opposite.op (n + 1)))
      (Pi.π (fun (i : ℕ) ↦ if i < n + 1 then M i else N i) n ≫ eqToHom sorry)
Tactic: simp only [Functor.ofOpSequence_obj, dite_eq_ite, limit.lift_π, Fan.mk_pt,
      Fan.mk_π_app, ← h ⟨n + 1⟩, 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))
m : s.pt ⟶ Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f)
h : ∀ (j : ℕᵒᵖ), m ≫ NatTrans.app (Cone.π (cone f)) j = s.π.app j
n : ℕ
| (CategoryStruct.comp (Y := functorObj.{v_1, u_1} M N (n + 1)) (NatTrans.app (Cone.π (cone f)) (Opposite.op (n + 1)))
      (Pi.π (fun (i : ℕ) ↦ if i < n + 1 then M i else N i) n) :
    Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f) ⟶
      if n < n + 1 then M n else N n)
have a : Pi.π M n ≫ eqToHom sorry
Tactic: simp only [← dite_eq_ite, cone_π_app_comp_Pi_π_pos f (n + 1) n (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))
m : s.pt ⟶ Cone.pt (F := Functor.ofOpSequence (X := functorObj.{v_1, u_1} M N) (functorMap f)) (cone f)
h : ∀ (j : ℕᵒᵖ), m ≫ NatTrans.app (Cone.π (cone f)) j = s.π.app j
n : ℕ
⊢ m ≫ Pi.π M n =
    m ≫
      CategoryStruct.comp (Y := functorObj.{v_1, u_1} M N (n + 1))
        (NatTrans.app (Cone.π (cone f)) (Opposite.op (n + 1)))
        (Pi.π (fun (i : ℕ) ↦ if i < n + 1 then M i else N i) n ≫ eqToHom ⋯)
have h₁ : m ≫ Pi.π M n = m ≫ CategoryStruct.comp (Y := if n < n + 1 then M n else N n) (Pi.π M n ≫ eqToHom sorry) (eqToHom sorry)
Tactic: slice_rhs 2 3 => simp only [← dite_eq_ite, cone_π_app_comp_Pi_π_pos f (n + 1) n (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
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasFiniteBiproducts.{v_1, u_1} C
inst_4 : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi.{v_1, u_1} (C := C) (X :=
    Cone.pt.{0, v_1, 0, u_1} (F :=
      pair
        (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
        (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
          if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ)))
      (BinaryFan.mk (P :=
        prod.{v_1, u_1}
          (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦
            if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
          (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
            if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ)))
        prod.fst prod.snd))
    (Y :=
    prod.{v_1, u_1}
      (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
      (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ)))
    (prod.map
      (Pi.map fun (i : { x : ℕ // x < n + 1 }) ↦
        if h : (↑i : ℕ) < n then eqToHom ⋯
        else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯)
      (Pi.map fun (i : { x : ℕ // ¬x < n + 1 }) ↦
        if h : (↑i : ℕ) < n then eqToHom ⋯
        else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯))
have inst : Epi.{v_1, u_1} (C := C) (X :=
  piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ)) (Y :=
  piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
  (Pi.map fun (i : { x : ℕ // x < n + 1 }) ↦
    if h : (↑i : ℕ) < n then eqToHom sorry
    else if h' : (↑i : ℕ) < n + 1 then eqToHom sorry ≫ f (↑i : ℕ) ≫ eqToHom sorry else eqToHom sorry)
Tactic: apply +allowSynthFailures prod.map_epi
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst_1 : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_2 : HasCountableProducts.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
inst_5 : ∀ (n : ℕ), Epi (f n)
n : ℕ
inst :
  Epi.{v_1, u_1} (C := C) (X :=
    piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
    (Y := piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
    (Pi.map fun (i : { x : ℕ // x < n + 1 }) ↦
      if h : (↑i : ℕ) < n then eqToHom ⋯
      else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯)
⊢ Epi.{v_1, u_1} (C := C) (X :=
    Cone.pt.{0, v_1, 0, u_1} (F :=
      pair
        (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
        (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
          if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ)))
      (BinaryFan.mk (P :=
        prod.{v_1, u_1}
          (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦
            if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
          (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦
            if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ)))
        prod.fst prod.snd))
    (Y :=
    prod.{v_1, u_1}
      (piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
      (piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ)))
    (prod.map
      (Pi.map fun (i : { x : ℕ // x < n + 1 }) ↦
        if h : (↑i : ℕ) < n then eqToHom ⋯
        else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯)
      (Pi.map fun (i : { x : ℕ // ¬x < n + 1 }) ↦
        if h : (↑i : ℕ) < n then eqToHom ⋯
        else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯))
have inst₁ : Epi.{v_1, u_1} (C := C) (X :=
  piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ)) (Y :=
  piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
  (Pi.map fun (i : { x : ℕ // ¬x < n + 1 }) ↦
    if h : (↑i : ℕ) < n then eqToHom sorry
    else if h' : (↑i : ℕ) < n + 1 then eqToHom sorry ≫ f (↑i : ℕ) ≫ eqToHom sorry else eqToHom sorry)
Tactic: apply +allowSynthFailures prod.map_epi
-- 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
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasFiniteBiproducts.{v_1, u_1} C
inst_4 : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi.{v_1, u_1} (C := C) (X :=
    piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
    (Y := piObj.{0, v_1, u_1} fun (i : { x : ℕ // x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
    (Pi.map fun (i : { x : ℕ // x < n + 1 }) ↦
      if h : (↑i : ℕ) < n then eqToHom ⋯
      else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯)
have inst : ∀ (j : { x : ℕ // x < n + 1 }),
  Epi.{v_1, u_1} (C := C) (X := if x : (↑j : ℕ) < n + 1 then M (↑j : ℕ) else N (↑j : ℕ)) (Y :=
    if x : (↑j : ℕ) < n then M (↑j : ℕ) else N (↑j : ℕ))
    (if h : (↑j : ℕ) < n then eqToHom sorry
    else if h' : (↑j : ℕ) < n + 1 then eqToHom sorry ≫ f (↑j : ℕ) ≫ eqToHom sorry else eqToHom sorry)
Tactic: apply +allowSynthFailures Pi.map_epi
-- 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
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasFiniteBiproducts.{v_1, u_1} C
inst_4 : ∀ (n : ℕ), Epi (f n)
n val : ℕ
property : val < n + 1
⊢ Epi.{v_1, u_1} (C := C) (X :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n + 1 then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ))
    (Y :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ))
    (if h : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n then eqToHom ⋯
    else
      if h' : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n + 1 then
        eqToHom ⋯ ≫ f (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) ≫ eqToHom ⋯
      else eqToHom ⋯)
have inst : ∀ (h : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n),
  Epi.{v_1, u_1} (C := C) (X :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n + 1 then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ))
    (eqToHom sorry)
Tactic: split
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst_1 : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_2 : HasCountableProducts.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
inst_5 : ∀ (n : ℕ), Epi (f n)
n val : ℕ
property : val < n + 1
inst :
  ∀ (h : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n),
    Epi.{v_1, u_1} (C := C) (X :=
      if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n + 1 then
        M (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ)
      else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ))
      (eqToHom ⋯)
⊢ Epi.{v_1, u_1} (C := C) (X :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n + 1 then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ))
    (Y :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ))
    (if h : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n then eqToHom ⋯
    else
      if h' : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n + 1 then
        eqToHom ⋯ ≫ f (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) ≫ eqToHom ⋯
      else eqToHom ⋯)
have inst₁ : ∀ (h : ¬(↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n),
  Epi (X :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n + 1 then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ))
    (Y :=
    if x : (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) < n then
      M (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ)
    else N (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ))
    (eqToHom sorry ≫ f (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < n + 1) val property) : ℕ) ≫ eqToHom sorry)
Tactic: split
-- 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
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasFiniteBiproducts.{v_1, u_1} C
inst_4 : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi.{v_1, u_1} (C := C) (X :=
    piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
    (Y := piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
    (Pi.map fun (i : { x : ℕ // ¬x < n + 1 }) ↦
      if h : (↑i : ℕ) < n then eqToHom ⋯
      else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯)
have inst : IsIso.{v_1, u_1} (C := C) (X :=
  piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ)) (Y :=
  piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
  (Pi.map fun (i : { x : ℕ // ¬x < n + 1 }) ↦
    if h : (↑i : ℕ) < n then eqToHom sorry
    else if h' : (↑i : ℕ) < n + 1 then eqToHom sorry ≫ f (↑i : ℕ) ≫ eqToHom sorry else eqToHom sorry)
Tactic: apply +allowSynthFailures IsIso.epi_of_iso
-- 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
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasFiniteBiproducts.{v_1, u_1} C
inst_4 : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ IsIso.{v_1, u_1} (C := C) (X :=
    piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n + 1 then M (↑i : ℕ) else N (↑i : ℕ))
    (Y := piObj.{0, v_1, u_1} fun (i : { x : ℕ // ¬x < n + 1 }) ↦ if x : (↑i : ℕ) < n then M (↑i : ℕ) else N (↑i : ℕ))
    (Pi.map fun (i : { x : ℕ // ¬x < n + 1 }) ↦
      if h : (↑i : ℕ) < n then eqToHom ⋯
      else if h' : (↑i : ℕ) < n + 1 then eqToHom ⋯ ≫ f (↑i : ℕ) ≫ eqToHom ⋯ else eqToHom ⋯)
have inst : ∀ (b : { x : ℕ // ¬x < n + 1 }),
  IsIso.{v_1, u_1} (C := C) (X := if x : (↑b : ℕ) < n + 1 then M (↑b : ℕ) else N (↑b : ℕ)) (Y :=
    if x : (↑b : ℕ) < n then M (↑b : ℕ) else N (↑b : ℕ))
    (if h : (↑b : ℕ) < n then eqToHom sorry
    else if h' : (↑b : ℕ) < n + 1 then eqToHom sorry ≫ f (↑b : ℕ) ≫ eqToHom sorry else eqToHom sorry)
Tactic: apply +allowSynthFailures Pi.map_isIso