-- 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.{u_1, u, u} k G
x y : G → (↑A : Type u_1)
g : G × G
rw :
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (x g.2) :
            (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (y g.2) :
            (↑A : Type u_1)) -
        (x (g.1 * g.2) + y (g.1 * g.2)) +
      (x g.1 + y g.1) =
    HSub.hSub (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (x g.2) :
            (↑A : Type u_1))
          (x (g.1 * g.2)) +
        x g.1 +
      (HSub.hSub (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (y g.2) :
            (↑A : Type u_1))
          (y (g.1 * g.2)) +
        y g.1)
rw₁ :
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (x g.2) :
            (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (y g.2) :
            (↑A : Type u_1)) -
        (x (g.1 * g.2) + y (g.1 * g.2)) +
      (x g.1 + y g.1) =
    HSub.hSub (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (x g.2) :
            (↑A : Type u_1))
          (x (g.1 * g.2)) +
        HSub.hSub (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (y g.2) :
            (↑A : Type u_1))
          (y (g.1 * g.2)) +
      (x g.1 + y g.1)
⊢ HSub.hSub (α := (↑A : Type u_1))
        ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
              (a : (↑A : Type u_1)) → (↑A : Type u_1))
            (x g.2 + y g.2) :
          (↑A : Type u_1))
        (x (g.1 * g.2) + y (g.1 * g.2)) +
      (x g.1 + y g.1) =
    HSub.hSub (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (x g.2) :
            (↑A : Type u_1))
          (x (g.1 * g.2)) +
        x g.1 +
      (HSub.hSub (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (y g.2) :
            (↑A : Type u_1))
          (y (g.1 * g.2)) +
        y g.1)
have rw₂ : HSub.hSub (α := (↑A : Type u_1))
        ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
              (a : (↑A : Type u_1)) → (↑A : Type u_1))
            (x g.2) :
          (↑A : Type u_1))
        (x (g.1 * g.2)) +
      HSub.hSub (α := (↑A : Type u_1))
        ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
              (a : (↑A : Type u_1)) → (↑A : Type u_1))
            (y g.2) :
          (↑A : Type u_1))
        (y (g.1 * g.2)) +
    (x g.1 + y g.1) =
  HSub.hSub (α := (↑A : Type u_1))
        ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
              (a : (↑A : Type u_1)) → (↑A : Type u_1))
            (x g.2) :
          (↑A : Type u_1))
        (x (g.1 * g.2)) +
      HSub.hSub (α := (↑A : Type u_1))
        ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g.1 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
              (a : (↑A : Type u_1)) → (↑A : Type u_1))
            (y g.2) :
          (↑A : Type u_1))
        (y (g.1 * g.2)) +
    (x g.1 + y g.1)
Tactic: rw [map_add, add_add_add_comm, add_sub_add_comm]