-- 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
f : G × G → (↑A : Type u_1)
simp_rw :
  (∀ (g h j : G),
      HSub.hSub (α := (↑A : Type u_1))
              ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                    (a : (↑A : Type u_1)) → (↑A : Type u_1))
                  (f (h, j)) :
                (↑A : Type u_1))
              (f (g * h, j)) +
            f (g, h * j) -
          f (g, h) =
        0) ↔
    ∀ (g h j : G),
      f (g * h, j) + f (g, h) =
        HAdd.hAdd (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (f (h, j)) :
            (↑A : Type u_1))
          (f (g, h * j))
simp_rw₁ :
  (∀ (g h j : G),
      HSub.hSub (α := (↑A : Type u_1))
            ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                  (a : (↑A : Type u_1)) → (↑A : Type u_1))
                (f (h, j)) :
              (↑A : Type u_1))
            (f (g * h, j)) +
          f (g, h * j) =
        f (g, h)) ↔
    ∀ (g h j : G),
      f (g * h, j) + f (g, h) =
        HAdd.hAdd (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (f (h, j)) :
            (↑A : Type u_1))
          (f (g, h * j))
simp_rw₂ :
  (∀ (g h j : G),
      HAdd.hAdd (α := (↑A : Type u_1))
            ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                  (a : (↑A : Type u_1)) → (↑A : Type u_1))
                (f (h, j)) :
              (↑A : Type u_1))
            (f (g, h * j)) -
          f (g * h, j) =
        f (g, h)) ↔
    ∀ (g h j : G),
      f (g * h, j) + f (g, h) =
        HAdd.hAdd (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (f (h, j)) :
            (↑A : Type u_1))
          (f (g, h * j))
⊢ f ∈ cocycles₂ A ↔
    ∀ (g h j : G),
      f (g * h, j) + f (g, h) =
        HAdd.hAdd (α := (↑A : Type u_1))
          ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                (a : (↑A : Type u_1)) → (↑A : Type u_1))
              (f (h, j)) :
            (↑A : Type u_1))
          (f (g, h * j))
have simp_rw₃ : (∀ (g h j : G),
    HAdd.hAdd (α := (↑A : Type u_1))
        ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
              (a : (↑A : Type u_1)) → (↑A : Type u_1))
            (f (h, j)) :
          (↑A : Type u_1))
        (f (g, h * j)) =
      f (g, h) + f (g * h, j)) ↔
  ∀ (g h j : G),
    f (g * h, j) + f (g, h) =
      HAdd.hAdd (α := (↑A : Type u_1))
        ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
              (a : (↑A : Type u_1)) → (↑A : Type u_1))
            (f (h, j)) :
          (↑A : Type u_1))
        (f (g, h * j))
Tactic: simp_rw [mem_cocycles₂_def, sub_eq_zero, sub_add_eq_add_sub, sub_eq_iff_eq_add, eq_comm,
    add_comm (f (_ * _, _))]