-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i j : ℕ
hij : j + 1 = i
z : (Fin i → G) →₀ (↑X.X₃ : Type u)
hz :
  Eq (α := (↑((inhomogeneousChains X.X₃).X j) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((inhomogeneousChains X.X₃).d i j) :
          (a : (↑((inhomogeneousChains X.X₃).X i) : Type u)) → (↑((inhomogeneousChains X.X₃).X j) : Type u))
        z :
      (↑((inhomogeneousChains X.X₃).X j) : Type u))
    (0 : (↑((inhomogeneousChains X.X₃).X j) : Type u))
y : (Fin i → G) →₀ (↑X.X₂ : Type u)
hy :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := (inhomogeneousChains X.X₂).X i) (Y :=
          HomologicalComplex.X (inhomogeneousChains (G := G) X.3) i)
          (HomologicalComplex.Hom.f (chainsMap (MonoidHom.id G) X.g) i) :
        (a : (↑((inhomogeneousChains X.X₂).X i) : Type u)) → (↑((inhomogeneousChains X.3).X i) : Type u))
      y =
    z
x : (Fin j → G) →₀ (↑X.X₁ : Type u)
hx :
  Eq (α := (Fin j → G) →₀ (↑X.X₂ : Type u))
    ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap :
          (a : (Fin j → G) →₀ (↑X.X₁ : Type u)) → (Fin j → G) →₀ (↑X.X₂ : Type u))
        x :
      (Fin j → G) →₀ (↑X.X₂ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((inhomogeneousChains X.X₂).d i j) :
          (a : (↑((inhomogeneousChains X.X₂).X i) : Type u)) → (↑((inhomogeneousChains X.X₂).X j) : Type u))
        y :
      (↑((inhomogeneousChains X.X₂).X j) : Type u))
⊢ Eq (α :=
    (↑(Functor.obj
          (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
            AddCommGrpCat.carrier))
          ((X₂ (X.map (chainsFunctor k G))).X j)) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X :=
            Functor.obj
              (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
                AddCommGrpCat.carrier))
              ((X₁ (X.map (chainsFunctor k G))).X j))
            (CategoryTheory.Functor.map
              (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
                AddCommGrpCat.carrier))
              (HomologicalComplex.Hom.f (f (X.map (chainsFunctor k G))) j)) :
          (a : (↑((forget₂ (ModuleCat k) Ab).obj ((X.map (chainsFunctor k G)).X₁.X j)) : Type u)) →
            (↑((forget₂ (ModuleCat k) Ab).obj ((X.map (chainsFunctor k G)).X₂.X j)) : Type u))
        x :
      (↑(Functor.obj
            (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommGrpCat.carrier))
            ((X₂ (X.map (chainsFunctor k G))).X j)) :
        Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X :=
            Functor.obj
              (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
                AddCommGrpCat.carrier))
              ((X₂ (X.map (chainsFunctor k G))).X i))
            (CategoryTheory.Functor.map
              (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
                AddCommGrpCat.carrier))
              ((X₂ (X.map (chainsFunctor k G))).d i j)) :
          (a : (↑((forget₂ (ModuleCat k) Ab).obj ((X.map (chainsFunctor k G)).X₂.X i)) : Type u)) →
            (↑((forget₂ (ModuleCat k) Ab).obj ((X.map (chainsFunctor k G)).X₂.X j)) : Type u))
        y :
      (↑(Functor.obj
            (forget₂ (ModuleCat k) (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) Ab (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommGrpCat.carrier))
            ((X₂ (X.map (chainsFunctor k G))).X j)) :
        Type u))

Tactic:
simpa using hx