-- 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
⊢ 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 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⁻¹ 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)