-- 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
g : G
a : (↑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))
have 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)
          sorry :
        (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))
Tactic: change QuotientAddGroup.lift _ _ _ ((H1Iso A).hom _) = _