-- 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 :
  ∀ (x : G) (x_1 : (↑A : Type u)),
    Eq (α := (↑(H1 A) : Type u))
      ((AddMonoidHom.comp
              ((fun (f : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u) →+ (↑(H1 A) : Type u)) ↦
                  (f.comp
                      (↑(cycles₁IsoOfIsTrivial A).symm.toLinearEquiv.toAddEquiv :
                        (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u) →+
                          (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) :
                    (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u) →+ (↑(H1 A) : Type u)))
                (AddMonoidHom.comp
                  ((fun (f : (↑(H1 A) : Type u) →+ (↑(H1 A) : Type u)) ↦
                      (f.comp
                          (↑(H1Iso A).symm.toLinearEquiv.toAddEquiv :
                            (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u) →+ (↑(H1 A) : Type u)) :
                        (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u) →+ (↑(H1 A) : Type u)))
                    (TensorProduct.lift (mkH1OfIsTrivial A) ∘ₗ H1ToTensorOfIsTrivial A).toAddMonoidHom)
                  (QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup)))
              (singleAddHom x) :
            (a : (↑A : Type u)) → (↑(H1 A) : Type u))
          x_1 :
        (↑(H1 A) : Type u))
      ((AddMonoidHom.comp
              ((fun (f : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u) →+ (↑(H1 A) : Type u)) ↦
                  (f.comp
                      (↑(cycles₁IsoOfIsTrivial A).symm.toLinearEquiv.toAddEquiv :
                        (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u) →+
                          (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) :
                    (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u) →+ (↑(H1 A) : Type u)))
                (AddMonoidHom.comp
                  ((fun (f : (↑(H1 A) : Type u) →+ (↑(H1 A) : Type u)) ↦
                      (f.comp
                          (↑(H1Iso A).symm.toLinearEquiv.toAddEquiv :
                            (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u) →+ (↑(H1 A) : Type u)) :
                        (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u) →+ (↑(H1 A) : Type u)))
                    (LinearMap.toAddMonoidHom (R := ℤ) (modM₁ := AddCommGroup.toIntModule (↑(H1 A) : Type u))
                      LinearMap.id))
                  (QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup)))
              (singleAddHom x) :
            (a : (↑A : Type u)) → (↑(H1 A) : Type u))
          x_1 :
        (↑(H1 A) : Type u))
⊢ Eq.{u + 1} (α := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u) →+ (↑(H1 A) : Type u))
    ((fun (f : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u) →+ (↑(H1 A) : Type u)) ↦
        (f.comp
            (↑(cycles₁IsoOfIsTrivial A).symm.toLinearEquiv.toAddEquiv :
              (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u) →+ (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) :
          (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u) →+ (↑(H1 A) : Type u)))
      (AddMonoidHom.comp
        ((fun (f : (↑(H1 A) : Type u) →+ (↑(H1 A) : Type u)) ↦
            (f.comp
                (↑(H1Iso A).symm.toLinearEquiv.toAddEquiv :
                  (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u) →+ (↑(H1 A) : Type u)) :
              (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u) →+ (↑(H1 A) : Type u)))
          (TensorProduct.lift (mkH1OfIsTrivial A) ∘ₗ H1ToTensorOfIsTrivial A).toAddMonoidHom)
        (QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup)))
    ((fun (f : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u) →+ (↑(H1 A) : Type u)) ↦
        (f.comp
            (↑(cycles₁IsoOfIsTrivial A).symm.toLinearEquiv.toAddEquiv :
              (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u) →+ (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) :
          (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u) →+ (↑(H1 A) : Type u)))
      (AddMonoidHom.comp
        ((fun (f : (↑(H1 A) : Type u) →+ (↑(H1 A) : Type u)) ↦
            (f.comp
                (↑(H1Iso A).symm.toLinearEquiv.toAddEquiv :
                  (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u) →+ (↑(H1 A) : Type u)) :
              (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u) →+ (↑(H1 A) : Type u)))
          (LinearMap.toAddMonoidHom (R := ℤ) (modM₁ := AddCommGroup.toIntModule (↑(H1 A) : Type u)) LinearMap.id))
        (QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup)))

Tactic:
ext