awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 → (↑A : Type u_1)
simp_rw :
  (∀ (g h : 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) :
              (↑A : Type u_1))
            (f (g * h)) +
          f g =
        0) ↔
    ∀ (g h : G),
      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) :
            (↑A : Type u_1))
          (f g)
⊢ f ∈ cocycles₁ A ↔
    ∀ (g h : G),
      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) :
            (↑A : Type u_1))
          (f g)
have simp_rw₁ : (∀ (g h : 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) :
            (↑A : Type u_1))
          (f g) -
        f (g * h) =
      0) ↔
  ∀ (g h : G),
    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) :
          (↑A : Type u_1))
        (f g)
Tactic: simp_rw [mem_cocycles₁_def, sub_add_eq_add_sub, sub_eq_zero, eq_comm]
-- 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 → (↑A : Type u_1)
simp_rw :
  (∀ (g h : 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) :
              (↑A : Type u_1))
            (f (g * h)) +
          f g =
        0) ↔
    ∀ (g h : G),
      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) :
            (↑A : Type u_1))
          (f g)
simp_rw₁ :
  (∀ (g h : 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) :
              (↑A : Type u_1))
            (f g) -
          f (g * h) =
        0) ↔
    ∀ (g h : G),
      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) :
            (↑A : Type u_1))
          (f g)
⊢ f ∈ cocycles₁ A ↔
    ∀ (g h : G),
      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) :
            (↑A : Type u_1))
          (f g)
have simp_rw₂ : (∀ (g h : 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) :
          (↑A : Type u_1))
        (f g) =
      f (g * h)) ↔
  ∀ (g h : G),
    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) :
          (↑A : Type u_1))
        (f g)
Tactic: simp_rw [mem_cocycles₁_def, sub_add_eq_add_sub, sub_eq_zero, eq_comm]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : ↥(cocycles₁ A)
⊢ Eq.{u_1 + 1} (α := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) 1) 0
have this : HSub.hSub (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      (((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) 1 : (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G) → (↑A : Type u_1)) 1) :
        (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) (HMul.hMul (α := G) 1 1) : (↑A : Type u_1)) +
    (f : (a : G) → (↑A : Type u_1)) 1 =
  0
Tactic: have := (mem_cocycles₁_def f).1 f.2 1 1
-- 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 : ↥(cocycles₁ A)
g : G
⊢ Eq.{u_1 + 1} (α := (↑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 : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
      (↑A : Type u_1))
    (-(f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
have rw : HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑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 : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
      (↑A : Type u_1))
    ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
  0
Tactic: rw [← add_eq_zero_iff_eq_neg, ← cocycles₁_map_one f, ← mul_inv_cancel g,
    (mem_cocycles₁_iff f).1 f.2 g g⁻¹]
-- 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 : ↥(cocycles₁ A)
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 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
    0
⊢ Eq.{u_1 + 1} (α := (↑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 : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
      (↑A : Type u_1))
    (-(f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
have rw₁ : HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑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 : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
      (↑A : Type u_1))
    ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
  (f : (a : G) → (↑A : Type u_1)) 1
Tactic: rw [← add_eq_zero_iff_eq_neg, ← cocycles₁_map_one f, ← mul_inv_cancel g,
    (mem_cocycles₁_iff f).1 f.2 g g⁻¹]
-- 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 : ↥(cocycles₁ A)
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 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
    0
rw₁ :
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑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 : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
    (f : (a : G) → (↑A : Type u_1)) 1
⊢ Eq.{u_1 + 1} (α := (↑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 : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
      (↑A : Type u_1))
    (-(f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
have rw₂ : HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑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 : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
      (↑A : Type u_1))
    ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
  (f : (a : G) → (↑A : Type u_1)) (g * g⁻¹)
Tactic: rw [← add_eq_zero_iff_eq_neg, ← cocycles₁_map_one f, ← mul_inv_cancel g,
    (mem_cocycles₁_iff f).1 f.2 g g⁻¹]
-- 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 : ↥(cocycles₁ A)
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 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
    0
rw₁ :
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑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 : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
    (f : (a : G) → (↑A : Type u_1)) 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 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
    (f : (a : G) → (↑A : Type u_1)) (g * g⁻¹)
⊢ Eq.{u_1 + 1} (α := (↑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 : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
      (↑A : Type u_1))
    (-(f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
have rw₃ : HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑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 : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
      (↑A : Type u_1))
    ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑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 : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
      (↑A : Type u_1))
    ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
Tactic: rw [← add_eq_zero_iff_eq_neg, ← cocycles₁_map_one f, ← mul_inv_cancel g,
    (mem_cocycles₁_iff f).1 f.2 g g⁻¹]
-- 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
inst_2 : A.IsTrivial
f : ↥(cocycles₁ A)
g h : G
⊢ (f : (a : G) → (↑A : Type u_1)) (g * h) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1))
have rw : HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑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 : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1)) :
      (↑A : Type u_1))
    ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
    ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1))
Tactic: rw [(mem_cocycles₁_iff f).1 f.2, isTrivial_apply A.ρ g (f h), add_comm]
-- 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
inst_2 : A.IsTrivial
f : ↥(cocycles₁ A)
g h : 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 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1))
⊢ (f : (a : G) → (↑A : Type u_1)) (g * h) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1))
have rw₁ : HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1))
    ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
    ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1))
Tactic: rw [(mem_cocycles₁_iff f).1 f.2, isTrivial_apply A.ρ g (f h), add_comm]
-- 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
inst_2 : A.IsTrivial
f : ↥(cocycles₁ A)
g h : 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 : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1))
rw₁ :
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1))
⊢ (f : (a : G) → (↑A : Type u_1)) (g * h) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1))
have rw₂ : HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
    ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1)) =
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
    ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1))
Tactic: rw [(mem_cocycles₁_iff f).1 f.2, isTrivial_apply A.ρ g (f h), add_comm]
-- 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)
⊢ Eq (α := (↑(ModuleCat.of k (G × G × G → (↑A : Type u_1))) : Type (max u u_1)))
      ((ModuleCat.Hom.hom (d₂₃ A) :
            (a : G × G → (↑A : Type u_1)) → (↑(ModuleCat.of k (G × G × G → (↑A : Type u_1))) : Type (max u u_1)))
          f :
        (↑(ModuleCat.of k (G × G × G → (↑A : Type u_1))) : Type (max u u_1)))
      (0 : (↑(ModuleCat.of k (G × G × G → (↑A : Type u_1))) : Type (max u u_1))) ↔
    ∀ (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
have simp_rw : (∀ (a a_1 b : G),
    HSub.hSub (α := (↑A : Type u_1))
            ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) a : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                  (a : (↑A : Type u_1)) → (↑A : Type u_1))
                (f (a_1, b)) :
              (↑A : Type u_1))
            (f (a * a_1, b)) +
          f (a, a_1 * b) -
        f (a, a_1) =
      0 (a, a_1, b)) ↔
  ∀ (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
Tactic: simp_rw [funext_iff, d₂₃_hom_apply, Prod.forall]
-- 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)
⊢ 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),
    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))
Tactic: simp_rw [mem_cocycles₂_def, sub_eq_zero, sub_add_eq_add_sub, sub_eq_iff_eq_add, eq_comm,
    add_comm (f (_ * _, _))]
-- 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))
⊢ 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),
    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))
Tactic: simp_rw [mem_cocycles₂_def, sub_eq_zero, sub_add_eq_add_sub, sub_eq_iff_eq_add, eq_comm,
    add_comm (f (_ * _, _))]