-- 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 (HAdd.hAdd (α := ℕ) 1 1) → G),
    Eq (α := (↑X.X₂ : Type u))
      (Function.comp (β := (↑X.X₁ : Type u)) (⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑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 × G → (↑X.X₁ : Type u))) : Type u)) →
                (↑((inhomogeneousCochains X.X₁).X 2) : Type u))
            x)
          g :
        (↑X.X₂ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X := (inhomogeneousCochains X.X₂).X 1) (Y :=
              (inhomogeneousCochains X.X₂).X (HAdd.hAdd (α := ℕ) 1 1))
              ((inhomogeneousCochains X.X₂).d 1 (HAdd.hAdd (α := ℕ) 1 1)) :
            (a : (↑((inhomogeneousCochains X.X₂).X 1) : Type u)) → (↑((inhomogeneousCochains X.X₂).X (1 + 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))
⊢ Eq (α := (Fin (HAdd.hAdd (α := ℕ) 1 1) → G) → (↑X.X₂ : Type u))
    (Function.comp (β := (↑X.X₁ : Type u)) (⇑(Rep.Hom.hom X.f) : (a : (↑X.X₁ : Type u)) → (↑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 × G → (↑X.X₁ : Type u))) : Type u)) →
            (↑((inhomogeneousCochains X.X₁).X 2) : Type u))
        x))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := (inhomogeneousCochains X.X₂).X 1) (Y :=
          (inhomogeneousCochains X.X₂).X (HAdd.hAdd (α := ℕ) 1 1))
          ((inhomogeneousCochains X.X₂).d 1 (HAdd.hAdd (α := ℕ) 1 1)) :
        (a : (↑((inhomogeneousCochains X.X₂).X 1) : Type u)) → (↑((inhomogeneousCochains X.X₂).X (1 + 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)))

Tactic:
ext g

Premises used: CategoryTheory.ShortComplex.g