-- 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
⊢ 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)

Tactic:
congr 1