-- 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 : ↥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)
h :
  ∀ (g : Fin (HAdd.hAdd (α := ℕ) 0 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 → (↑X.X₁ : Type u))) : Type u)) →
                (↑((inhomogeneousCochains X.X₁).X 1) : 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 0) (Y :=
              (inhomogeneousCochains X.X₂).X (HAdd.hAdd (α := ℕ) 0 1))
              ((inhomogeneousCochains X.X₂).d 0 (HAdd.hAdd (α := ℕ) 0 1)) :
            (a : (↑((inhomogeneousCochains X.X₂).X 0) : Type u)) → (↑((inhomogeneousCochains X.X₂).X (0 + 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 (↑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))
⊢ Eq (α := (Fin (HAdd.hAdd (α := ℕ) 0 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 → (↑X.X₁ : Type u))) : Type u)) → (↑((inhomogeneousCochains X.X₁).X 1) : 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 0) (Y :=
          (inhomogeneousCochains X.X₂).X (HAdd.hAdd (α := ℕ) 0 1))
          ((inhomogeneousCochains X.X₂).d 0 (HAdd.hAdd (α := ℕ) 0 1)) :
        (a : (↑((inhomogeneousCochains X.X₂).X 0) : Type u)) → (↑((inhomogeneousCochains X.X₂).X (0 + 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 (↑X.X₂ : Type u)) : Type u)) → (↑((inhomogeneousCochains X.X₂).X 0) : Type u))
          y :
        (↑((inhomogeneousCochains X.X₂).X 0) : Type u)))

Tactic:
ext g

Premises used: CategoryTheory.ShortComplex.g