-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic (goal)
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)
⊢ (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))
have 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
Tactic: ext