-- 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
z : ↥(cocycles₁ X.X₃)
y : G → (↑X.X₂ : Type u)
hy :
  Eq (α := G → (↑X.X₃ : Type u)) ((⇑(Rep.Hom.hom X.g) : (a : (↑X.X₂ : Type u)) → (↑X.X₃ : Type u)) ∘ y)
    (⇑z : (a : G) → (↑X.X₃ : Type u))
x : G × G → (↑X.X₁ : Type u)
hx :
  Eq (α := G × 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 (G → (↑X.X₂ : Type u))) : Type u)) →
          (↑(ModuleCat.of k (G × G → (↑X.X₂ : Type u))) : Type u))
      y)
h :
  ∀ (g : Fin 1 → 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) 1) (Y :=
              (inhomogeneousCochains X.X₃).X 1) (HomologicalComplex.Hom.f (cochainsMap (MonoidHom.id G) X.g) 1) :
            (a : (↑((inhomogeneousCochains X.2).X 1) : Type u)) → (↑((inhomogeneousCochains X.X₃).X 1) : 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 (G → (↑X.X₂ : Type u))) : Type u)) →
                  (↑((inhomogeneousCochains X.X₂).X 1) : Type u))
              y :
            (↑((inhomogeneousCochains X.X₂).X 1) : 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 (G → (↑X.X₃ : Type u))) : Type u)) → (↑((inhomogeneousCochains X.X₃).X 1) : Type u))
          (⇑z : (a : G) → (↑X.X₃ : Type u)) g :
        (↑X.X₃ : Type u))
⊢ Eq (α := (↑((inhomogeneousCochains X.X₃).X 1) : 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) 1) (Y :=
            (inhomogeneousCochains X.X₃).X 1) (HomologicalComplex.Hom.f (cochainsMap (MonoidHom.id G) X.g) 1) :
          (a : (↑((inhomogeneousCochains X.2).X 1) : Type u)) → (↑((inhomogeneousCochains X.X₃).X 1) : 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 (G → (↑X.X₂ : Type u))) : Type u)) →
                (↑((inhomogeneousCochains X.X₂).X 1) : Type u))
            y :
          (↑((inhomogeneousCochains X.X₂).X 1) : Type u)) :
      (↑((inhomogeneousCochains X.X₃).X 1) : 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 (G → (↑X.X₃ : Type u))) : Type u)) → (↑((inhomogeneousCochains X.X₃).X 1) : Type u))
        (⇑z : (a : G) → (↑X.X₃ : Type u)) :
      (↑((inhomogeneousCochains X.X₃).X 1) : Type u))

Tactic:
ext