-- 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)
H :
  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))
⊢ Eq (α := (↑(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))
            (Function.comp (β := Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
              (⇑(TensorProduct.lift (mkH1OfIsTrivial A)) :
                (a : Additive (Abelianization G) ⊗[ℤ] (↑A : Type u)) → (↑(H1 A) : Type u))
              (Function.comp (β :=
                ↥(cycles₁ A).toAddSubgroup ⧸ (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup)
                (⇑(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 : ↥(cycles₁ A).toAddSubgroup ⧸ (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup) →
                    Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
                (⇑(↑(ModuleCat.Hom.hom (H1Iso A).hom) :
                      (↑(H1 A) : Type u) →+
                        ↥(cycles₁ A).toAddSubgroup ⧸ (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup) :
                  (a : (↑(H1 A) : Type u)) →
                    ↥(cycles₁ A).toAddSubgroup ⧸ (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup)))
            (⇑(↑(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)
    (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)

Tactic:
change TensorProduct.lift _ (QuotientAddGroup.lift _ _ _ ((H1Iso A).hom _)) = _

Premises used: CategoryTheory.ConcreteCategory.hom, groupHomology.H1Iso, TensorProduct.lift, CategoryTheory.Iso.hom, DFunLike.coe, QuotientAddGroup.lift