-- 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.ρ : (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)))
have hf : HAdd.hAdd (α := (↑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))
    (-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)) +
      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: simp only [Fin.val_zero, zero_add, pow_one, neg_smul, one_smul, Fin.val_one,
    Nat.one_add, neg_one_sq, sub_eq_add_neg, add_assoc]