-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : (↑(ModuleCat.of k (G → (↑A : Type u_1))) : Type (max u u_1))
g : G × G × G
hf :
  HAdd.hAdd (β := (↑A : Type u_1))
            (HSub.hSub (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
              ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                    (a : (↑A : Type u_1)) → (↑A : Type u_1))
                  ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.2.1 :
                          (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                        (a : (↑A : Type u_1)) → (↑A : Type u_1))
                      (f g.2.2) :
                    (↑A : Type u_1)) :
                (↑A : Type u_1))
              ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                    (a : (↑A : Type u_1)) → (↑A : Type u_1))
                  (f (g.2.1 * g.2.2)) :
                (↑A : Type u_1)))
            ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                  (a : (↑A : Type u_1)) → (↑A : Type u_1))
                (f g.2.1) :
              (↑A : Type u_1)) -
          (HSub.hSub (α := (↑A : Type u_1))
              ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                    (a : (↑A : Type u_1)) → (↑A : Type u_1))
                  ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.2.1 :
                          (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                        (a : (↑A : Type u_1)) → (↑A : Type u_1))
                      (f g.2.2) :
                    (↑A : Type u_1)) :
                (↑A : Type u_1))
              (f (g.1 * (g.2.1 * g.2.2))) +
            f (g.1 * g.2.1)) +
        (HSub.hSub (α := (↑A : Type u_1))
            ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                  (a : (↑A : Type u_1)) → (↑A : Type u_1))
                (f (g.2.1 * g.2.2)) :
              (↑A : Type u_1))
            (f (g.1 * (g.2.1 * g.2.2))) +
          f g.1) -
      (HSub.hSub (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (f g.2.1) :
            (↑A : Type u_1))
          (f (g.1 * g.2.1)) +
        f g.1) =
    0
⊢ Eq.{u_1 + 1} (α := (↑A : Type u_1))
    ((ModuleCat.Hom.hom (d₁₂ A ≫ d₂₃ A) :
          (a : (↑(ModuleCat.of k (G → (↑A : Type u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G × G × G → (↑A : Type u_1))) : Type (max u u_1)))
        f g :
      (↑A : Type u_1))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (G → (↑A : Type u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G × G × G → (↑A : Type u_1))) : Type (max u u_1)))
        f g :
      (↑A : Type u_1))

Tactic:
simp [mul_assoc, Pi.zero_apply (M := fun _ => A)]

Premises used: mul_assoc, Pi.zero_apply