-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k G H : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ_1 : Quiver.Hom.{?u.1141002, max u (?u.1141002 + 1)} A (res f B)
n_1 : ℕ
S : Subgroup G
inst_3 : S.Normal
n : ℕ
X Y : Rep k G
φ : X ⟶ Y
simp :
  Eq (α :=
    cycles X n ⟶
      Functor.obj (Functor.comp (D := Rep k (G ⧸ S)) (quotientToCoinvariantsFunctor k S) (functor k (G ⧸ S) n)) Y)
    (HomologicalComplex.cyclesMap
        (chainsMap (MonoidHom.comp (QuotientGroup.mk' S) (MonoidHom.id G))
          (φ ≫
            ofHom
              {
                toLinearMap :=
                  (↑(Hom.hom (Y.toCoinvariantsMkQ S) :
                        Y.ρ.IntertwiningMap
                          (res (QuotientGroup.mk' S) (Functor.obj (quotientToCoinvariantsFunctor k S) Y)).ρ) :
                    [inst_4 :
                        FunLike
                          (Y.ρ.IntertwiningMap
                            (MonoidHom.comp ((quotientToCoinvariantsFunctor k S).obj Y).ρ (QuotientGroup.mk' S)))
                          (↑Y : Type u) (↑((quotientToCoinvariantsFunctor k S).obj Y) : Type u)] →
                      [SemilinearMapClass
                            (Y.ρ.IntertwiningMap
                              (MonoidHom.comp ((quotientToCoinvariantsFunctor k S).obj Y).ρ (QuotientGroup.mk' S)))
                            (RingHom.id k) (↑Y : Type u) (↑((quotientToCoinvariantsFunctor k S).obj Y) : Type u)] →
                        (↑Y : Type u) →ₗ[k] (↑((quotientToCoinvariantsFunctor k S).obj Y) : Type u)),
                isIntertwining' := ⋯ }))
        n ≫
      HomologicalComplex.homologyπ (inhomogeneousChains (Functor.obj (quotientToCoinvariantsFunctor k S) Y)) n)
    (HomologicalComplex.cyclesMap
        (chainsMap (MonoidHom.comp (MonoidHom.id (G ⧸ S)) (QuotientGroup.mk' S))
          (CategoryStruct.comp (Y := res (QuotientGroup.mk' S) (Functor.obj (quotientToCoinvariantsFunctor k S) X))
            (X.toCoinvariantsMkQ S : X ⟶ X.toCoinvariants S)
            (ofHom
              {
                toLinearMap :=
                  (↑(Hom.hom (CategoryTheory.Functor.map (quotientToCoinvariantsFunctor k S) φ)) :
                    [inst_4 :
                        FunLike
                          (((quotientToCoinvariantsFunctor k S).obj X).ρ.IntertwiningMap
                            (MonoidHom.comp ((quotientToCoinvariantsFunctor k S).obj Y).ρ (MonoidHom.id (G ⧸ S))))
                          (↑((quotientToCoinvariantsFunctor k S).obj X) : Type u)
                          (↑((quotientToCoinvariantsFunctor k S).obj Y) : Type u)] →
                      [SemilinearMapClass
                            (((quotientToCoinvariantsFunctor k S).obj X).ρ.IntertwiningMap
                              (MonoidHom.comp ((quotientToCoinvariantsFunctor k S).obj Y).ρ (MonoidHom.id (G ⧸ S))))
                            (RingHom.id k) (↑((quotientToCoinvariantsFunctor k S).obj X) : Type u)
                            (↑((quotientToCoinvariantsFunctor k S).obj Y) : Type u)] →
                        (↑((quotientToCoinvariantsFunctor k S).obj X) : Type u) →ₗ[k]
                          (↑((quotientToCoinvariantsFunctor k S).obj Y) : Type u)),
                isIntertwining' := ⋯ })))
        n ≫
      HomologicalComplex.homologyπ (inhomogeneousChains (Functor.obj (quotientToCoinvariantsFunctor k S) Y)) n)
⊢ Eq (α :=
    Functor.obj (functor k G n) X ⟶
      Functor.obj (Functor.comp (D := Rep k (G ⧸ S)) (quotientToCoinvariantsFunctor k S) (functor k (G ⧸ S) n)) Y)
    (CategoryTheory.Functor.map (functor k G n) φ ≫ map (QuotientGroup.mk' S) (Y.toCoinvariantsMkQ S) n)
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.comp (D := Rep k (G ⧸ S)) (quotientToCoinvariantsFunctor k S) (functor k (G ⧸ S) n)) X)
      (map (QuotientGroup.mk' S) (X.toCoinvariantsMkQ S) n)
      (CategoryTheory.Functor.map
        (Functor.comp (D := Rep k (G ⧸ S)) (quotientToCoinvariantsFunctor k S) (functor k (G ⧸ S) n)) φ))

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

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