-- 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
x : G
x_1 : (↑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)
have 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)
              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))
            (((↑(LinearEquiv.toAddEquiv
                      (LinearEquiv.ofLinear (ModuleCat.Hom.hom (H1Iso A).symm.hom)
                        (ModuleCat.Hom.hom (H1Iso A).symm.inv) sorry sorry)) :
                  (↑(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) sorry sorry)) :
                        (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) sorry sorry)) :
                  (↑(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) sorry sorry)) :
              (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: change TensorProduct.lift _ (QuotientAddGroup.lift _ _ _ ((H1Iso A).hom _)) = _