-- 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 (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)
⊢ 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)

Tactic:
simp only [comp_id, PInfty_f_idem_assoc, AlternatingFaceMapComplex.obj_X, Γ₀_obj_obj]

Premises used: CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.Γ₀_obj_obj, AlgebraicTopology.DoldKan.PInfty_f_idem_assoc, AlgebraicTopology.AlternatingFaceMapComplex.obj_X