-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
Goal:
k G : Type u
inst : CommRing k
n_1 : ℕ
inst_1 : Monoid G
A : Rep.{u_1, u, u} k G
n : ℕ
f g : (Fin n → G) → (↑A : Type u_1)
h :
  ∀ (x : Fin (n + 1) → G),
    HAdd.hAdd (α := (↑A : Type u_1))
        ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) (x 0) : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f + g) fun (i : Fin n) ↦ x i.succ))
        (∑ j : Fin (n + 1),
          HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1) • (f + g) (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) x)) =
      HAdd.hAdd (α := (Fin (n + 1) → G) → (↑A : Type u_1)) (β := (Fin (n + 1) → G) → (↑A : Type u_1))
        (fun (g : Fin (n + 1) → G) ↦
          HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
            ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) (g 0) : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                  (a : (↑A : Type u_1)) → (↑A : Type u_1))
                (f fun (i : Fin n) ↦ g i.succ) :
              (↑A : Type u_1))
            (∑ j : Fin (n + 1),
                HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1) • f (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) :
              (↑A : Type u_1)))
        (fun (g_1 : Fin (n + 1) → G) ↦
          HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
            ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) (g_1 0) :
                    (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                  (a : (↑A : Type u_1)) → (↑A : Type u_1))
                (g fun (i : Fin n) ↦ g_1 i.succ) :
              (↑A : Type u_1))
            (∑ j : Fin (n + 1),
                HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1) • g (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g_1) :
              (↑A : Type u_1)))
        x
⊢ (fun (g_1 : Fin (n + 1) → G) ↦
      HAdd.hAdd (α := (↑A : Type u_1))
        ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) (g_1 0) : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f + g) fun (i : Fin n) ↦ g_1 i.succ))
        (∑ j : Fin (n + 1),
          HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1) • (f + g) (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g_1))) =
    HAdd.hAdd (α := (Fin (n + 1) → G) → (↑A : Type u_1))
      (fun (g : Fin (n + 1) → G) ↦
        HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) (g 0) : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (f fun (i : Fin n) ↦ g i.succ) :
            (↑A : Type u_1))
          (∑ j : Fin (n + 1), HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1) • f (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g) :
            (↑A : Type u_1)))
      fun (g_1 : Fin (n + 1) → G) ↦
      HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
        ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) (g_1 0) : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
              (a : (↑A : Type u_1)) → (↑A : Type u_1))
            (g fun (i : Fin n) ↦ g_1 i.succ) :
          (↑A : Type u_1))
        (∑ j : Fin (n + 1), HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1) • g (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) g_1) :
          (↑A : Type u_1))

Tactic:
ext