-- 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.456050, max (?u.456050 + 1) u} (res f A) B
n_1 : ℕ
S : Subgroup G
inst_3 : S.Normal
n : ℕ
X Y : Rep k G
φ : X ⟶ Y
simp :
  Eq (α := cocycles (Functor.obj (quotientToInvariantsFunctor k S) X) n ⟶ Functor.obj (functor k G n) Y)
    (HomologicalComplex.cyclesMap
        (cochainsMap (MonoidHom.comp (MonoidHom.id (G ⧸ S)) (QuotientGroup.mk' S))
          (CategoryStruct.comp (Y :=
            of (X := (↑(Functor.obj (quotientToInvariantsFunctor k S) Y) : Type u))
              (MonoidHom.comp (ρ (Functor.obj (quotientToInvariantsFunctor k S) Y)) (QuotientGroup.mk' S)))
            (ofHom
              {
                toLinearMap :=
                  (↑(Hom.hom (CategoryTheory.Functor.map (quotientToInvariantsFunctor k S) φ)) :
                    [inst_4 :
                        FunLike
                          (IntertwiningMap
                            (MonoidHom.comp ((quotientToInvariantsFunctor k S).obj X).ρ (MonoidHom.id (G ⧸ S)))
                            ((quotientToInvariantsFunctor k S).obj Y).ρ)
                          (↑((quotientToInvariantsFunctor k S).obj X) : Type u)
                          (↑((quotientToInvariantsFunctor k S).obj Y) : Type u)] →
                      [SemilinearMapClass
                            (IntertwiningMap
                              (MonoidHom.comp ((quotientToInvariantsFunctor k S).obj X).ρ (MonoidHom.id (G ⧸ S)))
                              ((quotientToInvariantsFunctor k S).obj Y).ρ)
                            (RingHom.id k) (↑((quotientToInvariantsFunctor k S).obj X) : Type u)
                            (↑((quotientToInvariantsFunctor k S).obj Y) : Type u)] →
                        (↑((quotientToInvariantsFunctor k S).obj X) : Type u) →ₗ[k]
                          (↑((quotientToInvariantsFunctor k S).obj Y) : Type u)),
                isIntertwining' := ⋯ })
            (ofHom (Y.ρ.quotientToInvariants_lift S))))
        n ≫
      HomologicalComplex.homologyπ (inhomogeneousCochains (of Y.ρ)) n)
    (HomologicalComplex.cyclesMap
        (cochainsMap (MonoidHom.comp (QuotientGroup.mk' S) (MonoidHom.id G))
          (ofHom
              {
                toLinearMap :=
                  (↑(Hom.hom (ofHom (X.ρ.quotientToInvariants_lift S))) :
                    [inst_4 :
                        FunLike
                          (IntertwiningMap
                            (MonoidHom.comp ((quotientToInvariantsFunctor k S).obj X).ρ (QuotientGroup.mk' S)) X.ρ)
                          (↑((quotientToInvariantsFunctor k S).obj X) : Type u) (↑X : Type u)] →
                      [SemilinearMapClass
                            (IntertwiningMap
                              (MonoidHom.comp ((quotientToInvariantsFunctor k S).obj X).ρ (QuotientGroup.mk' S)) X.ρ)
                            (RingHom.id k) (↑((quotientToInvariantsFunctor k S).obj X) : Type u) (↑X : Type u)] →
                        (↑((quotientToInvariantsFunctor k S).obj X) : Type u) →ₗ[k] (↑X : Type u)),
                isIntertwining' := ⋯ } ≫
            φ))
        n ≫
      HomologicalComplex.homologyπ (inhomogeneousCochains Y) n)
⊢ Eq (α :=
    Functor.obj (Functor.comp (D := Rep k (G ⧸ S)) (quotientToInvariantsFunctor k S) (functor k (G ⧸ S) n)) X ⟶
      Functor.obj (functor k G n) Y)
    (CategoryTheory.Functor.map
        (Functor.comp (D := Rep k (G ⧸ S)) (quotientToInvariantsFunctor k S) (functor k (G ⧸ S) n)) φ ≫
      map (QuotientGroup.mk' S) (ofHom (Y.ρ.quotientToInvariants_lift S)) n)
    (CategoryStruct.comp (Y := Functor.obj (functor k G n) X)
      (map (QuotientGroup.mk' S) (ofHom (X.ρ.quotientToInvariants_lift S)) n)
      (CategoryTheory.Functor.map (functor k G n) φ))

Tactic:
simp only [Functor.comp_map, functor_map, ← cancel_epi (groupCohomology.π _ n),
      HomologicalComplex.homologyπ_naturality_assoc, HomologicalComplex.homologyπ_naturality,
      ← HomologicalComplex.cyclesMap_comp_assoc, ← cochainsMap_comp]

Premises used: HomologicalComplex.cyclesMap_comp_assoc, groupCohomology.cochainsMap_comp, HomologicalComplex.homologyπ_naturality, HomologicalComplex.homologyπ_naturality_assoc, groupCohomology.π, CategoryTheory.cancel_epi, CategoryTheory.Functor.comp_map, groupCohomology.functor_map