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
Z : C
n : ℕ
f : Z ⟶ X _⦋n⦌
h :
  Eq (α :=
    Z ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (f ≫ s.πSummand (IndexSet.id (op ⦋n⦌))) 0
A : IndexSet (op ⦋n⦌)
hA : ¬A.EqId
⊢ Eq (α := Z ⟶ HomologicalComplex.X K[X] n)
    (f ≫
      CategoryStruct.comp (Y := X _⦋n⦌)
        (s.πSummand A ≫ Cofan.inj (s.cofan (op ⦋n⦌)) A :
          X _⦋n⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n))
    0

Tactic:
simp only [assoc, s.cofan_inj_comp_PInfty_eq_zero A hA, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.SimplicialObject.Splitting.cofan_inj_comp_PInfty_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
n : ℕ
rw : 𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌))
| s.πSummand (IndexSet.id (op ⦋n⦌))

Tactic:
rw [← id_comp (s.πSummand _)]

Premises used: CategoryTheory.SimplicialObject.Splitting.πSummand, CategoryTheory.Category.id_comp
-- 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 : ℕ
conv_rhs :
  Eq (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
    (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
⊢ Eq (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌))) (s.πSummand (IndexSet.id (op ⦋n⦌)))

Tactic:
conv_rhs => rw [← id_comp (s.πSummand _)]

Premises used: CategoryTheory.SimplicialObject.Splitting.πSummand, CategoryTheory.Category.id_comp
-- 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 : ℕ
symm :
  Eq (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
    (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
⊢ Eq (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
    (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))

Tactic:
symm
-- 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 : ℕ
rw :
  HSub.hSub (α :=
      HomologicalComplex.X K[X] n ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
      (β :=
      HomologicalComplex.X K[X] n ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
      (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌))) =
    0
rw₁ :
  Eq (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (HSub.hSub (β := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) ≫
      s.πSummand (IndexSet.id (op ⦋n⦌)))
    0
rw₂ :
  Eq (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n)
    (HSub.hSub (β := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌))
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) ≫
      HomologicalComplex.Hom.f PInfty n)
    0
rw₃ :
  HSub.hSub (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n) (𝟙 (X _⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n)
      (HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f PInfty n) =
    0
rw₄ :
  HSub.hSub (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f PInfty n)
      (HomologicalComplex.Hom.f PInfty n ≫ HomologicalComplex.Hom.f PInfty n) =
    0
rw₅ :
  HSub.hSub (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f PInfty n)
      (HomologicalComplex.Hom.f PInfty n) =
    0
rw₆ rw₇ : Eq.{v_1 + 1} (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n) 0 0
⊢ Eq (α :=
    HomologicalComplex.X K[X] n ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
    (𝟙 (X _⦋n⦌) ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))
    (HomologicalComplex.Hom.f PInfty n ≫ s.πSummand (IndexSet.id (op ⦋n⦌)))

Tactic:
rw [← sub_eq_zero, ← sub_comp, ← comp_PInfty_eq_zero_iff, sub_comp, id_comp, PInfty_f_idem,
    sub_self]

Premises used: sub_self, sub_eq_zero, AlgebraicTopology.DoldKan.PInfty_f_idem, CategoryTheory.SimplicialObject.Splitting.comp_PInfty_eq_zero_iff, CategoryTheory.Preadditive.sub_comp, CategoryTheory.Category.id_comp
-- 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 : ℕ
rw : 𝟙 (HomologicalComplex.X K[X] n) ≫ HomologicalComplex.Hom.f PInfty n
| HomologicalComplex.Hom.f PInfty n

Tactic:
rw [← id_comp (PInfty.f n)]

Premises used: HomologicalComplex.Hom.f, AlgebraicTopology.DoldKan.PInfty, CategoryTheory.Category.id_comp
-- 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 : ℕ
conv_rhs :
  CategoryStruct.comp (Y :=
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
      (s.πSummand (IndexSet.id (op ⦋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⦌))) (HomologicalComplex.Hom.f PInfty n)) =
    𝟙 (HomologicalComplex.X K[X] n) ≫ HomologicalComplex.Hom.f PInfty n
⊢ Eq (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[X] n)
    (CategoryStruct.comp (Y :=
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
      (s.πSummand (IndexSet.id (op ⦋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⦌))) (HomologicalComplex.Hom.f PInfty n)))
    (HomologicalComplex.Hom.f PInfty n)

Tactic:
conv_rhs => rw [← id_comp (PInfty.f n)]

Premises used: HomologicalComplex.Hom.f, AlgebraicTopology.DoldKan.PInfty, CategoryTheory.Category.id_comp
-- 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 : ℕ
dsimp :
  Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y :=
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
        (s.πSummand (IndexSet.id (op ⦋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⦌))) (HomologicalComplex.Hom.f PInfty n)) :
      X _⦋n⦌ ⟶ X _⦋n⦌)
    (𝟙 (X _⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n : X _⦋n⦌ ⟶ X _⦋n⦌)
⊢ CategoryStruct.comp (Y :=
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
      (s.πSummand (IndexSet.id (op ⦋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⦌))) (HomologicalComplex.Hom.f PInfty n)) =
    𝟙 (HomologicalComplex.X K[X] n) ≫ HomologicalComplex.Hom.f PInfty n

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
n : ℕ
rw :
  Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y :=
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
      (s.πSummand (IndexSet.id (op ⦋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⦌))) (HomologicalComplex.Hom.f PInfty n)))
    (∑ j : IndexSet (op ⦋n⦌),
      CategoryStruct.comp (Y := X _⦋n⦌)
        (s.πSummand j ≫ Cofan.inj (s.cofan (op ⦋n⦌)) j :
          X _⦋n⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n))
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y :=
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n⦌)))).len)
        (s.πSummand (IndexSet.id (op ⦋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⦌))) (HomologicalComplex.Hom.f PInfty n)) :
      X _⦋n⦌ ⟶ X _⦋n⦌)
    (𝟙 (X _⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n : X _⦋n⦌ ⟶ X _⦋n⦌)

Tactic:
rw [s.decomposition_id, Preadditive.sum_comp]

Premises used: CategoryTheory.Preadditive.sum_comp, CategoryTheory.SimplicialObject.Splitting.decomposition_id
-- 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 : ℕ
rw :
  ∀ (x : IndexSet (op ⦋n⦌)),
    x ≠ IndexSet.id (op ⦋n⦌) →
      Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
        (CategoryStruct.comp (Y := X _⦋n⦌)
          (s.πSummand x ≫ Cofan.inj (s.cofan (op ⦋n⦌)) x :
            X _⦋n⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
          (HomologicalComplex.Hom.f PInfty n))
        0
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y :=
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
      (s.πSummand (IndexSet.id (op ⦋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⦌))) (HomologicalComplex.Hom.f PInfty n)))
    (∑ j : IndexSet (op ⦋n⦌),
      CategoryStruct.comp (Y := X _⦋n⦌)
        (s.πSummand j ≫ Cofan.inj (s.cofan (op ⦋n⦌)) j :
          X _⦋n⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n))

Tactic:
rw [Fintype.sum_eq_single (IndexSet.id (op ⦋n⦌)), assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SimplicialObject.Splitting.IndexSet.id, SimplexCategory.mk, Opposite.op, Fintype.sum_eq_single
-- 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 : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬A.EqId
rw :
  Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
    (s.πSummand A ≫
      CategoryStruct.comp (Y := X _⦋n⦌)
        (Cofan.inj (s.cofan (op ⦋n⦌)) A :
          summand s.N (op ⦋n⦌) A ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n))
    0
rw₁ : Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌) (s.πSummand A ≫ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := X _⦋n⦌ ⟶ X _⦋n⦌) 0 0
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
      (s.πSummand A ≫ Cofan.inj (s.cofan (op ⦋n⦌)) A :
        X _⦋n⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n))
    0

Tactic:
rw [assoc, s.cofan_inj_comp_PInfty_eq_zero A hA, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.SimplicialObject.Splitting.cofan_inj_comp_PInfty_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
j k : ℕ
A : IndexSet (op ⦋j⦌)
hA : ¬A.EqId
⊢ ¬Mono A.e

Tactic:
rw [A.eqId_iff_mono] at hA

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.eqId_iff_mono
-- 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 : ℕ
hij : ¬(ComplexShape.down ℕ).Rel i j
⊢ s.d i j = 0

Tactic:
simp only [d, K[X].shape i j hij, zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.SimplicialObject.Splitting.d, AlgebraicTopology.AlternatingFaceMapComplex.obj, CategoryTheory.Limits.zero_comp, HomologicalComplex.shape
-- 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
simp :
  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)
⊢ s.d i j ≫ s.d j k = 0

Tactic:
simp only [d, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SimplicialObject.Splitting.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 k : ℕ
h : (ComplexShape.down ℕ).Rel i j
h_1 : (ComplexShape.down ℕ).Rel j k
⊢ 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 ≫ 𝟙 (X _⦋j⦌) ≫ HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌))) 0

Tactic:
simp
-- 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 (α :=
    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 ≫ 𝟙 (X _⦋j⦌) ≫ HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌))) 0

Tactic:
have eq : K[X].d i j ≫ 𝟙 (X.obj (op ⦋j⦌)) ≫ K[X].d j k ≫
        s.πSummand (IndexSet.id (op ⦋k⦌)) = 0 := by
      simp
-- 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 ≫ 𝟙 (X _⦋j⦌) ≫ HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌))) 0
⊢ 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 := X _⦋j⦌)
        (∑ A : IndexSet (op ⦋j⦌), s.πSummand A ≫ Cofan.inj (s.cofan (op ⦋j⦌)) A :
          X _⦋j⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋j⦌))) (s.cofan (op ⦋j⦌)))
        (HomologicalComplex.d K[X] j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) :
          X _⦋j⦌ ⟶
            s.N
              (unop
                  (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋k⦌) ⟶ unop Δ' // Epi α })
                    (IndexSet.id (op ⦋k⦌)))).len))
    0

Tactic:
rw [s.decomposition_id] at eq

Premises used: CategoryTheory.SimplicialObject.Splitting.decomposition_id
-- 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 :
  HAdd.hAdd (α :=
      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⦌)))))
      (∑ j_1 ∈ {IndexSet.id (op ⦋j⦌)}ᶜ,
        HomologicalComplex.d K[X] i j ≫
          CategoryStruct.comp (Y := X _⦋j⦌)
            (s.πSummand j_1 ≫ Cofan.inj (s.cofan (op ⦋j⦌)) j_1 :
              X _⦋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
A : IndexSet (op ⦋j⦌)
hA : Membership.mem (γ := Finset (IndexSet (op ⦋j⦌))) {IndexSet.id (op ⦋j⦌)}ᶜ A
⊢ ¬A = IndexSet.id (op ⦋j⦌)

Tactic:
simp only [Finset.mem_compl, Finset.mem_singleton] at hA

Premises used: Finset.mem_singleton, Finset.mem_compl
-- 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 :
  HAdd.hAdd (α :=
      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⦌)))))
      (∑ j_1 ∈ {IndexSet.id (op ⦋j⦌)}ᶜ,
        HomologicalComplex.d K[X] i j ≫
          CategoryStruct.comp (Y := X _⦋j⦌)
            (s.πSummand j_1 ≫ Cofan.inj (s.cofan (op ⦋j⦌)) j_1 :
              X _⦋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
A : IndexSet (op ⦋j⦌)
hA : ¬A = IndexSet.id (op ⦋j⦌)
⊢ 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 := X _⦋j⦌)
        (s.πSummand A ≫ Cofan.inj (s.cofan (op ⦋j⦌)) A :
          X _⦋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

Tactic:
simp only [assoc, ι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