awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
n : ℕ
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) n ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) n)
    (HomologicalComplex.Hom.f
      (Karoubi.p (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex) ≫
        { f := fun (n : ℕ) ↦ Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) ≫ HomologicalComplex.Hom.f PInfty n,
            comm' := ⋯ } ≫
          Karoubi.p (Functor.obj N₁ X))
      n)
    (HomologicalComplex.Hom.f
      { f := fun (n : ℕ) ↦ Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) ≫ HomologicalComplex.Hom.f PInfty n,
        comm' := ⋯ }
      n)
have h : Eq.{v_1 + 1} (α := s.N n ⟶ X _⦋n⦌)
  (𝟙 (s.N n) ≫
    CategoryStruct.comp (Y := X _⦋n⦌)
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
          (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) :
            summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌)) ⟶
              Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
          (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) :
        s.N n ⟶ X _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n))
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
    (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) :
      summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌)) ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
    (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
n : ℕ
⊢ Eq.{v_1 + 1} (α := s.N n ⟶ X _⦋n⦌)
    (𝟙 (s.N n) ≫
      CategoryStruct.comp (Y := X _⦋n⦌)
        (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
            (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) :
              summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌)) ⟶
                Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
            (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) :
          s.N n ⟶ X _⦋n⦌)
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) :
        summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌)) ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n))
have h : Eq (α := s.N n ⟶ X _⦋n⦌)
  (CategoryStruct.comp (Y := X _⦋n⦌)
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
          (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) :
            summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌)) ⟶
              Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
          (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) :
        s.N n ⟶ X _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) :
    s.N n ⟶ X _⦋n⦌)
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) :
        summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌)) ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) :
    s.N n ⟶ X _⦋n⦌)
Tactic: rw [id_comp, assoc, PInfty_f_idem]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) j)
    (CategoryStruct.comp (Y :=
      HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) i)
      (s.πSummand (IndexSet.id (op ⦋i⦌)) :
        X _⦋i⦌ ⟶
          s.N
            (unop
                (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋i⦌) ⟶ unop Δ' // Epi α })
                  (IndexSet.id (op ⦋i⦌)))).len)
      (HomologicalComplex.d (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) i j))
    (HomologicalComplex.d (Karoubi.X (Functor.obj N₁ X)) i j ≫ s.πSummand (IndexSet.id (op ⦋j⦌)))
have dsimp : Eq (α := X _⦋i⦌ ⟶ s.N j)
  (CategoryStruct.comp (Y := s.N i)
    (s.πSummand (IndexSet.id (op ⦋i⦌)) :
      X _⦋i⦌ ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋i⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋i⦌)))).len)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
      (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
        summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
      (CategoryStruct.comp (Y := X _⦋j⦌) (HomologicalComplex.d K[X] i j) (s.πSummand (IndexSet.id (op ⦋j⦌))) :
        Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N j)))
  (CategoryStruct.comp (Y := X _⦋j⦌) (HomologicalComplex.d K[X] i j) (s.πSummand (IndexSet.id (op ⦋j⦌))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
| HomologicalComplex.d K[X] i j
have a : 𝟙 (HomologicalComplex.X K[X] i) ≫ HomologicalComplex.d K[X] i j
Tactic: rw [← id_comp (K[X].d i j)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
⊢ Eq (α := X _⦋i⦌ ⟶ s.N j)
    (CategoryStruct.comp (Y := s.N i)
      (s.πSummand (IndexSet.id (op ⦋i⦌)) :
        X _⦋i⦌ ⟶
          s.N
            (unop
                (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋i⦌) ⟶ unop Δ' // Epi α })
                  (IndexSet.id (op ⦋i⦌)))).len)
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
          summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := X _⦋j⦌) (HomologicalComplex.d K[X] i j) (s.πSummand (IndexSet.id (op ⦋j⦌))) :
          Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N j)))
    (CategoryStruct.comp (Y := X _⦋j⦌) (HomologicalComplex.d K[X] i j) (s.πSummand (IndexSet.id (op ⦋j⦌))))
have slice_rhs : Eq (α := X _⦋i⦌ ⟶ s.N j)
  (CategoryStruct.comp (Y := s.N i)
      (s.πSummand (IndexSet.id (op ⦋i⦌)) :
        X _⦋i⦌ ⟶
          s.N
            (unop
                (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋i⦌) ⟶ unop Δ' // Epi α })
                  (IndexSet.id (op ⦋i⦌)))).len)
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
          summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := X _⦋j⦌) (HomologicalComplex.d K[X] i j) (s.πSummand (IndexSet.id (op ⦋j⦌))) :
          Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N j)) :
    X _⦋i⦌ ⟶ s.N j)
  ((𝟙 (HomologicalComplex.X K[X] i) ≫ HomologicalComplex.d K[X] i j) ≫ s.πSummand (IndexSet.id (op ⦋j⦌)) :
    X _⦋i⦌ ⟶ s.N j)
Tactic: slice_rhs 1 1 => rw [← id_comp (K[X].d i j)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
⊢ Eq (α := X _⦋i⦌ ⟶ s.N j)
    (CategoryStruct.comp (Y := s.N i)
        (s.πSummand (IndexSet.id (op ⦋i⦌)) :
          X _⦋i⦌ ⟶
            s.N
              (unop
                  (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋i⦌) ⟶ unop Δ' // Epi α })
                    (IndexSet.id (op ⦋i⦌)))).len)
        (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
          (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
            summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
              Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
          (CategoryStruct.comp (Y := X _⦋j⦌) (HomologicalComplex.d K[X] i j) (s.πSummand (IndexSet.id (op ⦋j⦌))) :
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N j)) :
      X _⦋i⦌ ⟶ s.N j)
    ((𝟙 (HomologicalComplex.X K[X] i) ≫ HomologicalComplex.d K[X] i j) ≫ s.πSummand (IndexSet.id (op ⦋j⦌)) :
      X _⦋i⦌ ⟶ s.N j)
have dsimp : Eq (α := X _⦋i⦌ ⟶ s.N j)
  (CategoryStruct.comp (Y := s.N i)
      (s.πSummand (IndexSet.id (op ⦋i⦌)) :
        X _⦋i⦌ ⟶
          s.N
            (unop
                (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋i⦌) ⟶ unop Δ' // Epi α })
                  (IndexSet.id (op ⦋i⦌)))).len)
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
          summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := X _⦋j⦌) (HomologicalComplex.d K[X] i j) (s.πSummand (IndexSet.id (op ⦋j⦌))) :
          Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N j)) :
    X _⦋i⦌ ⟶ s.N j)
  (CategoryStruct.comp (Y := X _⦋j⦌) (𝟙 (X _⦋i⦌) ≫ HomologicalComplex.d K[X] i j) (s.πSummand (IndexSet.id (op ⦋j⦌))) :
    X _⦋i⦌ ⟶ s.N j)
Tactic: dsimp only [AlternatingFaceMapComplex.obj_X]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
⊢ Eq (α := X _⦋i⦌ ⟶ s.N j)
    (CategoryStruct.comp (Y := s.N i)
        (s.πSummand (IndexSet.id (op ⦋i⦌)) :
          X _⦋i⦌ ⟶
            s.N
              (unop
                  (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋i⦌) ⟶ unop Δ' // Epi α })
                    (IndexSet.id (op ⦋i⦌)))).len)
        (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
          (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
            summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
              Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
          (CategoryStruct.comp (Y := X _⦋j⦌) (HomologicalComplex.d K[X] i j) (s.πSummand (IndexSet.id (op ⦋j⦌))) :
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N j)) :
      X _⦋i⦌ ⟶ s.N j)
    (CategoryStruct.comp (Y := X _⦋j⦌) (𝟙 (X _⦋i⦌) ≫ HomologicalComplex.d K[X] i j)
        (s.πSummand (IndexSet.id (op ⦋j⦌))) :
      X _⦋i⦌ ⟶ s.N j)
have h₀ : ∀ (b : IndexSet (op ⦋i⦌)),
  Membership.mem (γ := Finset (IndexSet (op ⦋i⦌))) Finset.univ b →
    b ≠ IndexSet.id (op ⦋i⦌) →
      Eq (α := X _⦋i⦌ ⟶ s.N j)
        (CategoryStruct.comp (Y := X _⦋j⦌)
            (CategoryStruct.comp (Y := X _⦋i⦌)
              (s.πSummand b ≫ Cofan.inj (s.cofan (op ⦋i⦌)) b :
                X _⦋i⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
              (HomologicalComplex.d K[X] i j))
            (s.πSummand (IndexSet.id (op ⦋j⦌))) :
          X _⦋i⦌ ⟶ s.N j)
        (0 : X _⦋i⦌ ⟶ s.N j)
Tactic: rw [s.decomposition_id, sum_comp, sum_comp, Finset.sum_eq_single (IndexSet.id (op ⦋i⦌)),
                assoc, assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
h₀ :
  ∀ (b : IndexSet (op ⦋i⦌)),
    Membership.mem (γ := Finset (IndexSet (op ⦋i⦌))) Finset.univ b →
      b ≠ IndexSet.id (op ⦋i⦌) →
        Eq (α := X _⦋i⦌ ⟶ s.N j)
          (CategoryStruct.comp (Y := X _⦋j⦌)
              (CategoryStruct.comp (Y := X _⦋i⦌)
                (s.πSummand b ≫ Cofan.inj (s.cofan (op ⦋i⦌)) b :
                  X _⦋i⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
                (HomologicalComplex.d K[X] i j))
              (s.πSummand (IndexSet.id (op ⦋j⦌))) :
            X _⦋i⦌ ⟶ s.N j)
          (0 : X _⦋i⦌ ⟶ s.N j)
⊢ Eq (α := X _⦋i⦌ ⟶ s.N j)
    (CategoryStruct.comp (Y := s.N i)
        (s.πSummand (IndexSet.id (op ⦋i⦌)) :
          X _⦋i⦌ ⟶
            s.N
              (unop
                  (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋i⦌) ⟶ unop Δ' // Epi α })
                    (IndexSet.id (op ⦋i⦌)))).len)
        (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
          (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) :
            summand s.N (op ⦋i⦌) (IndexSet.id (op ⦋i⦌)) ⟶
              Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
          (CategoryStruct.comp (Y := X _⦋j⦌) (HomologicalComplex.d K[X] i j) (s.πSummand (IndexSet.id (op ⦋j⦌))) :
            Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N j)) :
      X _⦋i⦌ ⟶ s.N j)
    (CategoryStruct.comp (Y := X _⦋j⦌) (𝟙 (X _⦋i⦌) ≫ HomologicalComplex.d K[X] i j)
        (s.πSummand (IndexSet.id (op ⦋j⦌))) :
      X _⦋i⦌ ⟶ s.N j)
have h₁ : IndexSet.id (op ⦋i⦌) ∉ Finset.univ →
  Eq (α := X _⦋i⦌ ⟶ s.N j)
    (CategoryStruct.comp (Y := X _⦋j⦌)
        (CategoryStruct.comp (Y := X _⦋i⦌)
          (CategoryStruct.comp (Y :=
              s.N
                (unop
                    (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋i⦌) ⟶ unop Δ' // Epi α })
                      (IndexSet.id (op ⦋i⦌)))).len)
              (s.πSummand (IndexSet.id (op ⦋i⦌))) (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌))) :
            X _⦋i⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
          (HomologicalComplex.d K[X] i j))
        (s.πSummand (IndexSet.id (op ⦋j⦌))) :
      X _⦋i⦌ ⟶ s.N j)
    (0 : X _⦋i⦌ ⟶ s.N j)
Tactic: rw [s.decomposition_id, sum_comp, sum_comp, Finset.sum_eq_single (IndexSet.id (op ⦋i⦌)),
                assoc, assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Karoubi.X (Functor.obj N₁ X))
      (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)))
    (Karoubi.p (Functor.obj N₁ X) ≫
      { f := fun (n : ℕ) ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ } ≫
        Karoubi.p (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))
    { f := fun (n : ℕ) ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }
have h : ∀ (n : ℕ),
  Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) n ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) n)
    (HomologicalComplex.Hom.f
      (Karoubi.p (Functor.obj N₁ X) ≫
        { f := fun (n : ℕ) ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := sorry } ≫
          Karoubi.p (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))
      n)
    (HomologicalComplex.Hom.f { f := fun (n : ℕ) ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := sorry } n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
n : ℕ
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) n ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) n)
    (HomologicalComplex.Hom.f
      (Karoubi.p (Functor.obj N₁ X) ≫
        { f := fun (n : ℕ) ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ } ≫
          Karoubi.p (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))
      n)
    (HomologicalComplex.Hom.f { f := fun (n : ℕ) ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ } n)
have h : Eq (α := X _⦋n⦌ ⟶ s.N n)
  (CategoryStruct.comp (Y := X _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n)
      (CategoryStruct.comp (Y := s.N n)
        (s.πSummand (IndexSet.id (op ⦋n⦌)) :
          X _⦋n⦌ ⟶
            s.N
              (unop
                  (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                    (IndexSet.id (op ⦋n⦌)))).len)
        (𝟙 (s.N n))) :
    X _⦋n⦌ ⟶ s.N n)
  (s.πSummand (IndexSet.id (op ⦋n⦌)) :
    X _⦋n⦌ ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
⊢ Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)
      (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))
    ({
        f :=
          { f := fun (n : ℕ) ↦ Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) ≫ HomologicalComplex.Hom.f PInfty n,
            comm' := ⋯ :
            HomologicalComplex.Hom
              (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))
              (Karoubi.X (Functor.obj N₁ X)) },
        comm := ⋯ :
        Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} C ℕ)
          (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex) (Functor.obj N₁ X) } ≫
      { f := { f := fun (n : ℕ) ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }, comm := ⋯ })
    (𝟙 (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))
have h : ∀ (n : ℕ),
  Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) n ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        ({
            f :=
              {
                f := fun (n : ℕ) ↦
                  Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) ≫ HomologicalComplex.Hom.f PInfty n,
                comm' := sorry :
                HomologicalComplex.Hom
                  (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))
                  (Karoubi.X (Functor.obj N₁ X)) },
            comm := sorry :
            Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} C ℕ)
              (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex) (Functor.obj N₁ X) } ≫
          { f := { f := fun (n : ℕ) ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := sorry }, comm := sorry }))
      n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f (𝟙 (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))) n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
n : ℕ
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) n ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        ({
            f :=
              {
                f := fun (n : ℕ) ↦
                  Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) ≫ HomologicalComplex.Hom.f PInfty n,
                comm' := ⋯ :
                HomologicalComplex.Hom
                  (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))
                  (Karoubi.X (Functor.obj N₁ X)) },
            comm := ⋯ :
            Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} C ℕ)
              (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex) (Functor.obj N₁ X) } ≫
          { f := { f := fun (n : ℕ) ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }, comm := ⋯ }))
      n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f (𝟙 (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))) n)
have h : Eq.{v_1 + 1} (α :=
  HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) n ⟶
    HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) n)
  (𝟙 (summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌))))
  (HomologicalComplex.Hom.f
    (Karoubi.Hom.f (𝟙 (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))) n)
Tactic: simp only [assoc, PInfty_comp_πSummand_id, Karoubi.comp_f, HomologicalComplex.comp_f,
      cofan_inj_πSummand_eq_id]