-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g_1 : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g_1) x
j : ℕ
a : (↑A : Type u)
g : G
pos :
  ∀ (hj : Even (j + 1)),
    Eq (α := (↑((moduleCatChainComplex A g_1).X j) : Type u))
      (((LinearMap.compr₂
                    (A.coinvariantsTensorMk
                      (HomologicalComplex.X (ProjectiveResolution.complex (resolution k g_1⁻¹ ⋯)) (j + 1)))
                    (ModuleCat.Hom.hom
                      (CategoryStruct.comp (Y := (moduleCatChainComplex A g_1).X (j + 1))
                        (Iso.hom ((fun (x : ℕ) ↦ A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso) (j + 1)))
                        ((moduleCatChainComplex A g_1).d (j + 1) j))) :
                  (a : (↑A : Type u)) →
                    (↑((resolution k g_1⁻¹ ⋯).complex.X (j + 1)) : Type u) →ₗ[k]
                      (↑((moduleCatChainComplex A g_1).X j) : Type u))
                a ∘ₗ
              lsingle g :
            (a : k) → (↑((moduleCatChainComplex A g_1).X j) : Type u))
          1 :
        (↑((moduleCatChainComplex A g_1).X j) : Type u))
      (((LinearMap.compr₂
                    (A.coinvariantsTensorMk
                      (HomologicalComplex.X (ProjectiveResolution.complex (resolution k g_1⁻¹ ⋯)) (j + 1)))
                    (ModuleCat.Hom.hom
                      ((HomologicalComplex.coinvariantsTensorObj A
                              (ProjectiveResolution.complex (resolution k g_1⁻¹ ⋯))).d
                          (j + 1) j ≫
                        Iso.hom ((fun (x : ℕ) ↦ A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso) j))) :
                  (a : (↑A : Type u)) →
                    (↑((resolution k g_1⁻¹ ⋯).complex.X (j + 1)) : Type u) →ₗ[k]
                      (↑((moduleCatChainComplex A g_1).X j) : Type u))
                a ∘ₗ
              lsingle g :
            (a : k) → (↑((moduleCatChainComplex A g_1).X j) : Type u))
          1 :
        (↑((moduleCatChainComplex A g_1).X j) : Type u))
⊢ Eq (α := (↑((moduleCatChainComplex A g_1).X j) : Type u))
    (((LinearMap.compr₂
                  (A.coinvariantsTensorMk
                    (HomologicalComplex.X (ProjectiveResolution.complex (resolution k g_1⁻¹ ⋯)) (j + 1)))
                  (ModuleCat.Hom.hom
                    (CategoryStruct.comp (Y := (moduleCatChainComplex A g_1).X (j + 1))
                      (Iso.hom ((fun (x : ℕ) ↦ A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso) (j + 1)))
                      ((moduleCatChainComplex A g_1).d (j + 1) j))) :
                (a : (↑A : Type u)) →
                  (↑((resolution k g_1⁻¹ ⋯).complex.X (j + 1)) : Type u) →ₗ[k]
                    (↑((moduleCatChainComplex A g_1).X j) : Type u))
              a ∘ₗ
            lsingle g :
          (a : k) → (↑((moduleCatChainComplex A g_1).X j) : Type u))
        1 :
      (↑((moduleCatChainComplex A g_1).X j) : Type u))
    (((LinearMap.compr₂
                  (A.coinvariantsTensorMk
                    (HomologicalComplex.X (ProjectiveResolution.complex (resolution k g_1⁻¹ ⋯)) (j + 1)))
                  (ModuleCat.Hom.hom
                    ((HomologicalComplex.coinvariantsTensorObj A
                            (ProjectiveResolution.complex (resolution k g_1⁻¹ ⋯))).d
                        (j + 1) j ≫
                      Iso.hom ((fun (x : ℕ) ↦ A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso) j))) :
                (a : (↑A : Type u)) →
                  (↑((resolution k g_1⁻¹ ⋯).complex.X (j + 1)) : Type u) →ₗ[k]
                    (↑((moduleCatChainComplex A g_1).X j) : Type u))
              a ∘ₗ
            lsingle g :
          (a : k) → (↑((moduleCatChainComplex A g_1).X j) : Type u))
        1 :
      (↑((moduleCatChainComplex A g_1).X j) : Type u))
have neg : ∀ (hj : ¬Even (j + 1)),
  Eq (α := (↑((moduleCatChainComplex A g_1).X j) : Type u))
    (((LinearMap.compr₂
                  (A.coinvariantsTensorMk
                    (HomologicalComplex.X (ProjectiveResolution.complex (resolution k g_1⁻¹ sorry)) (j + 1)))
                  (ModuleCat.Hom.hom
                    (CategoryStruct.comp (Y := (moduleCatChainComplex A g_1).X (j + 1))
                      (Iso.hom ((fun (x : ℕ) ↦ A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso) (j + 1)))
                      ((moduleCatChainComplex A g_1).d (j + 1) j))) :
                (a : (↑A : Type u)) →
                  (↑((resolution k g_1⁻¹ sorry).complex.X (j + 1)) : Type u) →ₗ[k]
                    (↑((moduleCatChainComplex A g_1).X j) : Type u))
              a ∘ₗ
            lsingle g :
          (a : k) → (↑((moduleCatChainComplex A g_1).X j) : Type u))
        1 :
      (↑((moduleCatChainComplex A g_1).X j) : Type u))
    (((LinearMap.compr₂
                  (A.coinvariantsTensorMk
                    (HomologicalComplex.X (ProjectiveResolution.complex (resolution k g_1⁻¹ sorry)) (j + 1)))
                  (ModuleCat.Hom.hom
                    ((HomologicalComplex.coinvariantsTensorObj A
                            (ProjectiveResolution.complex (resolution k g_1⁻¹ sorry))).d
                        (j + 1) j ≫
                      Iso.hom ((fun (x : ℕ) ↦ A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso) j))) :
                (a : (↑A : Type u)) →
                  (↑((resolution k g_1⁻¹ sorry).complex.X (j + 1)) : Type u) →ₗ[k]
                    (↑((moduleCatChainComplex A g_1).X j) : Type u))
              a ∘ₗ
            lsingle g :
          (a : k) → (↑((moduleCatChainComplex A g_1).X j) : Type u))
        1 :
      (↑((moduleCatChainComplex A g_1).X j) : Type u))
Tactic: by_cases hj : Even (j + 1)