-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
i : ℕ
x : leftRegular k G ⟶ A
pos :
  ∀ (hi : Even i),
    Eq (α := (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
      ((ModuleCat.Hom.hom
              (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) i) ≫
                (moduleCatCochainComplex A g).d i (i + 1)) :
            (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
              (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
          x :
        (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
      ((ModuleCat.Hom.hom
              (CategoryStruct.comp (Y :=
                HomologicalComplex.X
                  (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A) (i + 1))
                (HomologicalComplex.d
                  (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A) i (i + 1))
                (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) (i + 1)))) :
            (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
              (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
          x :
        (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
⊢ Eq (α := (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
    ((ModuleCat.Hom.hom
            (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) i) ≫
              (moduleCatCochainComplex A g).d i (i + 1)) :
          (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
            (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
        x :
      (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
    ((ModuleCat.Hom.hom
            (CategoryStruct.comp (Y :=
              HomologicalComplex.X (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A)
                (i + 1))
              (HomologicalComplex.d
                (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A) i (i + 1))
              (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) (i + 1)))) :
          (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
            (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
        x :
      (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
have neg : ∀ (hi : ¬Even i),
  Eq (α := (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
    ((ModuleCat.Hom.hom
            (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) i) ≫
              (moduleCatCochainComplex A g).d i (i + 1)) :
          (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
            (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
        x :
      (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
    ((ModuleCat.Hom.hom
            (CategoryStruct.comp (Y :=
              HomologicalComplex.X (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A)
                (i + 1))
              (HomologicalComplex.d
                (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (resolution k g hg)) k A) i (i + 1))
              (Iso.hom ((fun (x : ℕ) ↦ A.leftRegularHomEquiv.toModuleIso) (i + 1)))) :
          (a : (↑(((resolution k g hg).complex.linearYonedaObj k A).X i) : Type u)) →
            (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
        x :
      (↑((moduleCatCochainComplex A g).X (i + 1)) : Type u))
Tactic: by_cases hi : Even i