-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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 (α :=
    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)) φ))
have 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' := sorry }))
      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' := sorry })))
      n ≫
    HomologicalComplex.homologyπ (inhomogeneousChains (Functor.obj (quotientToCoinvariantsFunctor k S) Y)) 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]