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

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

Tactic:
simp only [comp_id, PInfty_comp_πSummand_id]

Premises used: CategoryTheory.SimplicialObject.Splitting.PInfty_comp_πSummand_id, 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
h :
  ∀ (n : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) n ⟶
        HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) n)
      (HomologicalComplex.Hom.f
        (Karoubi.Hom.f
          ({
              f :=
                {
                  f := fun (n : ℕ) ↦
                    Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) ≫ HomologicalComplex.Hom.f PInfty n,
                  comm' := ⋯ :
                  HomologicalComplex.Hom
                    (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))
                    (Karoubi.X (Functor.obj N₁ X)) },
              comm := ⋯ :
              Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} C ℕ)
                (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex) (Functor.obj N₁ X) } ≫
            { f := { f := fun (n : ℕ) ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }, comm := ⋯ }))
        n)
      (HomologicalComplex.Hom.f
        (Karoubi.Hom.f (𝟙 (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))) n)
⊢ Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)
      (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))
    ({
        f :=
          { f := fun (n : ℕ) ↦ Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) ≫ HomologicalComplex.Hom.f PInfty n,
            comm' := ⋯ :
            HomologicalComplex.Hom
              (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))
              (Karoubi.X (Functor.obj N₁ X)) },
        comm := ⋯ :
        Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} C ℕ)
          (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex) (Functor.obj N₁ X) } ≫
      { f := { f := fun (n : ℕ) ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }, comm := ⋯ })
    (𝟙 (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))

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} (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) n ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) n)
    (𝟙 (summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌))))
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f (𝟙 (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))) n)
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) n ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        ({
            f :=
              {
                f := fun (n : ℕ) ↦
                  Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) ≫ HomologicalComplex.Hom.f PInfty n,
                comm' := ⋯ :
                HomologicalComplex.Hom
                  (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))
                  (Karoubi.X (Functor.obj N₁ X)) },
            comm := ⋯ :
            Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} C ℕ)
              (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex) (Functor.obj N₁ X) } ≫
          { f := { f := fun (n : ℕ) ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }, comm := ⋯ }))
      n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f (𝟙 (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))) n)

Tactic:
simp only [assoc, PInfty_comp_πSummand_id, Karoubi.comp_f, HomologicalComplex.comp_f,
      cofan_inj_πSummand_eq_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SimplicialObject.Splitting.PInfty_comp_πSummand_id, CategoryTheory.SimplicialObject.Splitting.cofan_inj_πSummand_eq_id, CategoryTheory.Idempotents.Karoubi.comp_f, HomologicalComplex.comp_f
-- 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 : ℕ
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) n ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) n)
    (𝟙 (summand s.N (op ⦋n⦌) (IndexSet.id (op ⦋n⦌))))
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f (𝟙 (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))) n)

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

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

Tactic:
simp only [πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, Karoubi.comp_f,
      HomologicalComplex.comp_f, N₁_obj_p, Karoubi.id_f]

Premises used: CategoryTheory.SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, AlgebraicTopology.DoldKan.N₁_obj_p, CategoryTheory.Idempotents.Karoubi.id_f, CategoryTheory.Idempotents.Karoubi.comp_f, HomologicalComplex.comp_f
-- 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
⊢ Eq (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) s.nondegComplex K[X])
    (Karoubi.Hom.f (Iso.hom s.toKaroubiNondegComplexIsoN₁) ≫ PInfty)
    (Karoubi.Hom.f (Iso.hom s.toKaroubiNondegComplexIsoN₁))

Tactic:
simpa using s.toKaroubiNondegComplexIsoN₁.hom.comm

Premises used: CategoryTheory.Idempotents.Karoubi.Hom.comm, CategoryTheory.Iso.hom, CategoryTheory.SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁
-- 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
rw :
  Eq (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) s.nondegComplex s.nondegComplex)
    (Karoubi.Hom.f (𝟙 (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) :
      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 (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)))
    (𝟙 s.nondegComplex)
⊢ Eq (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) s.nondegComplex s.nondegComplex)
    (Karoubi.Hom.f (Iso.hom s.toKaroubiNondegComplexIsoN₁) ≫ Karoubi.Hom.f (Iso.inv s.toKaroubiNondegComplexIsoN₁))
    (𝟙 s.nondegComplex)

Tactic:
rw [← dsimp% [-Karoubi.comp_f] Karoubi.comp_f s.toKaroubiNondegComplexIsoN₁.hom
    s.toKaroubiNondegComplexIsoN₁.inv, Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁
-- 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
⊢ Eq (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) s.nondegComplex s.nondegComplex)
    (Karoubi.Hom.f (𝟙 (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) :
      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 (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)))
    (𝟙 s.nondegComplex)

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
⊢ Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ)
    (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K[X])) (Karoubi.X (Functor.obj N₁ X))

Tactic:
exact PInfty

Premises used: AlgebraicTopology.DoldKan.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
⊢ Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K[X])
      (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))
    (Functor.map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (PInfty ≫ s.toNondegComplex))
    (Functor.map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.toNondegComplex)

Tactic:
simp [toNondegComplex]

Premises used: CategoryTheory.SimplicialObject.Splitting.toNondegComplex
-- 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
⊢ Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)
      (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))
    (Functor.map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (s.fromNondegComplex ≫ s.toNondegComplex))
    (Functor.map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (𝟙 s.nondegComplex))

Tactic:
simp [toNondegComplex, fromNondegComplex]

Premises used: CategoryTheory.SimplicialObject.Splitting.toNondegComplex, CategoryTheory.SimplicialObject.Splitting.fromNondegComplex
-- 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 : ℕ
⊢ Eq (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X s.nondegComplex n)
    (HomologicalComplex.Hom.f s.toNondegComplex n)
    (HomologicalComplex.Hom.f PInfty n ≫
      HomologicalComplex.Hom.f (Karoubi.Hom.f (Iso.inv s.toKaroubiNondegComplexIsoN₁)) n)

Tactic:
simp [toNondegComplex, fullyFaithfulToKaroubi]

Premises used: CategoryTheory.SimplicialObject.Splitting.toNondegComplex, CategoryTheory.Idempotents.fullyFaithfulToKaroubi
-- 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 : ℕ
⊢ Eq (α := HomologicalComplex.X s.nondegComplex n ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f s.fromNondegComplex n) (s.ι n ≫ HomologicalComplex.Hom.f PInfty n)

Tactic:
simp [fromNondegComplex, fullyFaithfulToKaroubi,
    cofan, IndexSet.id, IndexSet.e]

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.id, CategoryTheory.Idempotents.fullyFaithfulToKaroubi, CategoryTheory.SimplicialObject.Splitting.IndexSet.e, CategoryTheory.SimplicialObject.Splitting.cofan, CategoryTheory.SimplicialObject.Splitting.fromNondegComplex
-- 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
⊢ Eq (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) s.nondegComplex s.nondegComplex)
    (s.fromNondegComplex ≫ s.toNondegComplex) (𝟙 s.nondegComplex)

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
⊢ Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K[X])
      (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K[X]))
    (Functor.map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (s.toNondegComplex ≫ s.fromNondegComplex))
    (Functor.map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) PInfty)

Tactic:
simp [toNondegComplex, fromNondegComplex]

Premises used: CategoryTheory.SimplicialObject.Splitting.toNondegComplex, CategoryTheory.SimplicialObject.Splitting.fromNondegComplex
-- 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
⊢ Eq (α := Quiver.Hom (V := HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.down ℕ)) K[X] K[X])
    (s.toNondegComplex ≫ s.fromNondegComplex) PInfty

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
⊢ Eq (α := Quiver.Hom (V := HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.down ℕ)) s.nondegComplex s.nondegComplex)
    (s.fromNondegComplex ≫ s.toNondegComplex) (𝟙 s.nondegComplex)

Tactic:
simp
-- 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
dsimp :
  Eq (α := S₁.s.N i ⟶ S₂.s.N j)
    (Φ.f i ≫
      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))
    (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)
⊢ Eq (α := HomologicalComplex.X S₁.s.nondegComplex i ⟶ HomologicalComplex.X S₂.s.nondegComplex j)
    (Φ.f i ≫ HomologicalComplex.d S₂.s.nondegComplex i j) (HomologicalComplex.d S₁.s.nondegComplex i 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
erw :
  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)
⊢ Eq (α := S₁.s.N i ⟶ S₂.s.N j)
    (Φ.f i ≫
      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))
    (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:
erw [← cofan_inj_naturality_symm_assoc Φ (Splitting.IndexSet.id (op ⦋i⦌)),
          ((alternatingFaceMapComplex C).map Φ.F).comm_assoc i j]

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.id, CategoryTheory.Functor.map, CategoryTheory.SimplicialObject.Split.Hom.F, SimplexCategory.mk, Opposite.op, HomologicalComplex.Hom.comm_assoc, AlgebraicTopology.alternatingFaceMapComplex, CategoryTheory.SimplicialObject.Split.cofan_inj_naturality_symm_assoc