-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
⊢ 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)))
have 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))
Tactic: ext