awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
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 k : ℕ
h : (ComplexShape.down ℕ).Rel i j
h_1 : (ComplexShape.down ℕ).Rel j k
eq :
  Eq (α :=
    HomologicalComplex.X K[X] i ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋k⦌)))).len)
    (HomologicalComplex.d K[X] i j ≫
      CategoryStruct.comp (Y :=
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋j⦌)))).len)
        (s.πSummand (IndexSet.id (op ⦋j⦌)))
        (CategoryStruct.comp (Y := X _⦋j⦌)
          (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌)) :
            summand s.N (op ⦋j⦌) (IndexSet.id (op ⦋j⦌)) ⟶
              Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
          (HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)))))
    0
rw :
  Eq (α := s.N i ⟶ s.N k)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)))
        (Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌))) 0 :
      s.N i ⟶ s.N k)
    (0 : s.N i ⟶ s.N k)
rw₁ rw₂ : Eq.{v_1 + 1} (α := s.N i ⟶ s.N k) 0 0
⊢ Eq (α := s.N i ⟶ s.N k)
    (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 := HomologicalComplex.X K[X] j) (HomologicalComplex.d K[X] i j)
            (CategoryStruct.comp (Y := s.N j)
              (s.πSummand (IndexSet.id (op ⦋j⦌)) :
                X _⦋j⦌ ⟶
                  s.N
                    (unop
                        (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
                          (IndexSet.id (op ⦋j⦌)))).len)
              (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
                (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌)) :
                  summand s.N (op ⦋j⦌) (IndexSet.id (op ⦋j⦌)) ⟶
                    Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
                (CategoryStruct.comp (Y := HomologicalComplex.X K[X] k) (HomologicalComplex.d K[X] j k)
                    (s.πSummand (IndexSet.id (op ⦋k⦌))) :
                  Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)) ⟶ s.N k))) :
          Cocone.pt (J := Discrete (IndexSet (op ⦋i⦌))) (s.cofan (op ⦋i⦌)) ⟶ s.N k) :
      s.N i ⟶ s.N k)
    (0 : s.N i ⟶ s.N k)

Tactic:
rw [eq, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
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
dsimp :
  Eq (α := s.N i ⟶ X _⦋j⦌)
    (CategoryStruct.comp (Y := X _⦋i⦌)
        (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⦌)))
          (HomologicalComplex.Hom.f PInfty i : HomologicalComplex.X K[X] i ⟶ HomologicalComplex.X K[X] i))
        (HomologicalComplex.d K[X] i j) :
      s.N i ⟶ X _⦋j⦌)
    (CategoryStruct.comp (Y := s.N j)
        (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) :
          s.N i ⟶ s.N j)
        (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
            (Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌)) :
              summand s.N (op ⦋j⦌) (IndexSet.id (op ⦋j⦌)) ⟶
                Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
            (HomologicalComplex.Hom.f PInfty j : HomologicalComplex.X K[X] j ⟶ HomologicalComplex.X K[X] j) :
          s.N j ⟶ X _⦋j⦌) :
      s.N i ⟶ X _⦋j⦌)
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) i ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) j)
    ((Cofan.inj (s.cofan (op ⦋i⦌)) (IndexSet.id (op ⦋i⦌)) ≫ HomologicalComplex.Hom.f PInfty i) ≫
        HomologicalComplex.d (Karoubi.X (Functor.obj N₁ X)) i j :
      HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) i ⟶
        HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) j)
    (HomologicalComplex.d (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) i j ≫
        Cofan.inj (s.cofan (op ⦋j⦌)) (IndexSet.id (op ⦋j⦌)) ≫ HomologicalComplex.Hom.f PInfty j :
      HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) i ⟶
        HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) j)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
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
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 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)
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ)
      (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))
      (Karoubi.X (Functor.obj N₁ X)))
    (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))
    { f := fun (n : ℕ) ↦ Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) ≫ HomologicalComplex.Hom.f PInfty n,
      comm' := ⋯ }

Tactic:
ext n
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
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 : ℕ
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))
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
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
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⦌))))
⊢ 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⦌)))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
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
a : 𝟙 (HomologicalComplex.X K[X] i) ≫ HomologicalComplex.d K[X] i j
| HomologicalComplex.d K[X] i j

Tactic:
rw [← id_comp (K[X].d i j)]

Premises used: AlgebraicTopology.AlternatingFaceMapComplex.obj, CategoryTheory.Category.id_comp, HomologicalComplex.d
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
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
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)
⊢ 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:
slice_rhs 1 1 => rw [← id_comp (K[X].d i j)]

Premises used: AlgebraicTopology.AlternatingFaceMapComplex.obj, CategoryTheory.Category.id_comp, HomologicalComplex.d
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
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
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)
⊢ 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:
dsimp only [AlternatingFaceMapComplex.obj_X]

Premises used: AlgebraicTopology.AlternatingFaceMapComplex.obj_X
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
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)
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)
⊢ 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:
rw [s.decomposition_id, sum_comp, sum_comp, Finset.sum_eq_single (IndexSet.id (op ⦋i⦌)),
                assoc, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SimplicialObject.Splitting.IndexSet.id, CategoryTheory.Preadditive.sum_comp, Finset.sum_eq_single, CategoryTheory.SimplicialObject.Splitting.decomposition_id, SimplexCategory.mk, Opposite.op
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
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
A : IndexSet (op ⦋i⦌)
h₀ :
  Membership.mem (γ := Finset (IndexSet (op ⦋i⦌))) Finset.univ A →
    A ≠ IndexSet.id (op ⦋i⦌) →
      Eq (α := X _⦋i⦌ ⟶ s.N j)
        (CategoryStruct.comp (Y := X _⦋j⦌)
            (CategoryStruct.comp (Y := X _⦋i⦌)
              (s.πSummand A ≫ Cofan.inj (s.cofan (op ⦋i⦌)) A :
                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)
⊢ Membership.mem (γ := Finset (IndexSet (op ⦋i⦌))) Finset.univ A →
    A ≠ IndexSet.id (op ⦋i⦌) →
      Eq (α := X _⦋i⦌ ⟶ s.N j)
        (CategoryStruct.comp (Y := X _⦋j⦌)
            (CategoryStruct.comp (Y := X _⦋i⦌)
              (s.πSummand A ≫ Cofan.inj (s.cofan (op ⦋i⦌)) A :
                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:
_
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
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
A : IndexSet (op ⦋i⦌)
h_1 : Membership.mem (γ := Finset (IndexSet (op ⦋i⦌))) Finset.univ A
hA : A ≠ IndexSet.id (op ⦋i⦌)
⊢ Eq (α := X _⦋i⦌ ⟶ s.N j)
    (CategoryStruct.comp (Y := X _⦋j⦌)
        (CategoryStruct.comp (Y := X _⦋i⦌)
          (s.πSummand A ≫ Cofan.inj (s.cofan (op ⦋i⦌)) A :
            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:
simp only [assoc, s.ιSummand_comp_d_comp_πSummand_eq_zero _ _ _ hA, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.SimplicialObject.Splitting.ιSummand_comp_d_comp_πSummand_eq_zero
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
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
⊢ 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:
simp only [Finset.mem_univ, not_true, IsEmpty.forall_iff]

Premises used: Finset.mem_univ, not_true, IsEmpty.forall_iff
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
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
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' := ⋯ } ≫
            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)
⊢ 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' := ⋯ }

Tactic:
ext n