-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i j : ℕ
hij : i + 1 = j
z : (Fin i → G) → (↑X.X₃ : Type u)
hz :
  Eq (α := (↑((inhomogeneousCochains X.X₃).X j) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) ((inhomogeneousCochains X.X₃).d i j) :
          (a : (↑((inhomogeneousCochains X.X₃).X i) : Type u)) → (↑((inhomogeneousCochains X.X₃).X j) : Type u))
        z :
      (↑((inhomogeneousCochains X.X₃).X j) : Type u))
    (0 : (↑((inhomogeneousCochains 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 := HomologicalComplex.X (inhomogeneousCochains (G := G) X.2) i) (Y :=
          (inhomogeneousCochains X.X₃).X i) (HomologicalComplex.Hom.f (cochainsMap (MonoidHom.id G) X.g) i) :
        (a : (↑((inhomogeneousCochains X.2).X i) : Type u)) → (↑((inhomogeneousCochains X.X₃).X i) : Type u))
      y =
    z
x : (Fin j → G) → (↑X.X₁ : Type u)
hx :
  Eq (α := (Fin j → G) → (↑X.X₂ : Type u)) ((⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑X.X₂ : Type u)) ∘ x)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) ((inhomogeneousCochains X.X₂).d i j) :
        (a : (↑((inhomogeneousCochains X.X₂).X i) : Type u)) → (↑((inhomogeneousCochains X.X₂).X j) : Type u))
      y)
⊢ 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 (cochainsFunctor 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 (cochainsFunctor 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 (cochainsFunctor k G))) j)) :
          (a : (↑((forget₂ (ModuleCat k) Ab).obj ((X.map (cochainsFunctor k G)).X₁.X j)) : Type u)) →
            (↑((forget₂ (ModuleCat k) Ab).obj ((X.map (cochainsFunctor 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 (cochainsFunctor 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 (cochainsFunctor 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 (cochainsFunctor k G))).d i j)) :
          (a : (↑((forget₂ (ModuleCat k) Ab).obj ((X.map (cochainsFunctor k G)).X₂.X i)) : Type u)) →
            (↑((forget₂ (ModuleCat k) Ab).obj ((X.map (cochainsFunctor 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 (cochainsFunctor k G))).X j)) :
        Type u))

Tactic:
simpa using hx