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
n : ℕ
i : Fin (n + 1)
h :
  ∀ (A : IndexSet (op ⦋n⦌)),
    Eq (α :=
      summand s.N (op ⦋n⦌) A ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n + 1⦌)))).len)
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
        (Cofan.inj (s.cofan (op ⦋n⦌)) A) (X.σ i ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌))))
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
        (Cofan.inj (s.cofan (op ⦋n⦌)) A) 0)
⊢ Eq (α :=
    X _⦋n⦌ ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n + 1⦌)))).len)
    (X.σ i ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌))) 0

Tactic:
apply s.hom_ext'

Premises used: CategoryTheory.SimplicialObject.Splitting.hom_ext'
-- 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 : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
h :
  Eq (α :=
    summand s.N (op ⦋n⦌) A ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n + 1⦌ ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n + 1⦌)))).len)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) (X.map (SimplexCategory.σ i).op ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) 0)
⊢ Eq (α :=
    summand s.N (op ⦋n⦌) A ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n + 1⦌)))).len)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) (X.σ i ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) 0)

Tactic:
dsimp only [SimplicialObject.σ]

Premises used: CategoryTheory.SimplicialObject.σ
-- 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 : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
h : IndexSet.id (op ⦋n + 1⦌) ≠ A.epiComp (SimplexCategory.σ i).op
⊢ Eq (α :=
    summand s.N (op ⦋n⦌) A ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n + 1⦌ ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n + 1⦌)))).len)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) (X.map (SimplexCategory.σ i).op ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
      (Cofan.inj (s.cofan (op ⦋n⦌)) A) 0)

Tactic:
rw [comp_zero, s.cofan_inj_epi_naturality_assoc A (SimplexCategory.σ i).op,
    cofan_inj_πSummand_eq_zero]

Premises used: CategoryTheory.SimplicialObject.Splitting.cofan_inj_πSummand_eq_zero, Quiver.Hom.op, CategoryTheory.Limits.comp_zero, SimplexCategory.σ, CategoryTheory.SimplicialObject.Splitting.cofan_inj_epi_naturality_assoc
-- 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 : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
h : A.epiComp (SimplexCategory.σ i).op ≠ IndexSet.id (op ⦋n + 1⦌)
⊢ IndexSet.id (op ⦋n + 1⦌) ≠ A.epiComp (SimplexCategory.σ i).op

Tactic:
rw [ne_comm]

Premises used: ne_comm
-- 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 : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
h :
  ¬(unop
          ((A.epiComp (SimplexCategory.σ i).op).fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦
            { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α }))).len =
      (unop (op ⦋n + 1⦌)).len
⊢ ¬(A.epiComp (SimplexCategory.σ i).op).EqId

Tactic:
rw [IndexSet.eqId_iff_len_eq]

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.eqId_iff_len_eq
-- 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 : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
⊢ (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α }))).len ≤
    (unop (op ⦋n⦌)).len

Tactic:
have h := SimplexCategory.len_le_of_epi A.e
-- 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 : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
h :
  (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α }))).len ≤
    (unop (op ⦋n⦌)).len
h₁ : ¬(unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len = n + 1
⊢ ¬(unop
          ((A.epiComp (SimplexCategory.σ i).op).fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦
            { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α }))).len =
      (unop (op ⦋n + 1⦌)).len

Tactic:
dsimp at h ⊢
-- 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 : ℕ
i : Fin (n + 1)
A : IndexSet (op ⦋n⦌)
h : (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ≤ n
⊢ ¬(unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len = n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬A.EqId
⊢ ¬Mono A.e

Tactic:
rw [SimplicialObject.Splitting.IndexSet.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
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬Mono A.e
rw :
  Eq (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n)
    ((s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α }))).len ≫
        X.map A.e.op) ≫
      HomologicalComplex.Hom.f PInfty n)
    0
rw₁ :
  Eq (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n)
    (s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α }))).len ≫
      X.map A.e.op ≫ HomologicalComplex.Hom.f PInfty n)
    0
rw₂ :
  Eq (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n)
    (s.ι (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n⦌) ⟶ unop Δ' // Epi α }))).len ≫ 0) 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := summand s.N (op ⦋n⦌) A ⟶ HomologicalComplex.X K[X] n) 0 0
⊢ Eq (α := summand s.N (op ⦋n⦌) A ⟶ 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⦌)) A) (HomologicalComplex.Hom.f PInfty n))
    0

Tactic:
rw [SimplicialObject.Splitting.cofan_inj_eq, assoc, degeneracy_comp_PInfty X n A.e hA, comp_zero]

Premises used: CategoryTheory.SimplicialObject.Splitting.cofan_inj_eq, CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.SimplicialObject.Splitting.IndexSet.e, AlgebraicTopology.DoldKan.degeneracy_comp_PInfty
-- 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⦌
mp :
  Eq (α := Z ⟶ HomologicalComplex.X K[X] n) (f ≫ HomologicalComplex.Hom.f PInfty n) 0 →
    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
mpr :
  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 →
    Eq (α := Z ⟶ HomologicalComplex.X K[X] n) (f ≫ HomologicalComplex.Hom.f PInfty n) 0
⊢ Eq (α := Z ⟶ HomologicalComplex.X K[X] n) (f ≫ HomologicalComplex.Hom.f PInfty n) 0 ↔
    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

Tactic:
constructor
-- 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 ⟶ HomologicalComplex.X K[X] n) (f ≫ HomologicalComplex.Hom.f PInfty n) 0
mp :
  ∀ (f : Z ⟶ X _⦋0⦌) (h : Eq (α := Z ⟶ HomologicalComplex.X K[X] 0) (f ≫ HomologicalComplex.Hom.f PInfty 0) 0),
    Eq (α :=
      Z ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋0⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋0⦌)))).len)
      (f ≫ s.πSummand (IndexSet.id (op ⦋0⦌))) 0
mp₁ :
  ∀ (n : ℕ) (f : Z ⟶ X _⦋n + 1⦌)
    (h : Eq (α := Z ⟶ HomologicalComplex.X K[X] (n + 1)) (f ≫ HomologicalComplex.Hom.f PInfty (n + 1)) 0),
    Eq (α :=
      Z ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n + 1⦌)))).len)
      (f ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌))) 0
⊢ 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

Tactic:
rcases n with _ | 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
Z : C
f : Z ⟶ X _⦋0⦌
h : f ≫ 𝟙 (X _⦋0⦌) = 0
⊢ f = 0

Tactic:
rw [comp_id] at h

Premises used: CategoryTheory.Category.comp_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
Z : C
f : Z ⟶ X _⦋0⦌
h : f = 0
mp :
  Eq (α :=
    Z ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋0⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋0⦌)))).len)
    (0 ≫ s.πSummand (IndexSet.id (op ⦋0⦌))) 0
mp₁ mp₂ :
  Eq.{v_1 + 1} (α :=
    Z ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋0⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋0⦌)))).len)
    0 0
⊢ Eq (α :=
    Z ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋0⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋0⦌)))).len)
    (f ≫ s.πSummand (IndexSet.id (op ⦋0⦌))) 0

Tactic:
rw [h, zero_comp]

Premises used: CategoryTheory.Limits.zero_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
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : Eq (α := Z ⟶ HomologicalComplex.X K[X] (n + 1)) (f ≫ HomologicalComplex.Hom.f PInfty (n + 1)) 0
⊢ f ≫
      HAdd.hAdd (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
        (HomologicalComplex.Hom.f PInfty (n + 1)) (HomologicalComplex.Hom.f QInfty (n + 1)) =
    f ≫ 𝟙 (HomologicalComplex.X K[X] (n + 1))

Tactic:
have h' := f ≫= PInfty_f_add_QInfty_f (n + 1)
-- 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 + 1⦌
h : Eq (α := Z ⟶ HomologicalComplex.X K[X] (n + 1)) (f ≫ HomologicalComplex.Hom.f PInfty (n + 1)) 0
h' :
  f ≫
      HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1⦌) (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1⦌) (HomologicalComplex.Hom.f PInfty (n + 1))
        (HomologicalComplex.Hom.f QInfty (n + 1)) =
    f ≫ 𝟙 (X _⦋n + 1⦌)
⊢ f ≫ HomologicalComplex.Hom.f QInfty (n + 1) = f

Tactic:
rw [comp_id, comp_add, h, zero_add] at h'

Premises used: CategoryTheory.Category.comp_id, zero_add, CategoryTheory.Preadditive.comp_add
-- 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 + 1⦌
h : Eq (α := Z ⟶ HomologicalComplex.X K[X] (n + 1)) (f ≫ HomologicalComplex.Hom.f PInfty (n + 1)) 0
h' : f ≫ HomologicalComplex.Hom.f QInfty (n + 1) = f
mp :
  ∀ (x : Fin (n + 1)),
    Membership.mem (γ := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < n + 1} x →
      Eq (α :=
        Z ⟶
          s.N
            (unop
                (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α })
                  (IndexSet.id (op ⦋n + 1⦌)))).len)
        (f ≫
          (HomologicalComplex.Hom.f (P (↑x : ℕ)) (n + 1) ≫ X.δ x.rev.succ ≫ X.σ x.rev) ≫
            s.πSummand (IndexSet.id (op ⦋n + 1⦌)))
        0
⊢ Eq (α :=
    Z ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n + 1⦌)))).len)
    (f ≫ s.πSummand (IndexSet.id (op ⦋n + 1⦌))) 0

Tactic:
rw [← h', assoc, QInfty_f, decomposition_Q, Preadditive.sum_comp, Preadditive.comp_sum,
        Finset.sum_eq_zero]

Premises used: CategoryTheory.Category.assoc, AlgebraicTopology.DoldKan.QInfty_f, Finset.sum_eq_zero, CategoryTheory.Preadditive.sum_comp, CategoryTheory.Preadditive.comp_sum, AlgebraicTopology.DoldKan.decomposition_Q
-- 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 + 1⦌
h : Eq (α := Z ⟶ HomologicalComplex.X K[X] (n + 1)) (f ≫ HomologicalComplex.Hom.f PInfty (n + 1)) 0
h' : f ≫ HomologicalComplex.Hom.f QInfty (n + 1) = f
i : Fin (n + 1)
mp :
  Membership.mem (γ := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < n + 1} i →
    Eq (α :=
      Z ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n + 1⦌)))).len)
      (f ≫
        (HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev) ≫
          s.πSummand (IndexSet.id (op ⦋n + 1⦌)))
      0
⊢ Membership.mem (γ := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < n + 1} i →
    Eq (α :=
      Z ⟶
        s.N
          (unop
              (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α })
                (IndexSet.id (op ⦋n + 1⦌)))).len)
      (f ≫
        (HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev) ≫
          s.πSummand (IndexSet.id (op ⦋n + 1⦌)))
      0

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
Z : C
n : ℕ
f : Z ⟶ X _⦋n + 1⦌
h : Eq (α := Z ⟶ HomologicalComplex.X K[X] (n + 1)) (f ≫ HomologicalComplex.Hom.f PInfty (n + 1)) 0
h' : f ≫ HomologicalComplex.Hom.f QInfty (n + 1) = f
i : Fin (n + 1)
h_1 : Membership.mem (γ := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < n + 1} i
⊢ Eq (α :=
    Z ⟶
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋n + 1⦌) ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n + 1⦌)))).len)
    (f ≫
      (HomologicalComplex.Hom.f (P (↑i : ℕ)) (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev) ≫
        s.πSummand (IndexSet.id (op ⦋n + 1⦌)))
    0

Tactic:
simp only [assoc, σ_comp_πSummand_id_eq_zero, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero, 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
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
mpr :
  ∀ (a : IndexSet (op ⦋n⦌)),
    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
⊢ Eq (α := Z ⟶ HomologicalComplex.X K[X] n) (f ≫ HomologicalComplex.Hom.f PInfty n) 0

Tactic:
rw [← comp_id f, assoc, s.decomposition_id, Preadditive.sum_comp, Preadditive.comp_sum,
      Fintype.sum_eq_zero]

Premises used: CategoryTheory.Category.assoc, Fintype.sum_eq_zero, CategoryTheory.Preadditive.sum_comp, CategoryTheory.Category.comp_id, CategoryTheory.Preadditive.comp_sum, 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
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⦌)
pos :
  ∀ (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
neg :
  ∀ (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
⊢ 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:
by_cases hA : A.EqId

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.EqId
-- 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 = IndexSet.id (op ⦋n⦌)
pos :
  Eq (α := Z ⟶ HomologicalComplex.X K[X] n)
    (f ≫
      CategoryStruct.comp (Y := 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⦌))) (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌))) :
          X _⦋n⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n))
    0
⊢ 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:
subst hA
-- 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
pos :
  Eq (α := Z ⟶ HomologicalComplex.X K[X] n)
    (f ≫
      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 := X _⦋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)))
    0
pos₁ :
  Eq (α := Z ⟶ HomologicalComplex.X K[X] n)
    (CategoryStruct.comp (Y :=
      s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })
              (IndexSet.id (op ⦋n⦌)))).len)
      0
      (CategoryStruct.comp (Y := X _⦋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)))
    0
pos₂ pos₃ : Eq.{v_1 + 1} (α := Z ⟶ HomologicalComplex.X K[X] n) 0 0
⊢ Eq (α := Z ⟶ HomologicalComplex.X K[X] n)
    (f ≫
      CategoryStruct.comp (Y := 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⦌))) (Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌))) :
          X _⦋n⦌ ⟶ Cocone.pt (J := Discrete (IndexSet (op ⦋n⦌))) (s.cofan (op ⦋n⦌)))
        (HomologicalComplex.Hom.f PInfty n))
    0

Tactic:
rw [assoc, reassoc_of% h, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.zero_comp