Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
x✝¹ : G
x✝ : ↑A
⊢ (((((⇑(TensorProduct.lift (mkH1OfIsTrivial A)) ∘
                ⇑(QuotientAddGroup.lift (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup
                      ((Finsupp.liftAddHom fun g ↦
                            ↑((TensorProduct.mk ℤ (Additive (Abelianization G)) ↑A)
                                (Additive.ofMul (Abelianization.of g)))).comp
                        (cycles₁ A).toAddSubgroup.subtype)
                      ⋯) ∘
                  ⇑↑(ModuleCat.Hom.hom (H1Iso A).hom)) ∘
              ⇑↑(LinearEquiv.ofLinearMap (ModuleCat.Hom.hom (H1Iso A).symm.hom) (ModuleCat.Hom.hom (H1Iso A).symm.inv) ⋯
                      ⋯).toAddEquiv) ∘
            ⇑(QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup)) ∘
          ⇑↑(LinearEquiv.ofLinearMap (ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).symm.hom)
                  (ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).symm.inv) ⋯ ⋯).toAddEquiv) ∘
        ⇑(singleAddHom x✝¹))
      x✝ =
    ((((⇑LinearMap.id ∘
              ⇑↑(LinearEquiv.ofLinearMap (ModuleCat.Hom.hom (H1Iso A).symm.hom) (ModuleCat.Hom.hom (H1Iso A).symm.inv) ⋯
                      ⋯).toAddEquiv) ∘
            ⇑(QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup)) ∘
          ⇑↑(LinearEquiv.ofLinearMap (ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).symm.hom)
                  (ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).symm.inv) ⋯ ⋯).toAddEquiv) ∘
        ⇑(singleAddHom x✝¹))
      x✝

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

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
x✝¹ : G
x✝ : ↑A
⊢ (TensorProduct.lift (mkH1OfIsTrivial A))
      ((QuotientAddGroup.lift (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup
          ((Finsupp.liftAddHom fun g ↦
                ↑((TensorProduct.mk ℤ (Additive (Abelianization G)) ↑A) (Additive.ofMul (Abelianization.of g)))).comp
            (cycles₁ A).toAddSubgroup.subtype)
          ⋯)
        ((ConcreteCategory.hom (H1Iso A).hom)
          (↑(LinearEquiv.ofLinearMap (ModuleCat.Hom.hom (H1Iso A).symm.hom) (ModuleCat.Hom.hom (H1Iso A).symm.inv) ⋯
                  ⋯).toAddEquiv
            ((QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup)
              (↑(LinearEquiv.ofLinearMap (ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).symm.hom)
                      (ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).symm.inv) ⋯ ⋯).toAddEquiv
                ((singleAddHom x✝¹) x✝)))))) =
    ((((⇑LinearMap.id ∘
              ⇑↑(LinearEquiv.ofLinearMap (ModuleCat.Hom.hom (H1Iso A).symm.hom) (ModuleCat.Hom.hom (H1Iso A).symm.inv) ⋯
                      ⋯).toAddEquiv) ∘
            ⇑(QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup)) ∘
          ⇑↑(LinearEquiv.ofLinearMap (ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).symm.hom)
                  (ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).symm.inv) ⋯ ⋯).toAddEquiv) ∘
        ⇑(singleAddHom x✝¹))
      x✝