-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑((inhomogeneousCochains A).X 1) : Type u)
y : G × G
⊢ HSub.hSub (α := (↑A : Type u))
        ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) y.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            (x ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) y.2)) :
          (↑A : Type u))
        (x ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) (y.1 * y.2))) +
      x ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) y.1) =
    HAdd.hAdd (α := (↑A : Type u)) (β := (↑A : Type u))
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u))
                (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
                    (a : G × G) → (i : Fin 2) → G)
                  y 0) :
              (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          (x fun (i : Fin 1) ↦
            ((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
                (a : G × G) → (i : Fin 2) → G)
              y i.succ) :
        (↑A : Type u))
      (∑ j : Fin (1 + 1),
          HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1) •
            x
              (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2)
                (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
                    (a : G × G) → (i : Fin 2) → G)
                  y)) :
        (↑A : Type u))
have hf : HSub.hSub (α := (↑A : Type u))
      ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) y.1 : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          (x ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) y.2)) :
        (↑A : Type u))
      (x ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) (y.1 * y.2))) +
    x ((Equiv.symm (Equiv.funUnique (Fin 1) G) : (a : G) → Fin 1 → G) y.1) =
  HAdd.hAdd (α := (↑A : Type u))
    ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u))
              (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
                  (a : G × G) → (i : Fin 2) → G)
                y 0) :
            (↑A : Type u) →ₗ[k] (↑A : Type u)) :
          (a : (↑A : Type u)) → (↑A : Type u))
        (x fun (i : Fin 1) ↦
          ((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) : (a : G × G) → (i : Fin 2) → G)
            y i.succ) :
      (↑A : Type u))
    (HPow.hPow (α := k) (-1) ((↑0 : ℕ) + 1) •
        x
          (Fin.contractNth 0 (fun (x1 x2 : G) ↦ x1 * x2)
            (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
                (a : G × G) → (i : Fin 2) → G)
              y)) +
      HPow.hPow (α := k) (-1) ((↑1 : ℕ) + 1) •
        x
          (Fin.contractNth 1 (fun (x1 x2 : G) ↦ x1 * x2)
            (((Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ G) : G × G ≃ ((i : Fin 2) → G)) :
                (a : G × G) → (i : Fin 2) → G)
              y)))
Tactic: rw [Fin.sum_univ_two]