-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
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))
have change : 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))
                    sorry)) :
              (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: change mapDomain _ _ _ = Finsupp.linearCombination _ _ _