-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence (goal)
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 (α := (↑(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))
have 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))
Tactic: subst hij
Cleared hypotheses: j, hij, hz, x, hx