-- 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
z : ↥X.X₃.ρ.invariants
y : (↑X.X₂ : Type u)
hy : (Rep.Hom.hom X.g : (a : (↑X.X₂ : Type u)) → (↑X.X₃ : Type u)) y = (↑z : (↑X.X₃ : Type u))
x : G → (↑X.X₁ : Type u)
hx :
  Eq (α := 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) (d₀₁ X.X₂) :
        (a : (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u)) → (↑(ModuleCat.of k (G → (↑X.X₂ : Type u))) : Type u))
      y)
⊢ Eq (α := (↑((inhomogeneousCochains X.X₃).X 0) : Type u))
    ((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) 0) (Y :=
            (inhomogeneousCochains X.X₃).X 0) (HomologicalComplex.Hom.f (cochainsMap (MonoidHom.id G) X.g) 0) :
          (a : (↑((inhomogeneousCochains X.2).X 0) : Type u)) → (↑((inhomogeneousCochains X.X₃).X 0) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₀ X.X₂).inv :
              (a : (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u)) → (↑((inhomogeneousCochains X.X₂).X 0) : Type u))
            y :
          (↑((inhomogeneousCochains X.X₂).X 0) : Type u)) :
      (↑((inhomogeneousCochains X.X₃).X 0) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (cochainsIso₀ X.X₃).inv :
          (a : (↑(ModuleCat.of k (↑X.X₃ : Type u)) : Type u)) → (↑((inhomogeneousCochains X.X₃).X 0) : Type u))
        (↑z : (↑X.X₃ : Type u)) :
      (↑((inhomogeneousCochains X.X₃).X 0) : Type u))
have h : ∀ (g : Fin 0 → G),
  Eq (α := (↑X.X₃ : Type u))
    ((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) 0) (Y :=
            (inhomogeneousCochains X.X₃).X 0) (HomologicalComplex.Hom.f (cochainsMap (MonoidHom.id G) X.g) 0) :
          (a : (↑((inhomogeneousCochains X.2).X 0) : Type u)) → (↑((inhomogeneousCochains X.X₃).X 0) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (cochainsIso₀ X.X₂).inv :
              (a : (↑(ModuleCat.of k (↑X.X₂ : Type u)) : Type u)) → (↑((inhomogeneousCochains X.X₂).X 0) : Type u))
            y :
          (↑((inhomogeneousCochains X.X₂).X 0) : Type u))
        g :
      (↑X.X₃ : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (cochainsIso₀ X.X₃).inv :
          (a : (↑(ModuleCat.of k (↑X.X₃ : Type u)) : Type u)) → (↑((inhomogeneousCochains X.X₃).X 0) : Type u))
        (↑z : (↑X.X₃ : Type u)) g :
      (↑X.X₃ : Type u))
Tactic: ext