-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
h :
  ∀ (g : G) (a : (↑A : Type u)),
    Eq (α := Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
      ((((Multiplicative.toAdd :
                  (a : Multiplicative ((↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))) →
                    (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
                ((MonoidHom.comp
                      ((AddMonoidHom.toMultiplicativeRight :
                          (a :
                              Additive (Abelianization G) →+
                                (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) →
                            Abelianization G →*
                              Multiplicative ((↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)))
                        (LinearMap.compr₂ₛₗ (TensorProduct.mk ℤ (Additive (Abelianization G)) (↑A : Type u))
                            (H1ToTensorOfIsTrivial A ∘ₗ TensorProduct.lift (mkH1OfIsTrivial A))).toAddMonoidHom)
                      Abelianization.of :
                    (a : G) → Multiplicative ((↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)))
                  g) :
              (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) :
            (a : (↑A : Type u)) → Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
          a :
        Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
      ((((Multiplicative.toAdd :
                  (a : Multiplicative ((↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))) →
                    (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
                ((MonoidHom.comp
                      ((AddMonoidHom.toMultiplicativeRight :
                          (a :
                              Additive (Abelianization G) →+
                                (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) →
                            Abelianization G →*
                              Multiplicative ((↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)))
                        (LinearMap.toAddMonoidHom
                          (LinearMap.compr₂ₛₗ (TensorProduct.mk ℤ (Additive (Abelianization G)) (↑A : Type u))
                            LinearMap.id)))
                      Abelianization.of :
                    (a : G) → Multiplicative ((↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)))
                  g) :
              (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) :
            (a : (↑A : Type u)) → Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
          a :
        Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
⊢ (LinearMap.compr₂ₛₗ (TensorProduct.mk ℤ (Additive (Abelianization G)) (↑A : Type u))
        (H1ToTensorOfIsTrivial A ∘ₗ TensorProduct.lift (mkH1OfIsTrivial A))).toAddMonoidHom =
    LinearMap.toAddMonoidHom
      (LinearMap.compr₂ₛₗ (TensorProduct.mk ℤ (Additive (Abelianization G)) (↑A : Type u)) LinearMap.id)

Tactic:
ext g a

Premises used: CategoryTheory.ShortComplex.g