awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
simp :
  Eq (α := S₁.s.N i ⟶ S₂.s.N j)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
        (Cofan.inj (S₁.s.cofan (op ⦋i⦌)) (Splitting.IndexSet.id (op ⦋i⦌)))
        (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) S₁.X) i j ≫
          HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) Φ.F) j ≫
            S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) :
      Splitting.summand S₁.s.N (op ⦋i⦌) (Splitting.IndexSet.id (op ⦋i⦌)) ⟶ S₂.s.N j)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋i⦌)) (Splitting.IndexSet.id (op ⦋i⦌)) :
        Splitting.summand S₁.s.N (op ⦋i⦌) (Splitting.IndexSet.id (op ⦋i⦌)) ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
      (CategoryStruct.comp (Y := S₁.X _⦋j⦌) (HomologicalComplex.d K[S₁.X] i j)
          (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j) :
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)) ⟶ S₂.s.N j))
⊢ Eq (α := S₁.s.N i ⟶ S₂.s.N j)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
        (Cofan.inj (S₁.s.cofan (op ⦋i⦌)) (Splitting.IndexSet.id (op ⦋i⦌)))
        (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) S₁.X) i j ≫
          HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) Φ.F) j ≫
            S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) :
      Splitting.summand S₁.s.N (op ⦋i⦌) (Splitting.IndexSet.id (op ⦋i⦌)) ⟶ S₂.s.N j)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
        (Cofan.inj (S₁.s.cofan (op ⦋i⦌)) (Splitting.IndexSet.id (op ⦋i⦌)) :
          Splitting.summand S₁.s.N (op ⦋i⦌) (Splitting.IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := S₁.X _⦋j⦌) (HomologicalComplex.d K[S₁.X] i j)
            (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) :
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)) ⟶ S₁.s.N j) ≫
      Φ.f j)

Tactic:
simp only [assoc]

Premises used: CategoryTheory.Category.assoc
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
e_a :
  Eq (α := HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) S₁.X) j ⟶ S₂.s.N j)
    (HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) Φ.F) j ≫
      S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)))
    (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j)
⊢ Eq (α := S₁.s.N i ⟶ S₂.s.N j)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
        (Cofan.inj (S₁.s.cofan (op ⦋i⦌)) (Splitting.IndexSet.id (op ⦋i⦌)))
        (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) S₁.X) i j ≫
          HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) Φ.F) j ≫
            S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) :
      Splitting.summand S₁.s.N (op ⦋i⦌) (Splitting.IndexSet.id (op ⦋i⦌)) ⟶ S₂.s.N j)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋i⦌)) (Splitting.IndexSet.id (op ⦋i⦌)) :
        Splitting.summand S₁.s.N (op ⦋i⦌) (Splitting.IndexSet.id (op ⦋i⦌)) ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
      (CategoryStruct.comp (Y := S₁.X _⦋j⦌) (HomologicalComplex.d K[S₁.X] i j)
          (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j) :
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)) ⟶ S₂.s.N j))

Tactic:
congr 2
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
e_a :
  ∀ (A : Splitting.IndexSet (op ⦋j⦌)),
    Eq (α := Splitting.summand S₁.s.N (op ⦋j⦌) A ⟶ S₂.s.N j)
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
        (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A)
        (HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) Φ.F) j ≫
          S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
        (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
⊢ Eq (α := HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) S₁.X) j ⟶ S₂.s.N j)
    (HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) Φ.F) j ≫
      S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)))
    (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j)

Tactic:
apply S₁.s.hom_ext'

Premises used: CategoryTheory.SimplicialObject.Split.s, CategoryTheory.SimplicialObject.Splitting.hom_ext'
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
e_a :
  Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (Φ.F.app (op ⦋j⦌) ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
⊢ Eq (α := Splitting.summand S₁.s.N (op ⦋j⦌) A ⟶ S₂.s.N j)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A)
      (HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) Φ.F) j ≫
        S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))

Tactic:
dsimp [alternatingFaceMapComplex]

Premises used: AlgebraicTopology.alternatingFaceMapComplex
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
e_a :
  Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
          Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
⊢ Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (Φ.F.app (op ⦋j⦌) ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))

Tactic:
rw [cofan_inj_naturality_symm_assoc Φ A]

Premises used: CategoryTheory.SimplicialObject.Split.cofan_inj_naturality_symm_assoc
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
pos :
  ∀ (h : A.EqId),
    Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
      (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
        CategoryStruct.comp (Y := S₂.X _⦋j⦌)
          (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
            Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
              Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
          (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
        (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
neg :
  ∀ (h : ¬A.EqId),
    Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
      (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
        CategoryStruct.comp (Y := S₂.X _⦋j⦌)
          (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
            Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
              Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
          (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
        (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
⊢ Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
          Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))

Tactic:
by_cases h : 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
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h_1 : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
h : A = Splitting.IndexSet.id (op ⦋j⦌)
pos :
  Eq (α :=
    S₁.s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α })
              (Splitting.IndexSet.id (op ⦋j⦌)))).len ⟶
      S₂.s.N j)
    (Φ.f
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
              (Splitting.IndexSet.id (op ⦋j⦌)))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)) :
          Splitting.summand S₂.s.N (op ⦋j⦌) (Splitting.IndexSet.id (op ⦋j⦌)) ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)))
      (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
⊢ Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
          Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))

Tactic:
subst h
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
pos :
  Φ.f
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
              (Splitting.IndexSet.id (op ⦋j⦌)))).len ≫
      𝟙 (Splitting.summand S₂.s.N (op ⦋j⦌) (Splitting.IndexSet.id (op ⦋j⦌))) =
    CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)))
      (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j)
⊢ Eq (α :=
    S₁.s.N
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α })
              (Splitting.IndexSet.id (op ⦋j⦌)))).len ⟶
      S₂.s.N j)
    (Φ.f
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
              (Splitting.IndexSet.id (op ⦋j⦌)))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)) :
          Splitting.summand S₂.s.N (op ⦋j⦌) (Splitting.IndexSet.id (op ⦋j⦌)) ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)))
      (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))

Tactic:
rw [Splitting.cofan_inj_πSummand_eq_id]

Premises used: CategoryTheory.SimplicialObject.Splitting.cofan_inj_πSummand_eq_id
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
pos :
  Φ.f j ≫ 𝟙 (S₂.s.N j) =
    CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)))
      (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j)
⊢ Φ.f
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
              (Splitting.IndexSet.id (op ⦋j⦌)))).len ≫
      𝟙 (Splitting.summand S₂.s.N (op ⦋j⦌) (Splitting.IndexSet.id (op ⦋j⦌))) =
    CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)))
      (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j)

Tactic:
dsimp
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
pos :
  Φ.f j =
    CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)))
      (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j)
pos₁ pos₂ : Φ.f j = Φ.f j
⊢ Φ.f j ≫ 𝟙 (S₂.s.N j) =
    CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)))
      (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j)

Tactic:
rw [comp_id, Splitting.cofan_inj_πSummand_eq_id_assoc]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.SimplicialObject.Splitting.cofan_inj_πSummand_eq_id_assoc
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h_1 : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
h : ¬A.EqId
neg :
  Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
          Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) =
    0 ≫ Φ.f j
neg₁ :
  Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫ 0)
    (0 ≫ Φ.f j)
neg₂ :
  Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫ 0) 0
neg₃ neg₄ :
  Eq.{v_1 + 1} (α :=
    S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j) 0 0
⊢ Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
          Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))

Tactic:
rw [S₁.s.cofan_inj_πSummand_eq_zero_assoc _ _ (Ne.symm h),
            S₂.s.cofan_inj_πSummand_eq_zero _ _ (Ne.symm h), zero_comp, comp_zero]

Premises used: CategoryTheory.SimplicialObject.Split.s, CategoryTheory.SimplicialObject.Splitting.cofan_inj_πSummand_eq_zero, CategoryTheory.Limits.comp_zero, Ne.symm, CategoryTheory.Limits.zero_comp, CategoryTheory.SimplicialObject.Splitting.cofan_inj_πSummand_eq_zero_assoc
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y : Split.{v_1, u_1} C
Φ : X ⟶ Y
h :
  ∀ (n : ℕ),
    Eq (α :=
      HomologicalComplex.X
          (Karoubi.X (Functor.obj (nondegComplexFunctor ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) X)) n ⟶
        HomologicalComplex.X (Karoubi.X (Functor.obj (forget C ⋙ N₁) Y)) n)
      (HomologicalComplex.Hom.f
        (Karoubi.Hom.f
          (Functor.map (nondegComplexFunctor ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Φ ≫
            Iso.hom
              ((fun (S : Split.{v_1, u_1} C) ↦
                  (S.s.toKaroubiNondegComplexIsoN₁ :
                    Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
                      (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) S.s.nondegComplex)
                      (Functor.obj N₁ S.X)))
                Y)))
        n)
      (HomologicalComplex.Hom.f
        (Karoubi.Hom.f
          (Iso.hom
              ((fun (S : Split.{v_1, u_1} C) ↦
                  (S.s.toKaroubiNondegComplexIsoN₁ :
                    Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
                      (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) S.s.nondegComplex)
                      (Functor.obj N₁ S.X)))
                X) ≫
            Functor.map (forget C ⋙ N₁) Φ))
        n)
⊢ Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (nondegComplexFunctor ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) X)
      (Functor.obj (forget C ⋙ N₁) Y))
    (Functor.map (nondegComplexFunctor ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Φ ≫
      Iso.hom
        ((fun (S : Split.{v_1, u_1} C) ↦
            (S.s.toKaroubiNondegComplexIsoN₁ :
              Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
                (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) S.s.nondegComplex) (Functor.obj N₁ S.X)))
          Y))
    (Iso.hom
        ((fun (S : Split.{v_1, u_1} C) ↦
            (S.s.toKaroubiNondegComplexIsoN₁ :
              Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
                (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) S.s.nondegComplex) (Functor.obj N₁ S.X)))
          X) ≫
      Functor.map (forget C ⋙ N₁) Φ)

Tactic:
ext n