-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
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
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)))
⊢ 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))

Tactic:
rw [Fin.sum_univ_two]

Premises used: Fin.sum_univ_two