awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
w :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X _⦋n⦌)
    (((kernelSubobject (X.δ i.succ.succ)).factorThru
          (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
        (kernelSubobject (X.δ i.succ.succ)).arrow) ≫
      X.δ i.succ.succ ≫ X.δ 0)
    0
w₁ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X _⦋n⦌)
    ((kernelSubobject (X.δ i.succ.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      (kernelSubobject (X.δ i.succ.succ)).arrow ≫ X.δ i.succ.succ ≫ X.δ 0)
    0
w₂ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X _⦋n⦌)
    ((kernelSubobject (X.δ i.succ.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      0 ≫ X.δ 0)
    0
w₃ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X _⦋n⦌)
    ((kernelSubobject (X.δ i.succ.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      0)
    0
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X _⦋n⦌)
    (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ i.succ.succ ≫ X.δ 0)
    0
have w₄ : Eq.{v_1 + 1} (α :=
  Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
    X _⦋n⦌)
  0 0
Tactic: rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i.succ (by simp)),
      Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying (objX X (n + 1 + 1)) ⟶
      Functor.obj underlying (objX X n))
    (objD X (n + 1) ≫ objD X n) 0
have zero : Eq (α :=
  Functor.obj (C := Subobject.{v_1, u_1} (X _⦋HAdd.hAdd (α := ℕ) 0 1 + 1⦌)) underlying
      (objX X (HAdd.hAdd (α := ℕ) 0 1 + 1)) ⟶
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying (objX X 0))
  (objD X (HAdd.hAdd (α := ℕ) 0 1) ≫ objD X 0) 0
Tactic: rcases n with _ | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
zero :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋HAdd.hAdd (α := ℕ) 0 1 + 1⦌)) underlying
        (objX X (HAdd.hAdd (α := ℕ) 0 1 + 1)) ⟶
      Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying (objX X 0))
    (objD X (HAdd.hAdd (α := ℕ) 0 1) ≫ objD X 0) 0
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1⦌)) underlying (objX X (n + 1 + 1)) ⟶
      Functor.obj underlying (objX X n))
    (objD X (n + 1) ≫ objD X n) 0
have succ : ∀ (n : ℕ),
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying (objX X (n + 1 + 1 + 1)) ⟶
      Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying (objX X (n + 1)))
    (objD X (n + 1 + 1) ≫ objD X (n + 1)) 0
Tactic: rcases n with _ | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋HAdd.hAdd (α := ℕ) 0 1 + 1⦌)) underlying
        (objX X (HAdd.hAdd (α := ℕ) 0 1 + 1)) ⟶
      Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying (objX X 0))
    (objD X (HAdd.hAdd (α := ℕ) 0 1) ≫ objD X 0) 0
have zero : Eq (α :=
  Quiver.Hom.{v_1, u_1} (V := C)
    (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
    (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
  (factorThru (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ))
      (arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) sorry ≫
    arrow (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0 ≫ inv (arrow ⊤))
  0
Tactic: dsimp [objD]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying (objX X (n + 1 + 1 + 1)) ⟶
      Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying (objX X (n + 1)))
    (objD X (n + 1 + 1) ≫ objD X (n + 1)) 0
have succ : Eq (α :=
  Quiver.Hom.{v_1, u_1} (V := C)
    (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)))
    (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))))
  (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))
      (arrow (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) sorry ≫
    factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))
      (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) sorry)
  0
Tactic: dsimp [objD]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
⊢ Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
    (factorThru (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯ ≫
      arrow (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0 ≫ inv (arrow ⊤))
    0
have zero : Eq (α :=
  Quiver.Hom.{v_1, u_1} (V := C)
    (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
    (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
  ((arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ≫ X.δ 0 ≫ inv (arrow ⊤)) 0
Tactic: rw [Subobject.factorThru_arrow_assoc, Category.assoc, ← Fin.castSucc_zero,
      ← X.δ_comp_δ_assoc (Fin.zero_le (0 : Fin 2)),
      ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin 2) (by simp)),
      Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
zero :
  Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
    ((arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ≫ X.δ 0 ≫ inv (arrow ⊤)) 0
⊢ Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
    (factorThru (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯ ≫
      arrow (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0 ≫ inv (arrow ⊤))
    0
have zero₁ : Eq (α :=
  Quiver.Hom.{v_1, u_1} (V := C)
    (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
    (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
  (arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0 ≫ X.δ 0 ≫ inv (arrow ⊤)) 0
Tactic: rw [Subobject.factorThru_arrow_assoc, Category.assoc, ← Fin.castSucc_zero,
      ← X.δ_comp_δ_assoc (Fin.zero_le (0 : Fin 2)),
      ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin 2) (by simp)),
      Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
zero :
  Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
    ((arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ≫ X.δ 0 ≫ inv (arrow ⊤)) 0
zero₁ :
  Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
    (arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0 ≫ X.δ 0 ≫ inv (arrow ⊤)) 0
⊢ Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
    (factorThru (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯ ≫
      arrow (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0 ≫ inv (arrow ⊤))
    0
have zero₂ : Eq (α :=
  Quiver.Hom.{v_1, u_1} (V := C)
    (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
    (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
  (arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫
    X.δ (Fin.castSucc 0) ≫ X.δ 0 ≫ inv (arrow ⊤))
  0
Tactic: rw [Subobject.factorThru_arrow_assoc, Category.assoc, ← Fin.castSucc_zero,
      ← X.δ_comp_δ_assoc (Fin.zero_le (0 : Fin 2)),
      ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin 2) (by simp)),
      Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
zero :
  Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
    ((arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ≫ X.δ 0 ≫ inv (arrow ⊤)) 0
zero₁ :
  Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
    (arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0 ≫ X.δ 0 ≫ inv (arrow ⊤)) 0
zero₂ :
  Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
    (arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫
      X.δ (Fin.castSucc 0) ≫ X.δ 0 ≫ inv (arrow ⊤))
    0
⊢ Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
    (factorThru (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯ ≫
      arrow (Finset.inf Finset.univ fun (k : Fin 1) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0 ≫ inv (arrow ⊤))
    0
have zero₃ : Eq (α :=
  Quiver.Hom.{v_1, u_1} (V := C)
    (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋2⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)))
    (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤))
  (arrow (Finset.inf Finset.univ fun (k : Fin 2) ↦ kernelSubobject (X.δ k.succ)) ≫
    X.δ (Fin.succ 0) ≫ X.δ 0 ≫ inv (arrow ⊤))
  0
Tactic: rw [Subobject.factorThru_arrow_assoc, Category.assoc, ← Fin.castSucc_zero,
      ← X.δ_comp_δ_assoc (Fin.zero_le (0 : Fin 2)),
      ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin 2) (by simp)),
      Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))))
    (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯ ≫
      factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯)
    0
have succ : Eq (α :=
  Quiver.Hom.{v_1, u_1} (V := C)
    (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)))
    (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))))
  (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))
    (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) sorry ≫
      arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0)
    sorry)
  0
Tactic: rw [factorThru_right, factorThru_eq_zero, factorThru_arrow_assoc, Category.assoc,
      ← Fin.castSucc_zero,
      ← X.δ_comp_δ (Fin.zero_le (0 : Fin (n + 3))),
      ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin (n + 3)) (by simp)),
      Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
succ :
  Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))))
    (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))
      (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))
          (arrow (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯ ≫
        arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0)
      ⋯)
    0
⊢ Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))))
    (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯ ≫
      factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯)
    0
have succ₁ : Eq (α :=
  Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
    X _⦋n + 1⦌)
  (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))
      (arrow (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) sorry ≫
    arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0)
  0
Tactic: rw [factorThru_right, factorThru_eq_zero, factorThru_arrow_assoc, Category.assoc,
      ← Fin.castSucc_zero,
      ← X.δ_comp_δ (Fin.zero_le (0 : Fin (n + 3))),
      ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin (n + 3)) (by simp)),
      Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
succ :
  Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))))
    (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))
      (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))
          (arrow (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯ ≫
        arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0)
      ⋯)
    0
succ₁ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X _⦋n + 1⦌)
    (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯ ≫
      arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0)
    0
⊢ Eq (α :=
    Quiver.Hom.{v_1, u_1} (V := C)
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)))
      (Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1⦌)) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))))
    (factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯ ≫
      factorThru (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ⋯)
    0
have succ₂ : Eq (α :=
  Functor.obj (C := Subobject.{v_1, u_1} (X _⦋n + 1 + 1 + 1⦌)) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
    X _⦋n + 1⦌)
  ((arrow (Finset.inf Finset.univ fun (k : Fin (n + 2 + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ 0) ≫ X.δ 0) 0
Tactic: rw [factorThru_right, factorThru_eq_zero, factorThru_arrow_assoc, Category.assoc,
      ← Fin.castSucc_zero,
      ← X.δ_comp_δ (Fin.zero_le (0 : Fin (n + 3))),
      ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin (n + 3)) (by simp)),
      Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
⊢ (objX Y n).Factors ((objX X n).arrow ≫ f.app (op ⦋n⦌))
have zero : Factors (X := HomologicalComplex.X (obj X) 0) (objX Y 0) (arrow (objX X 0) ≫ f.app (op ⦋0⦌))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
n : ℕ
zero : Factors (X := HomologicalComplex.X (obj X) 0) (objX Y 0) (arrow (objX X 0) ≫ f.app (op ⦋0⦌))
⊢ (objX Y n).Factors ((objX X n).arrow ≫ f.app (op ⦋n⦌))
have succ : ∀ (n : ℕ),
  Factors (X := HomologicalComplex.X (obj X) (n + 1)) (objX Y (n + 1)) (arrow (objX X (n + 1)) ≫ f.app (op ⦋n + 1⦌))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.MooreComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f_1 f : X ⟶ Y
⊢ Factors (X := HomologicalComplex.X (obj X) 0) (objX Y 0) (arrow (objX X 0) ≫ f.app (op ⦋0⦌))
have zero : Factors (X := Functor.obj (C := Subobject.{v_1, u_1} (X _⦋0⦌)) underlying ⊤) ⊤ (arrow ⊤ ≫ f.app (op ⦋0⦌))
Tactic: dsimp