-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
n : ℕ
f : (Fin n → G) → (↑A : Type u)
h :
  Eq (α := (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (d A n) :
          (a : (↑(ModuleCat.of k ((Fin n → G) → (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
        f :
      (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (n + 1) → G) → (↑A : Type u))) : Type u))
⊢ Eq (α :=
    (↑(Functor.obj
          (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          ((inhomogeneousCochains A).X (n + 1))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X :=
            Functor.obj
              (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
                AddCommGrpCat.carrier))
              ((inhomogeneousCochains A).X n))
            (Y :=
            Functor.obj
              (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
                AddCommGrpCat.carrier))
              ((inhomogeneousCochains A).X (n + 1)))
            (CategoryTheory.Functor.map
              (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
                AddCommGrpCat.carrier))
              ((inhomogeneousCochains A).d n (n + 1))) :
          (a : (↑((forget₂ (ModuleCat k) Ab).obj ((inhomogeneousCochains A).X n)) : Type u)) →
            (↑((forget₂ (ModuleCat k) Ab).obj ((inhomogeneousCochains A).X (n + 1))) : Type u))
        f :
      (↑(Functor.obj
            (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommGrpCat.carrier))
            ((inhomogeneousCochains A).X (n + 1))) :
        Type u))
    (0 :
      (↑(Functor.obj
            (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommGrpCat.carrier))
            ((inhomogeneousCochains A).X (n + 1))) :
        Type u))

Tactic:
simp [h]