-- 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
g : G
a : (↑A : Type u)
change :
  Eq (α := Additive (Abelianization G) ⊗[ℤ] (↑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))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) ((isoCycles₁ A).inv ≫ π A 1) :
              (a : ↥(cycles₁ A)) → (↑(H1 A) : Type u))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) (cycles₁IsoOfIsTrivial A).inv :
                  (a : G →₀ (↑A : Type u)) → ↥(cycles₁ A))
                (single g a) :
              ↥(cycles₁ A)))) :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    ((Additive.ofMul : (a : Abelianization G) → Additive (Abelianization G))
          ((Abelianization.of : (a : G) → Abelianization G) g) ⊗ₜ[ℤ]
        a :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
⊢ Eq (α := Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))
    (Function.comp (α := (↑(H1 A) : Type u)) (β :=
        ↥(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) :
          (a : (↑(H1 A) : Type u)) →
            ↥(cycles₁ A).toAddSubgroup ⧸ (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) ((isoCycles₁ A).inv ≫ π A 1) :
              (a : ↥(cycles₁ A)) → (↑(H1 A) : Type u))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                    ModuleCat.carrier) (cycles₁IsoOfIsTrivial A).inv :
                  (a : G →₀ (↑A : Type u)) → ↥(cycles₁ A))
                (single g a) :
              ↥(cycles₁ A)) :
          (↑(H1 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 :
      Additive (Abelianization G) ⊗[ℤ] (↑A : Type u))

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

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