-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
refine :
  ∀ (x : Fin 1 → G) (r : k),
    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))
      ((ModuleCat.Hom.hom (HomologicalComplex.Hom.f (HomotopyEquiv.hom (forget₂ToModuleCatHomotopyEquiv k G)) 0) :
            (a : ((classifyingSpaceUniversalCover G).obj (Opposite.op { len := 0 })).V →₀ 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))
      (((ModuleCat.Hom.hom
                (CategoryTheory.Functor.map
                  (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))
                  (ε k G)) :
              (↑(HomologicalComplex.X (forget₂ToModuleCat k G) 0) : Type u) →ₗ[k]
                (↑(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)) :
            (a : ((classifyingSpaceUniversalCover G).obj (Opposite.op { len := 0 })).V →₀ 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 (forget₂ToModuleCat k G) 0 ⟶
      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)
    (HomologicalComplex.Hom.f (HomotopyEquiv.hom (forget₂ToModuleCatHomotopyEquiv k G)) 0)
    (CategoryTheory.Functor.map
      (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))
      (ε k G))

Tactic:
refine ModuleCat.hom_ext <| Finsupp.lhom_ext fun (x : Fin 1 → G) r => ?_

Premises used: Finsupp.lhom_ext, ModuleCat.hom_ext