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 k G
⊢ ModuleCat.ofHom A.ρ.invariants.subtype ≫ d₀₁.{u, u_1} A = 0
have hf : ∀ (x : (↑A : Type (max u u_1))) (hx : x ∈ A.ρ.invariants) (g : G),
  Eq (α := (↑A : Type (max u u_1)))
    ((ModuleCat.Hom.hom (ModuleCat.ofHom A.ρ.invariants.subtype ≫ d₀₁.{u, u_1} A) :
          (a : (↑(ModuleCat.of k ↥A.ρ.invariants) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
        (Subtype.mk (p := fun (x : (↑A : Type (max u u_1))) ↦ x ∈ A.ρ.invariants) x hx) g :
      (↑A : Type (max u u_1)))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k ↥A.ρ.invariants) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
        (Subtype.mk (p := fun (x : (↑A : Type (max u u_1))) ↦ x ∈ A.ρ.invariants) x hx) g :
      (↑A : Type (max u u_1)))
Tactic: ext ⟨x, hx⟩ g
-- 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 k G
x : (↑A : Type (max u u_1))
hx : x ∈ A.ρ.invariants
g : G
⊢ Eq (α := (↑A : Type (max u u_1)))
    ((ModuleCat.Hom.hom (ModuleCat.ofHom A.ρ.invariants.subtype ≫ d₀₁.{u, u_1} A) :
          (a : (↑(ModuleCat.of k ↥A.ρ.invariants) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
        (Subtype.mk (p := fun (x : (↑A : Type (max u u_1))) ↦ x ∈ A.ρ.invariants) x hx) g :
      (↑A : Type (max u u_1)))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k ↥A.ρ.invariants) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
        (Subtype.mk (p := fun (x : (↑A : Type (max u u_1))) ↦ x ∈ A.ρ.invariants) x hx) g :
      (↑A : Type (max u u_1)))
have hx₁ : (((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
        (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
      (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
    x =
  x
Tactic: replace hx := hx g
-- 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 k G
x : (↑A : Type (max u u_1))
hx_1 : x ∈ A.ρ.invariants
g : G
hx :
  (((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
          (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
        (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
      x =
    x
⊢ Eq (α := (↑A : Type (max u u_1)))
    ((ModuleCat.Hom.hom (ModuleCat.ofHom A.ρ.invariants.subtype ≫ d₀₁.{u, u_1} A) :
          (a : (↑(ModuleCat.of k ↥A.ρ.invariants) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
        (Subtype.mk (p := fun (x : (↑A : Type (max u u_1))) ↦ x ∈ A.ρ.invariants) x hx_1) g :
      (↑A : Type (max u u_1)))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k ↥A.ρ.invariants) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
        (Subtype.mk (p := fun (x : (↑A : Type (max u u_1))) ↦ x ∈ A.ρ.invariants) x hx_1) g :
      (↑A : Type (max u u_1)))
have hx₁ : HSub.hSub (α := (↑A : Type (max u u_1)))
    ((((A.ρ : (a : G) → (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) g :
            (↑A : Type (max u u_1)) →ₗ[k] (↑A : Type (max u u_1))) :
          (a : (↑A : Type (max u u_1))) → (↑A : Type (max u u_1)))
        x :
      (↑A : Type (max u u_1)))
    x =
  0
Tactic: rw [← sub_eq_zero] at hx
Cleared hypotheses: hx
-- 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
⊢ (((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 + y) g.2) -
        (x + y) (g.1 * g.2) +
      (x + y) g.1 =
    HAdd.hAdd (α := G × G → (↑A : Type u_1)) (β := G × G → (↑A : Type u_1))
      (fun (g : G × G) ↦
        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)
      (fun (g : G × G) ↦
        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)
      g
have dsimp : 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)
Tactic: dsimp
-- 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
⊢ 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 : 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)
Tactic: rw [map_add, add_add_add_comm, add_sub_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
r : k
x : G → (↑A : Type u_1)
g : G × G
⊢ (((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))
          ((r • x) g.2) -
        (r • x) (g.1 * g.2) +
      (r • x) g.1 =
    HSMul.hSMul (α := k) (β := G × G → (↑A : Type u_1)) ((RingHom.id k : (a : k) → k) r : k)
      (fun (g : G × G) ↦
        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)
      g
have dsimp : 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))
          (r • x g.2) :
        (↑A : Type u_1))
      (r • x (g.1 * g.2)) +
    r • x g.1 =
  r •
    (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)
Tactic: dsimp
-- 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
r : k
x : G → (↑A : Type u_1)
g : G × G
⊢ 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))
            (r • x g.2) :
          (↑A : Type u_1))
        (r • x (g.1 * g.2)) +
      r • x g.1 =
    r •
      (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)
have rw : HSMul.hSMul (β := (↑A : Type u_1)) r
        ((((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)) -
      r • x (g.1 * g.2) +
    r • x g.1 =
  r •
    (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)
Tactic: rw [map_smul, smul_add, smul_sub]
-- 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
r : k
x : G → (↑A : Type u_1)
g : G × G
rw :
  HSMul.hSMul (β := (↑A : Type u_1)) r
          ((((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)) -
        r • x (g.1 * g.2) +
      r • x g.1 =
    r •
      (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))
            (r • x g.2) :
          (↑A : Type u_1))
        (r • x (g.1 * g.2)) +
      r • x g.1 =
    r •
      (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)
have rw₁ : HSMul.hSMul (β := (↑A : Type u_1)) r
        ((((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)) -
      r • x (g.1 * g.2) +
    r • x g.1 =
  r •
      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)) +
    r • x g.1
Tactic: rw [map_smul, smul_add, smul_sub]
-- 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
r : k
x : G → (↑A : Type u_1)
g : G × G
rw :
  HSMul.hSMul (β := (↑A : Type u_1)) r
          ((((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)) -
        r • x (g.1 * g.2) +
      r • x g.1 =
    r •
      (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)
rw₁ :
  HSMul.hSMul (β := (↑A : Type u_1)) r
          ((((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)) -
        r • x (g.1 * g.2) +
      r • x g.1 =
    r •
        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)) +
      r • 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))
            (r • x g.2) :
          (↑A : Type u_1))
        (r • x (g.1 * g.2)) +
      r • x g.1 =
    r •
      (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)
have rw₂ : HSMul.hSMul (β := (↑A : Type u_1)) r
        ((((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)) -
      r • x (g.1 * g.2) +
    r • x g.1 =
  HSMul.hSMul (β := (↑A : Type u_1)) r
        ((((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)) -
      r • x (g.1 * g.2) +
    r • x g.1
Tactic: rw [map_smul, smul_add, smul_sub]
-- 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
⊢ (((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 + y) (g.2.1, g.2.2)) -
          (x + y) (g.1 * g.2.1, g.2.2) +
        (x + y) (g.1, g.2.1 * g.2.2) -
      (x + y) (g.1, g.2.1) =
    HAdd.hAdd (α := G × G × G → (↑A : Type u_1)) (β := G × G × G → (↑A : Type u_1))
      (fun (g : G × G × G) ↦
        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))
      (fun (g : G × G × G) ↦
        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))
      g
have dsimp : 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))
Tactic: dsimp
-- 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
⊢ 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 : 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))
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]
-- 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
r : k
x : G × G → (↑A : Type u_1)
g : G × G × G
⊢ (((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))
            ((r • x) (g.2.1, g.2.2)) -
          (r • x) (g.1 * g.2.1, g.2.2) +
        (r • x) (g.1, g.2.1 * g.2.2) -
      (r • x) (g.1, g.2.1) =
    HSMul.hSMul (α := k) (β := G × G × G → (↑A : Type u_1)) ((RingHom.id k : (a : k) → k) r : k)
      (fun (g : G × G × G) ↦
        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))
      g
have dsimp : 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))
            (r • x (g.2.1, g.2.2)) :
          (↑A : Type u_1))
        (r • x (g.1 * g.2.1, g.2.2)) +
      r • x (g.1, g.2.1 * g.2.2) -
    r • x (g.1, g.2.1) =
  r •
    (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))
Tactic: dsimp