-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ_1 : Quiver.Hom.{?u.450927, max (?u.450927 + 1) u} (res f A) B
n_1 n : ℕ
X Y : Rep k H
φ : X ⟶ Y
simp :
  Eq (α := cocycles X n ⟶ groupCohomology (of (MonoidHom.comp Y.ρ f)) n)
    (HomologicalComplex.cyclesMap
        (cochainsMap (MonoidHom.comp (MonoidHom.id H) f)
          (ofHom
            {
              toLinearMap :=
                (↑(Hom.hom φ) :
                  [inst_3 :
                      FunLike (IntertwiningMap (MonoidHom.comp X.ρ (MonoidHom.id H)) Y.ρ) (↑X : Type u) (↑Y : Type u)] →
                    [SemilinearMapClass (IntertwiningMap (MonoidHom.comp X.ρ (MonoidHom.id H)) Y.ρ) (RingHom.id k)
                          (↑X : Type u) (↑Y : Type u)] →
                      (↑X : Type u) →ₗ[k] (↑Y : Type u)),
              isIntertwining' := ⋯ }))
        n ≫
      HomologicalComplex.homologyπ (inhomogeneousCochains (res f Y)) n)
    (HomologicalComplex.cyclesMap
        (cochainsMap (f.comp (MonoidHom.id G))
          (CategoryStruct.comp (Y := of ((MonoidHom.comp X.ρ f).comp (MonoidHom.id G)))
            (ofHom
              {
                toLinearMap :=
                  (↑(IntertwiningMap.id (MonoidHom.comp X.ρ f)) :
                    [inst_3 :
                        FunLike (IntertwiningMap (MonoidHom.comp X.ρ f) (MonoidHom.comp X.ρ f)) (↑X : Type u)
                          (↑X : Type u)] →
                      [SemilinearMapClass (IntertwiningMap (MonoidHom.comp X.ρ f) (MonoidHom.comp X.ρ f)) (RingHom.id k)
                            (↑X : Type u) (↑X : Type u)] →
                        (↑X : Type u) →ₗ[k] (↑X : Type u)),
                isIntertwining' := ⋯ })
            (ofHom
              {
                toLinearMap :=
                  (↑(Hom.hom φ) :
                    [inst_3 : FunLike (X.ρ.IntertwiningMap Y.ρ) (↑X : Type u) (↑Y : Type u)] →
                      [SemilinearMapClass (X.ρ.IntertwiningMap Y.ρ) (RingHom.id k) (↑X : Type u) (↑Y : Type u)] →
                        (↑X : Type u) →ₗ[k] (↑Y : Type u)),
                isIntertwining' := ⋯ })))
        n ≫
      HomologicalComplex.homologyπ (inhomogeneousCochains (of (MonoidHom.comp Y.ρ f))) n)
⊢ Eq (α := Functor.obj (functor k H n) X ⟶ Functor.obj (resFunctor f ⋙ functor k G n) Y)
    (CategoryTheory.Functor.map (functor k H n) φ ≫ map f (𝟙 (res f Y)) n)
    (map f (𝟙 (res f X)) n ≫ CategoryTheory.Functor.map (resFunctor f ⋙ functor k G n) φ)

Tactic:
simp only [functor_obj, Functor.comp_obj, functor_map, Functor.comp_map,
      ← cancel_epi (groupCohomology.π _ n), HomologicalComplex.homologyπ_naturality_assoc,
      HomologicalComplex.homologyπ_naturality, ← HomologicalComplex.cyclesMap_comp_assoc,
      ← cochainsMap_comp, res_obj_ρ, Category.comp_id, Rep.hom_id]

Premises used: CategoryTheory.Functor.comp_obj, HomologicalComplex.cyclesMap_comp_assoc, groupCohomology.cochainsMap_comp, Rep.hom_id, HomologicalComplex.homologyπ_naturality, HomologicalComplex.homologyπ_naturality_assoc, groupCohomology.functor_obj, CategoryTheory.Category.comp_id, groupCohomology.π, Rep.res_obj_ρ, CategoryTheory.cancel_epi, CategoryTheory.Functor.comp_map, groupCohomology.functor_map