awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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
K : ChainComplex.{v_1, u_1, 0} C ℕ
i : ℕ
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (obj (Γ₀ ⋙ N₁) K)) i ⟶
      (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K)).X i)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (Iso.hom (Iso.app N₁Γ₀ K))) i)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        (Iso.hom
          (Iso.symm (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≪≫
            mapIso (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₀NondegComplexIso K))))
      i)

Tactic:
simp [N₁Γ₀, Γ₀'CompNondegComplexFunctor]

Premises used: AlgebraicTopology.DoldKan.Γ₀'CompNondegComplexFunctor, AlgebraicTopology.DoldKan.N₁Γ₀
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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
K : ChainComplex.{v_1, u_1, 0} C ℕ
simp :
  Eq (α := obj (Γ₀ ⋙ N₁) K ⟶ obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K)
    (Iso.hom
      (Iso.symm (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≪≫
        mapIso (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₀NondegComplexIso K)))
    (Iso.inv (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≫
      map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Iso.hom (Γ₀NondegComplexIso K)))
⊢ Eq (α := obj (Γ₀ ⋙ N₁) K ⟶ obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K) (Iso.hom (Iso.app N₁Γ₀ K))
    (Iso.inv (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≫
      map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Iso.hom (Γ₀NondegComplexIso K)))

Tactic:
simp only [N₁Γ₀_app]

Premises used: AlgebraicTopology.DoldKan.N₁Γ₀_app
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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
K : ChainComplex.{v_1, u_1, 0} C ℕ
⊢ Eq (α := obj (Γ₀ ⋙ N₁) K ⟶ obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K)
    (Iso.hom
      (Iso.symm (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≪≫
        mapIso (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₀NondegComplexIso K)))
    (Iso.inv (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≫
      map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Iso.hom (Γ₀NondegComplexIso K)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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
K : ChainComplex.{v_1, u_1, 0} C ℕ
simp :
  Eq (α := obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K ⟶ obj (Γ₀ ⋙ N₁) K)
    (Iso.inv
      (Iso.symm (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≪≫
        mapIso (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₀NondegComplexIso K)))
    (map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Iso.inv (Γ₀NondegComplexIso K)) ≫
      Iso.hom (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)))
⊢ Eq (α := obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K ⟶ obj (Γ₀ ⋙ N₁) K) (Iso.inv (Iso.app N₁Γ₀ K))
    (map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Iso.inv (Γ₀NondegComplexIso K)) ≫
      Iso.hom (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)))

Tactic:
simp only [N₁Γ₀_app]

Premises used: AlgebraicTopology.DoldKan.N₁Γ₀_app
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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
K : ChainComplex.{v_1, u_1, 0} C ℕ
⊢ Eq (α := obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K ⟶ obj (Γ₀ ⋙ N₁) K)
    (Iso.inv
      (Iso.symm (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≪≫
        mapIso (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₀NondegComplexIso K)))
    (map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Iso.inv (Γ₀NondegComplexIso K)) ≫
      Iso.hom (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
rw :
  Eq (α :=
    HomologicalComplex.X (Karoubi.X (obj (Γ₀ ⋙ N₁) K)) n ⟶
      (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K)).X n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        (Iso.inv (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≫
          map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Iso.hom (Γ₀NondegComplexIso K))))
      n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (Iso.inv (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)))) n)
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (obj (Γ₀ ⋙ N₁) K)) n ⟶
      (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K)).X n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (NatTrans.app (Iso.hom N₁Γ₀) K)) n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (Iso.inv (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)))) n)

Tactic:
rw [N₁Γ₀_hom_app]

Premises used: AlgebraicTopology.DoldKan.N₁Γ₀_hom_app
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (obj (Γ₀ ⋙ N₁) K)) n ⟶
      (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K)).X n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        (Iso.inv (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≫
          map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Iso.hom (Γ₀NondegComplexIso K))))
      n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (Iso.inv (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)))) n)

Tactic:
apply comp_id

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
rw :
  Eq (α :=
    (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K)).X n ⟶
      HomologicalComplex.X (Karoubi.X (obj (Γ₀ ⋙ N₁) K)) n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        (map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Iso.inv (Γ₀NondegComplexIso K)) ≫
          Iso.hom (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K))))
      n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (Iso.hom (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)))) n)
⊢ Eq (α :=
    (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K)).X n ⟶
      HomologicalComplex.X (Karoubi.X (obj (Γ₀ ⋙ N₁) K)) n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (NatTrans.app (Iso.inv N₁Γ₀) K)) n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (Iso.hom (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)))) n)

Tactic:
rw [N₁Γ₀_inv_app]

Premises used: AlgebraicTopology.DoldKan.N₁Γ₀_inv_app
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
⊢ Eq (α :=
    (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K)).X n ⟶
      HomologicalComplex.X (Karoubi.X (obj (Γ₀ ⋙ N₁) K)) n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        (map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Iso.inv (Γ₀NondegComplexIso K)) ≫
          Iso.hom (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K))))
      n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (Iso.hom (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)))) n)

Tactic:
apply id_comp

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : ChainComplex.{v_1, u_1, 0} C ℕ
h :
  ∀ (n : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (obj (Γ₀ ⋙ N₁) X)) n ⟶
        HomologicalComplex.X (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⋙ Γ₂ ⋙ N₂) X)) n)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (NatTrans.app (Iso.inv N₂Γ₂ToKaroubiIso) X)) n)
      (HomologicalComplex.Hom.f PInfty n)
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Karoubi.X (obj (Γ₀ ⋙ N₁) X))
      (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⋙ Γ₂ ⋙ N₂) X)))
    (Karoubi.Hom.f (NatTrans.app (Iso.inv N₂Γ₂ToKaroubiIso) X)) PInfty

Tactic:
ext n
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
h :
  Eq.{v_1 + 1} (α := Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ X (op ⦋n⦌))
        (HomologicalComplex.Hom.f PInfty n :
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (obj Γ₀ X)) n ⟶
            HomologicalComplex.X (Karoubi.X (obj N₂ (obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) (obj Γ₀ X)))) n)
        (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ X (op ⦋n⦌))
          (HomologicalComplex.Hom.f PInfty n ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)) :
            Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
          (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ X (op ⦋n⦌))
              (HomologicalComplex.Hom.f PInfty n ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)) :
                Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
              (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ X (op ⦋n⦌))
                  (HomologicalComplex.Hom.f PInfty n :
                    HomologicalComplex.X
                        (AlternatingFaceMapComplex.obj (obj Γ₂ (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) X)).X)
                        n ⟶
                      HomologicalComplex.X
                        (AlternatingFaceMapComplex.obj (obj Γ₂ (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) X)).X)
                        n)
                  (Splitting.desc (Γ₀.splitting X) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
                      𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
                        Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A :
                    Γ₀.obj X _⦋n⦌ ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌)) :
                Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌)) :
            Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))) :
      Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (HomologicalComplex.Hom.f PInfty n :
      HomologicalComplex.X (AlternatingFaceMapComplex.obj (obj Γ₀ X)) n ⟶
        HomologicalComplex.X (Karoubi.X (obj N₂ (obj Γ₂ (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) X)))) n)
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (obj (Γ₀ ⋙ N₁) X)) n ⟶
      HomologicalComplex.X (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⋙ Γ₂ ⋙ N₂) X)) n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (NatTrans.app (Iso.inv N₂Γ₂ToKaroubiIso) X)) n)
    (HomologicalComplex.Hom.f PInfty n)

Tactic:
dsimp [N₂Γ₂ToKaroubiIso]

Premises used: AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
⊢ Eq.{v_1 + 1} (α := Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (HomologicalComplex.Hom.f PInfty n ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)) : Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (HomologicalComplex.Hom.f PInfty n :
      HomologicalComplex.X (AlternatingFaceMapComplex.obj (obj Γ₀ X)) n ⟶
        HomologicalComplex.X (AlternatingFaceMapComplex.obj (obj Γ₀ X)) n)

Tactic:
comp_id _

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
h :
  Eq (α := Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (Splitting.desc (Γ₀.splitting X) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
        𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
          Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A :
      Γ₀.obj X _⦋n⦌ ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)))
⊢ Eq.{v_1 + 1} (α := Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ X (op ⦋n⦌))
        (HomologicalComplex.Hom.f PInfty n :
          HomologicalComplex.X (AlternatingFaceMapComplex.obj (obj Γ₀ X)) n ⟶
            HomologicalComplex.X (AlternatingFaceMapComplex.obj (obj Γ₀ X)) n)
        (Splitting.desc (Γ₀.splitting X) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
            𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
              Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A :
          Γ₀.obj X _⦋n⦌ ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌)) :
      Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (HomologicalComplex.Hom.f PInfty n :
      HomologicalComplex.X (AlternatingFaceMapComplex.obj (obj Γ₀ X)) n ⟶
        HomologicalComplex.X (Karoubi.X (obj N₂ (obj Γ₂ (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) X)))) n)

Tactic:
convert! comp_id _

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
h :
  ∀ (A : Splitting.IndexSet (op ⦋n⦌)),
    Eq (α := Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌) A ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
      (CategoryStruct.comp (Y :=
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
          Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌)))
          (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)))
        (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A :
          Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌) A ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
              Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌)))
              (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)))
        (Splitting.desc (Γ₀.splitting X) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
            𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
              Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A :
          Γ₀.obj X _⦋n⦌ ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)))
⊢ Eq (α := Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (Splitting.desc (Γ₀.splitting X) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
        𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
          Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A :
      Γ₀.obj X _⦋n⦌ ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)))

Tactic:
apply (Γ₀.splitting X).hom_ext'

Premises used: AlgebraicTopology.DoldKan.Γ₀.splitting, CategoryTheory.SimplicialObject.Splitting.hom_ext'
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
A : Splitting.IndexSet (op ⦋n⦌)
h :
  Eq.{v_1 + 1} (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌) A ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
      Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)))
⊢ Eq (α := Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌) A ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
        Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌)))
        (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A :
        Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌) A ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
            Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌)))
            (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)))
      (Splitting.desc (Γ₀.splitting X) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
          𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
            Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A :
        Γ₀.obj X _⦋n⦌ ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌)))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)))

Tactic:
rw [Splitting.ι_desc]

Premises used: CategoryTheory.SimplicialObject.Splitting.ι_desc
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
A : Splitting.IndexSet (op ⦋n⦌)
h :
  Eq.{v_1 + 1} (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌) A ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
      Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A)
h₁ h₂ :
  Eq (α := Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌) A ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A) (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A)
⊢ Eq.{v_1 + 1} (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj X) (Γ₀.splitting X)) (op ⦋n⦌) A ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
    (𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
      Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)))

Tactic:
erw [comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)
n : ℕ
dsimp :
  Eq (α := X.X.X n ⟶ Γ₀.Obj.obj₂ X.X (op ⦋n⦌))
    (HomologicalComplex.Hom.f
        (Karoubi.Hom.f
          (NatTrans.app
            (preimage
              (obj
                (whiskeringLeft (ChainComplex.{v_1, u_1, 0} C ℕ) (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
                  (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)))
                (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)))
              (Iso.inv N₁Γ₀ ≫ Iso.inv N₂Γ₂ToKaroubiIso))
            X))
        n :
      X.X.X n ⟶ HomologicalComplex.X (Karoubi.X (obj N₂ (obj Γ₂ X))) n)
    (X.p.f n ≫ Cofan.inj (Splitting.cofan (Γ₀.splitting X.X) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
⊢ Eq (α :=
    (obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) X).X.X n ⟶ HomologicalComplex.X (Karoubi.X (obj (Γ₂ ⋙ N₂) X)) n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (NatTrans.app (Iso.inv N₂Γ₂) X)) n)
    (X.p.f n ≫ Cofan.inj (Splitting.cofan (Γ₀.splitting X.X) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))

Tactic:
dsimp [N₂Γ₂]

Premises used: AlgebraicTopology.DoldKan.N₂Γ₂
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)
n : ℕ
simp :
  Eq (α := X.X.X n ⟶ Γ₀.Obj.obj₂ X.X (op ⦋n⦌))
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (map (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) X.decompId_i)) n ≫
        X.p.f n ≫ Cofan.inj (Splitting.cofan (Γ₀.splitting X.X) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
      X.X.X n ⟶ HomologicalComplex.X (Karoubi.X (obj N₂ (obj Γ₂ X))) n)
    (X.p.f n ≫ Cofan.inj (Splitting.cofan (Γ₀.splitting X.X) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
      X.X.X n ⟶
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
          Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj X.X) (Γ₀.splitting X.X)) (op ⦋n⦌)))
          (Splitting.cofan (Γ₀.splitting X.X) (op ⦋n⦌)))
⊢ Eq (α := X.X.X n ⟶ Γ₀.Obj.obj₂ X.X (op ⦋n⦌))
    (HomologicalComplex.Hom.f
        (Karoubi.Hom.f
          (NatTrans.app
            (preimage
              (obj
                (whiskeringLeft (ChainComplex.{v_1, u_1, 0} C ℕ) (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
                  (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)))
                (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)))
              (Iso.inv N₁Γ₀ ≫ Iso.inv N₂Γ₂ToKaroubiIso))
            X))
        n :
      X.X.X n ⟶ HomologicalComplex.X (Karoubi.X (obj N₂ (obj Γ₂ X))) n)
    (X.p.f n ≫ Cofan.inj (Splitting.cofan (Γ₀.splitting X.X) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))

Tactic:
simp only [whiskeringLeft_obj_preimage_app, NatTrans.comp_app, Functor.comp_map,
    Karoubi.comp_f, N₂Γ₂ToKaroubiIso_inv_app, HomologicalComplex.comp_f,
    N₁Γ₀_inv_app_f_f, toKaroubi_obj_X, Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f,
    PInfty_on_Γ₀_splitting_summand_eq_self, N₂_map_f_f, Γ₂_map_f_app, unop_op, Karoubi.decompId_p_f,
    PInfty_on_Γ₀_splitting_summand_eq_self_assoc, Splitting.IndexSet.id_fst, SimplexCategory.len_mk,
    Splitting.ι_desc]

Premises used: SimplexCategory.len_mk, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_inv_app, CategoryTheory.SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, CategoryTheory.SimplicialObject.Splitting.IndexSet.id_fst, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc, CategoryTheory.Idempotents.Karoubi.comp_f, HomologicalComplex.comp_f, CategoryTheory.Idempotents.whiskeringLeft_obj_preimage_app, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self, CategoryTheory.SimplicialObject.Splitting.ι_desc, Opposite.unop_op, CategoryTheory.Idempotents.Karoubi.decompId_p_f, CategoryTheory.NatTrans.comp_app, AlgebraicTopology.DoldKan.Γ₂_map_f_app, CategoryTheory.Idempotents.toKaroubi_obj_X, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f, AlgebraicTopology.DoldKan.N₂_map_f_f, CategoryTheory.Functor.comp_map
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)
n : ℕ
⊢ Eq (α := X.X.X n ⟶ Γ₀.Obj.obj₂ X.X (op ⦋n⦌))
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (map (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) X.decompId_i)) n ≫
        X.p.f n ≫ Cofan.inj (Splitting.cofan (Γ₀.splitting X.X) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
      X.X.X n ⟶ HomologicalComplex.X (Karoubi.X (obj N₂ (obj Γ₂ X))) n)
    (X.p.f n ≫ Cofan.inj (Splitting.cofan (Γ₀.splitting X.X) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)) :
      X.X.X n ⟶
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
          Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj X.X) (Γ₀.splitting X.X)) (op ⦋n⦌)))
          (Splitting.cofan (Γ₀.splitting X.X) (op ⦋n⦌)))

Tactic:
apply Karoubi.HomologicalComplex.p_idem_assoc

Premises used: CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem_assoc