-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
m : ℕ
h : QuasiIsoAt (C := Rep k G) (K := Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (resolution.π k g) m
pos :
  ∀ (hm : Odd (m + 1)),
    Eq (α :=
      Submodule k
        (↑(ShortComplex.X₂
              (ShortComplex.map
                (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
                (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
                  fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier)))) :
          Type u))
      (LinearMap.range
        (ModuleCat.Hom.hom
          (ShortComplex.f
            (ShortComplex.map
              (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
              (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
                fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))))))
      (LinearMap.ker
        (ModuleCat.Hom.hom
          (ShortComplex.g
            (ShortComplex.map
              (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
              (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
                fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))))))
⊢ Eq (α :=
    Submodule k
      (↑(ShortComplex.X₂
            (ShortComplex.map
              (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
              (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
                fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier)))) :
        Type u))
    (LinearMap.range
      (ModuleCat.Hom.hom
        (ShortComplex.f
          (ShortComplex.map
            (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
            (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
              fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))))))
    (LinearMap.ker
      (ModuleCat.Hom.hom
        (ShortComplex.g
          (ShortComplex.map
            (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
            (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
              fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))))))
have neg : ∀ (hm : ¬Odd (m + 1)),
  Eq (α :=
    Submodule k
      (↑(ShortComplex.X₂
            (ShortComplex.map
              (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
              (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
                fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier)))) :
        Type u))
    (LinearMap.range
      (ModuleCat.Hom.hom
        (ShortComplex.f
          (ShortComplex.map
            (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
            (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
              fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))))))
    (LinearMap.ker
      (ModuleCat.Hom.hom
        (ShortComplex.g
          (ShortComplex.map
            (HomologicalComplex.sc' (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) (m + 2) (m + 1) m)
            (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
              fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))))))
Tactic: by_cases hm : Odd (m + 1)