-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
x : Fin 1 → G
r : k
simp :
  Eq (α :=
    (↑(HomologicalComplex.X
          (Functor.obj (ChainComplex.single₀ (ModuleCat k))
            (Functor.obj
              (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
                fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
              (trivial k G k)))
          0) :
      Type u))
    ((mapDomain (α :=
            (Functor.obj (𝟭 (SimplicialObject (Type u)))
                  (SimplicialObject.augment
                      (classifyingSpaceUniversalCover G ⋙
                        forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
                          fun (X : Action (Type u) G) ↦ X.V))
                      (⊤_ Type u)
                      (terminal.from
                        ((classifyingSpaceUniversalCover G ⋙
                              forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
                                fun (X : Action (Type u) G) ↦ X.V)).obj
                          (Opposite.op { len := 0 : SimplexCategory })))
                      ⋯).left).obj
              (Opposite.op { len := 0 }))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                  ((SimplicialObject.augment
                          (classifyingSpaceUniversalCover G ⋙
                            forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
                              fun (X : Action (Type u) G) ↦ X.V))
                          (⊤_ Type u)
                          (terminal.from
                            ((classifyingSpaceUniversalCover G ⋙
                                  forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun))
                                    (CC := fun (X : Action (Type u) G) ↦ X.V)).obj
                              (Opposite.op { len := 0 : SimplexCategory })))
                          ⋯).hom.app
                    (Opposite.op { len := 0 : SimplexCategory }))) :
              (a :
                  ((𝟭 (SimplicialObject (Type u))).obj
                        (SimplicialObject.augment (classifyingSpaceUniversalCover G ⋙ forget (Action (Type u) G))
                            (⊤_ Type u)
                            (terminal.from
                              ((classifyingSpaceUniversalCover G ⋙ forget (Action (Type u) G)).obj
                                (Opposite.op { len := 0 })))
                            ⋯).left).obj
                    (Opposite.op { len := 0 })) →
                ((SimplicialObject.const (Type u)).obj
                      (SimplicialObject.augment (classifyingSpaceUniversalCover G ⋙ forget (Action (Type u) G))
                          (⊤_ Type u)
                          (terminal.from
                            ((classifyingSpaceUniversalCover G ⋙ forget (Action (Type u) G)).obj
                              (Opposite.op { len := 0 })))
                          ⋯).right).obj
                  (Opposite.op { len := 0 }))
            ((ModuleCat.Hom.hom'
                  (Iso.hom
                    (HomologicalComplex.XIsoOfEq
                      (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex (ModuleCat k))
                        (compForgetAugmented.toModule k G))
                      ⋯)) :
                (a :
                    (↑(((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex (ModuleCat k)).obj
                              (compForgetAugmented.toModule k G)).X
                          0) :
                      Type u)) →
                  (↑(((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex (ModuleCat k)).obj
                            (compForgetAugmented.toModule k G)).X
                        0) :
                    Type u))
              ((ModuleCat.Hom.hom' (eqToHom ⋯) :
                  (a : (↑((forget₂ToModuleCat k G).X 0) : Type u)) →
                    (↑((AlternatingFaceMapComplex.obj
                              (SimplicialObject.Augmented.drop.obj (compForgetAugmented.toModule k G))).X
                          0) :
                      Type u))
                (single x r))) :
          (a :
              ((SimplicialObject.const (Type u)).obj
                    (SimplicialObject.augment (classifyingSpaceUniversalCover G ⋙ forget (Action (Type u) G))
                        (⊤_ Type u)
                        (terminal.from
                          ((classifyingSpaceUniversalCover G ⋙ forget (Action (Type u) G)).obj
                            (Opposite.op { len := 0 })))
                        ⋯).right).obj
                (Opposite.op { len := 0 })) →
            (↑(((ChainComplex.single₀ (ModuleCat k)).obj ((forget₂ (Rep k G) (ModuleCat k)).obj (trivial k G k))).X 0) :
              Type u))
        default :
      (↑(HomologicalComplex.X
            (Functor.obj (ChainComplex.single₀ (ModuleCat k))
              (Functor.obj
                (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
                  fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                (trivial k G k)))
            0) :
        Type u))
    ((linearCombination k fun (x : Fin 1 → G) ↦ 1 :
          (a : (Fin 1 → G) →₀ k) →
            (↑(((ChainComplex.single₀ (ModuleCat k)).obj ((forget₂ (Rep k G) (ModuleCat k)).obj (trivial k G k))).X 0) :
              Type u))
        (single x r) :
      (↑(HomologicalComplex.X
            (Functor.obj (ChainComplex.single₀ (ModuleCat k))
              (Functor.obj
                (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
                  fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                (trivial k G k)))
            0) :
        Type u))
⊢ Eq (α :=
    (↑(HomologicalComplex.X
          (Functor.obj (ChainComplex.single₀ (ModuleCat k))
            (Functor.obj
              (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
                fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
              (trivial k G k)))
          0) :
      Type u))
    ((mapDomain (α :=
            (Functor.obj (𝟭 (SimplicialObject (Type u))) (compForgetAugmented G).left).obj (Opposite.op { len := 0 }))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                  ((compForgetAugmented G).hom.app (Opposite.op { len := 0 : SimplexCategory }))) :
              (a :
                  (fun (X : Type u) ↦ X)
                    (((𝟭 (SimplicialObject (Type u))).obj (compForgetAugmented G).left).obj
                      (Opposite.op { len := 0 }))) →
                (fun (X : Type u) ↦ X)
                  (((SimplicialObject.const (Type u)).obj (compForgetAugmented G).right).obj
                    (Opposite.op { len := 0 })))
            ((ModuleCat.Hom.hom'
                  (Iso.hom
                    (HomologicalComplex.XIsoOfEq
                      (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex (ModuleCat k))
                        (compForgetAugmented.toModule k G))
                      ⋯)) :
                (a :
                    (↑(((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex (ModuleCat k)).obj
                              (compForgetAugmented.toModule k G)).X
                          0) :
                      Type u)) →
                  (↑(((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex (ModuleCat k)).obj
                            (compForgetAugmented.toModule k G)).X
                        0) :
                    Type u))
              ((ModuleCat.Hom.hom'
                    (HomologicalComplex.Hom.f
                      (HomotopyEquiv.hom (HomotopyEquiv.ofIso (Iso.symm (compForgetAugmentedIso k G)))) 0) :
                  (a : (↑((forget₂ToModuleCat k G).X 0) : Type u)) →
                    (↑((AlternatingFaceMapComplex.obj
                              (SimplicialObject.Augmented.drop.obj (compForgetAugmented.toModule k G))).X
                          0) :
                      Type u))
                (single x r))) :
          (a : ((SimplicialObject.const (Type u)).obj (compForgetAugmented G).right).obj (Opposite.op { len := 0 })) →
            (↑(((ChainComplex.single₀ (ModuleCat k)).obj ((forget₂ (Rep k G) (ModuleCat k)).obj (trivial k G k))).X 0) :
              Type u))
        default :
      (↑(HomologicalComplex.X
            (Functor.obj (ChainComplex.single₀ (ModuleCat k))
              (Functor.obj
                (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
                  fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                (trivial k G k)))
            0) :
        Type u))
    ((linearCombination k fun (x : Fin 1 → G) ↦ 1 :
          (a : (Fin 1 → G) →₀ k) →
            (↑(((ChainComplex.single₀ (ModuleCat k)).obj ((forget₂ (Rep k G) (ModuleCat k)).obj (trivial k G k))).X 0) :
              Type u))
        (single x r) :
      (↑(HomologicalComplex.X
            (Functor.obj (ChainComplex.single₀ (ModuleCat k))
              (Functor.obj
                (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
                  fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                (trivial k G k)))
            0) :
        Type u))

Tactic:
simp only [HomotopyEquiv.ofIso, Iso.symm_hom, compForgetAugmented, compForgetAugmentedIso,
    eqToIso.inv, HomologicalComplex.eqToHom_f]

Premises used: HomologicalComplex.eqToHom_f, CategoryTheory.Iso.symm_hom, HomotopyEquiv.ofIso, classifyingSpaceUniversalCover.compForgetAugmented, CategoryTheory.eqToIso.inv, Rep.standardComplex.compForgetAugmentedIso