∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact)
  {i j : ℕ} (hij : j + 1 = i) (z : (Fin i → G) →₀ ↑X.X₃.V)
  (hz : (CategoryTheory.ConcreteCategory.hom ((groupHomology.inhomogeneousChains X.X₃).d i j)) z = 0)
  (y : (Fin i → G) →₀ ↑X.X₂.V),
  (CategoryTheory.ConcreteCategory.hom ((groupHomology.chainsMap (MonoidHom.id G) X.g).f i)) y = z →
    ∀ (x : (Fin j → G) →₀ ↑X.X₁.V)
      (hx :
        (Finsupp.mapRange.linearMap (ModuleCat.Hom.hom X.f.hom)) x =
          (CategoryTheory.ConcreteCategory.hom ((groupHomology.inhomogeneousChains X.X₂).d i j)) y),
      (CategoryTheory.ConcreteCategory.hom (groupHomology.δ hX i j hij))
          ((CategoryTheory.ConcreteCategory.hom (groupHomology.π X.X₃ i)) (groupHomology.cyclesMk i j ⋯ z ⋯)) =
        (CategoryTheory.ConcreteCategory.hom (groupHomology.π X.X₁ j)) (groupHomology.cyclesMkOfCompEqD hX hx)