-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality (goal)
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 ψ).τ₂
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ CategoryTheory.Functor.map (resFunctor f) ψ)).τ₂ =
    (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂
have 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' := sorry :
                              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 := sorry }.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 := sorry :
                    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 := sorry }.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 := sorry :
                    ShortComplex (ModuleCat k) }.X₂ :
              Type u)) :
          (a : K × K) → (↑C : Type u))
        a_1 :
      (↑C : Type u))
Tactic: { simp only [shortComplexH2]
    ext
    simp [Prod.map] }