-- 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)
subst :
  ∀
    (hz :
      Eq (α := (↑((inhomogeneousCochains X.X₃).X (i + 1)) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (Y := (inhomogeneousCochains X.X₃).X (i + 1))
                ((inhomogeneousCochains X.X₃).d i (i + 1)) :
              (a : (↑((inhomogeneousCochains X.X₃).X i) : Type u)) →
                (↑((inhomogeneousCochains X.X₃).X (i + 1)) : Type u))
            z :
          (↑((inhomogeneousCochains X.X₃).X (i + 1)) : Type u))
        (0 : (↑((inhomogeneousCochains X.X₃).X (i + 1)) : Type u)))
    (x : (Fin (i + 1) → G) → (↑X.X₁ : Type u))
    (hx :
      Eq (α := (Fin (i + 1) → 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) (Y := (inhomogeneousCochains X.X₂).X (i + 1))
              ((inhomogeneousCochains X.X₂).d i (i + 1)) :
            (a : (↑((inhomogeneousCochains X.X₂).X i) : Type u)) → (↑((inhomogeneousCochains X.X₂).X (i + 1)) : Type u))
          y)),
    Eq (α := (↑(ModuleCat.of k ((Fin (i + 1) → G) → (↑X.X₃ : Type u))) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (inhomogeneousCochains.d X.X₃ i) :
            (a : (↑(ModuleCat.of k ((Fin i → G) → (↑X.X₃ : Type u))) : Type u)) →
              (↑(ModuleCat.of k ((Fin (i + 1) → G) → (↑X.X₃ : Type u))) : Type u))
          z :
        (↑(ModuleCat.of k ((Fin (i + 1) → G) → (↑X.X₃ : Type u))) : Type u))
      (0 : (↑(ModuleCat.of k ((Fin (i + 1) → G) → (↑X.X₃ : Type u))) : Type u))
⊢ Eq (α := (↑(ModuleCat.of k ((Fin (i + 1) → G) → (↑X.X₃ : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (inhomogeneousCochains.d X.X₃ i) :
          (a : (↑(ModuleCat.of k ((Fin i → G) → (↑X.X₃ : Type u))) : Type u)) →
            (↑(ModuleCat.of k ((Fin (i + 1) → G) → (↑X.X₃ : Type u))) : Type u))
        z :
      (↑(ModuleCat.of k ((Fin (i + 1) → G) → (↑X.X₃ : Type u))) : Type u))
    (0 : (↑(ModuleCat.of k ((Fin (i + 1) → G) → (↑X.X₃ : Type u))) : Type u))

Tactic:
subst hij