-- 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 × G → (↑A : Type u_1)
g : 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.1, g.2.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.1, g.2.2)) :
              (↑A : Type u_1)) -
          (x (g.1 * g.2.1, g.2.2) + y (g.1 * g.2.1, g.2.2)) +
        (x (g.1, g.2.1 * g.2.2) + y (g.1, g.2.1 * g.2.2)) -
      (x (g.1, g.2.1) + y (g.1, g.2.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.1, g.2.2)) :
              (↑A : Type u_1))
            (x (g.1 * g.2.1, g.2.2)) +
          x (g.1, g.2.1 * g.2.2) -
        x (g.1, g.2.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.1, g.2.2)) :
              (↑A : Type u_1))
            (y (g.1 * g.2.1, g.2.2)) +
          y (g.1, g.2.1 * g.2.2) -
        y (g.1, g.2.1))
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.1, g.2.2)) :
              (↑A : Type u_1))
            (x (g.1 * g.2.1, g.2.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.1, g.2.2)) :
              (↑A : Type u_1))
            (y (g.1 * g.2.1, g.2.2)) +
        (x (g.1, g.2.1 * g.2.2) + y (g.1, g.2.1 * g.2.2)) -
      (x (g.1, g.2.1) + y (g.1, g.2.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.1, g.2.2)) :
              (↑A : Type u_1))
            (x (g.1 * g.2.1, g.2.2)) +
          x (g.1, g.2.1 * g.2.2) -
        x (g.1, g.2.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.1, g.2.2)) :
              (↑A : Type u_1))
            (y (g.1 * g.2.1, g.2.2)) +
          y (g.1, g.2.1 * g.2.2) -
        y (g.1, g.2.1))
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.1, g.2.2)) :
            (↑A : Type u_1))
          (x (g.1 * g.2.1, g.2.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.1, g.2.2)) :
            (↑A : Type u_1))
          (y (g.1 * g.2.1, g.2.2)) +
      (x (g.1, g.2.1 * g.2.2) + y (g.1, g.2.1 * g.2.2) - (x (g.1, g.2.1) + y (g.1, g.2.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.1, g.2.2)) :
              (↑A : Type u_1))
            (x (g.1 * g.2.1, g.2.2)) +
          x (g.1, g.2.1 * g.2.2) -
        x (g.1, g.2.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.1, g.2.2)) :
              (↑A : Type u_1))
            (y (g.1 * g.2.1, g.2.2)) +
          y (g.1, g.2.1 * g.2.2) -
        y (g.1, g.2.1))
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.1, g.2.2)) :
            (↑A : Type u_1))
          (x (g.1 * g.2.1, g.2.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.1, g.2.2)) :
            (↑A : Type u_1))
          (y (g.1 * g.2.1, g.2.2)) +
      (x (g.1, g.2.1 * g.2.2) - x (g.1, g.2.1) + (y (g.1, g.2.1 * g.2.2) - y (g.1, g.2.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.1, g.2.2)) :
              (↑A : Type u_1))
            (x (g.1 * g.2.1, g.2.2)) +
          x (g.1, g.2.1 * g.2.2) -
        x (g.1, g.2.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.1, g.2.2)) :
              (↑A : Type u_1))
            (y (g.1 * g.2.1, g.2.2)) +
          y (g.1, g.2.1 * g.2.2) -
        y (g.1, g.2.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.1, g.2.2) + y (g.2.1, g.2.2)) :
            (↑A : Type u_1))
          (x (g.1 * g.2.1, g.2.2) + y (g.1 * g.2.1, g.2.2)) +
        (x (g.1, g.2.1 * g.2.2) + y (g.1, g.2.1 * g.2.2)) -
      (x (g.1, g.2.1) + y (g.1, g.2.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.1, g.2.2)) :
              (↑A : Type u_1))
            (x (g.1 * g.2.1, g.2.2)) +
          x (g.1, g.2.1 * g.2.2) -
        x (g.1, g.2.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.1, g.2.2)) :
              (↑A : Type u_1))
            (y (g.1 * g.2.1, g.2.2)) +
          y (g.1, g.2.1 * g.2.2) -
        y (g.1, g.2.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.1, g.2.2)) :
          (↑A : Type u_1))
        (x (g.1 * g.2.1, g.2.2)) +
      (x (g.1, g.2.1 * g.2.2) - x (g.1, g.2.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.1, g.2.2)) :
          (↑A : Type u_1))
        (y (g.1 * g.2.1, g.2.2)) +
      (y (g.1, g.2.1 * g.2.2) - y (g.1, g.2.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.1, g.2.2)) :
            (↑A : Type u_1))
          (x (g.1 * g.2.1, g.2.2)) +
        x (g.1, g.2.1 * g.2.2) -
      x (g.1, g.2.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.1, g.2.2)) :
            (↑A : Type u_1))
          (y (g.1 * g.2.1, g.2.2)) +
        y (g.1, g.2.1 * g.2.2) -
      y (g.1, g.2.1))
Tactic: rw [map_add, add_sub_add_comm (A.ρ _ _), add_sub_assoc, add_sub_add_comm, add_add_add_comm,
          add_sub_assoc, add_sub_assoc]