-- 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
x : G
x_1 : (↑A : Type u)
⊢ Eq (α := (↑(H1 A) : Type u))
    ((TensorProduct.lift (mkH1OfIsTrivial A) :
          (a : Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) → (↑(H1 A) : Type u))
        ((QuotientAddGroup.lift (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup
                (AddMonoidHom.comp
                  ((Finsupp.liftAddHom :
                      (a : G → (↑A : Type u) →+ Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) →
                        (G →₀ (↑A : Type u)) →+ Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
                    fun (g : G) ↦
                    (↑((TensorProduct.mk ℤ (Additive (Abelianization G)) (↑A : Type u) :
                              (a : Additive (Abelianization G)) →
                                (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
                            ((Additive.ofMul : (a : Abelianization G) → Additive (Abelianization G))
                              ((Abelianization.of : (a : G) → Abelianization G) g)) :
                          (↑A : Type u) →ₗ[ℤ] Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) :
                      (↑A : Type u) →+ Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)))
                  (cycles₁ A).toAddSubgroup.subtype)
                ⋯ :
              (a :
                  ↥(ModuleCat.Hom.hom (shortComplexH1 A).g).ker ⧸
                    (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup) →
                Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (H1Iso A).hom :
                (a : (↑(H1 A) : Type u)) → (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u))
              (((↑(LinearEquiv.toAddEquiv
                        (LinearEquiv.ofLinear (ModuleCat.Hom.hom (H1Iso A).symm.hom)
                          (ModuleCat.Hom.hom (H1Iso A).symm.inv) ⋯ ⋯)) :
                    (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u) →+ (↑(H1 A) : Type u)) :
                  (a :
                      ↥(ModuleCat.Hom.hom (shortComplexH1 A).g).ker ⧸
                        (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup) →
                    (↑(H1 A) : Type u))
                ((QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup :
                      (a : ↥(cycles₁ A)) →
                        ↥(ModuleCat.Hom.hom (shortComplexH1 A).g).ker ⧸
                          (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup)
                    (((↑(LinearEquiv.toAddEquiv
                              (LinearEquiv.ofLinear (ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).symm.hom)
                                (ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).symm.inv) ⋯ ⋯)) :
                          (G →₀ (↑A : Type u)) →+ ↥(cycles₁ A)) :
                        (a : G →₀ (↑A : Type u)) → ↥(cycles₁ A))
                      ((singleAddHom x : (a : (↑A : Type u)) → G →₀ (↑A : Type u)) x_1)) :
                  ↥(ModuleCat.Hom.hom (shortComplexH1 A).g).ker ⧸
                    (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup))) :
          Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) :
      (↑(H1 A) : Type u))
    (Function.comp (β := G →₀ (↑A : Type u))
        (Function.comp (β := ↥(cycles₁ A))
          (Function.comp (β :=
            ↥(ModuleCat.Hom.hom (shortComplexH1 A).g).ker ⧸ (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup)
            (Function.comp (β := (↑(H1 A) : Type u)) (⇑LinearMap.id : (a : (↑(H1 A) : Type u)) → (↑(H1 A) : Type u))
              (⇑(↑(LinearEquiv.toAddEquiv
                        (LinearEquiv.ofLinear (ModuleCat.Hom.hom (H1Iso A).symm.hom)
                          (ModuleCat.Hom.hom (H1Iso A).symm.inv) ⋯ ⋯)) :
                    (↑(shortComplexH1 A).moduleCatLeftHomologyData.H : Type u) →+ (↑(H1 A) : Type u)) :
                (a :
                    ↥(ModuleCat.Hom.hom (shortComplexH1 A).g).ker ⧸
                      (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup) →
                  (↑(H1 A) : Type u)))
            (⇑(QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup) :
              (a : ↥(cycles₁ A)) →
                ↥(ModuleCat.Hom.hom (shortComplexH1 A).g).ker ⧸
                  (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup))
          (⇑(↑(LinearEquiv.toAddEquiv
                    (LinearEquiv.ofLinear (ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).symm.hom)
                      (ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).symm.inv) ⋯ ⋯)) :
                (G →₀ (↑A : Type u)) →+ ↥(cycles₁ A)) :
            (a : G →₀ (↑A : Type u)) → ↥(cycles₁ A)))
        (⇑(singleAddHom x) : (a : (↑A : Type u)) → G →₀ (↑A : Type u)) x_1 :
      (↑(H1 A) : Type u))

Tactic:
simpa [AddSubgroup.subtype, -π_comp_H1Iso_inv_apply, QuotientAddGroup.mk',
          cycles₁IsoOfIsTrivial_inv_apply (A := A)] using (π_comp_H1Iso_inv_apply A _).symm

Premises used: QuotientAddGroup.mk', AddSubgroup.subtype, groupHomology.π_comp_H1Iso_inv_apply, groupHomology.cycles₁IsoOfIsTrivial_inv_apply, Eq.symm