-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Goal:
k : Type u
inst : CommRing k
G H K : Type u
inst_1 : Group G
inst_2 : Group H
inst_3 : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
refine_2 :
  Hom.τ₂
      (mapShortComplexH2 (g.comp f)
        (φ ≫
          ofHom
            {
              toLinearMap :=
                (↑(Hom.hom ψ) :
                  [inst_4 : FunLike (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (↑B : Type u) (↑C : Type u)] →
                    [SemilinearMapClass (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (RingHom.id k) (↑B : Type u)
                          (↑C : Type u)] →
                      (↑B : Type u) →ₗ[k] (↑C : Type u)),
              isIntertwining' := ⋯ })) =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂
refine_2₁ :
  ∀ (a : G × G) (x : (↑A : Type u)) (a_1 : K × K),
    Eq (α := (↑C : Type u))
      ((((ModuleCat.Hom.hom
                      (Hom.τ₂
                        (mapShortComplexH2 (g.comp f)
                          (φ ≫
                            ofHom
                              {
                                toLinearMap :=
                                  (↑(Hom.hom ψ) :
                                    [inst_4 :
                                        FunLike (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (↑B : Type u)
                                          (↑C : Type u)] →
                                      [SemilinearMapClass (B.ρ.IntertwiningMap (MonoidHom.comp C.ρ g)) (RingHom.id k)
                                            (↑B : Type u) (↑C : Type u)] →
                                        (↑B : Type u) →ₗ[k] (↑C : Type u)),
                                isIntertwining' := ⋯ :
                                IntertwiningMap (MonoidHom.comp B.ρ f) ((MonoidHom.comp C.ρ g).comp f) }))) ∘ₗ
                    lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (K × K × K →₀ (↑C : Type u)),
                            X₂ := ModuleCat.of k (K × K →₀ (↑C : Type u)), X₃ := ModuleCat.of k (K →₀ (↑C : Type u)),
                            f := d₃₂ C, g := d₂₁ C, zero := ⋯ }.X₂ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (K × K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K × K →₀ (↑C : Type u)),
                      X₃ := ModuleCat.of k (K →₀ (↑C : Type u)), f := d₃₂ C, g := d₂₁ C, zero := ⋯ :
                      ShortComplex (ModuleCat k) }.X₂ :
                Type u)) :
            (a : K × K) → (↑C : Type u))
          a_1 :
        (↑C : Type u))
      ((((ModuleCat.Hom.hom (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂ ∘ₗ lsingle a :
                  (a : (↑A : Type u)) →
                    (↑{ X₁ := ModuleCat.of k (K × K × K →₀ (↑C : Type u)),
                            X₂ := ModuleCat.of k (K × K →₀ (↑C : Type u)), X₃ := ModuleCat.of k (K →₀ (↑C : Type u)),
                            f := d₃₂ C, g := d₂₁ C, zero := ⋯ }.X₂ :
                      Type u))
                x :
              (↑{ X₁ := ModuleCat.of k (K × K × K →₀ (↑C : Type u)), X₂ := ModuleCat.of k (K × K →₀ (↑C : Type u)),
                      X₃ := ModuleCat.of k (K →₀ (↑C : Type u)), f := d₃₂ C, g := d₂₁ C, zero := ⋯ :
                      ShortComplex (ModuleCat k) }.X₂ :
                Type u)) :
            (a : K × K) → (↑C : Type u))
          a_1 :
        (↑C : Type u))
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₂ =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂

Tactic:
{ simp only [shortComplexH2]
    ext
    simp [Prod.map] }

Premises used: Prod.map, groupHomology.shortComplexH2