awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
r : k
x : (↑A : Type (max u u_1))
g : G
dsimp :
  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)))
          (r • x) :
        (↑A : Type (max u u_1)))
      (r • x) =
    r •
      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
⊢ 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)))
          (r • x) :
        (↑A : Type (max u u_1)))
      (r • x) =
    HSMul.hSMul (α := k) (β := G → (↑A : Type (max u u_1))) ((RingHom.id k : (a : k) → k) r : k)
      (fun (g : G) ↦
        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)
      g

Tactic:
dsimp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
r : k
x : (↑A : Type (max u u_1))
g : G
rw :
  HSMul.hSMul (β := (↑A : Type (max u u_1))) r
        ((((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))) -
      r • x =
    r •
      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
rw₁ rw₂ :
  HSMul.hSMul (β := (↑A : Type (max u u_1))) r
        ((((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))) -
      r • x =
    HSMul.hSMul (β := (↑A : Type (max u u_1))) r
        ((((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))) -
      r • x
⊢ 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)))
          (r • x) :
        (↑A : Type (max u u_1)))
      (r • x) =
    r •
      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

Tactic:
rw [map_smul, smul_sub]

Premises used: smul_sub, map_smul
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
h :
  ∀ (x : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))),
    x ∈ (ModuleCat.Hom.hom (d₀₁.{u, u_1} A)).ker ↔ x ∈ A.ρ.invariants
⊢ (ModuleCat.Hom.hom (d₀₁.{u, u_1} A)).ker = A.ρ.invariants

Tactic:
ext x
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))
h :
  (∀ (x_1 : G),
      Eq (α := (↑A : Type (max u u_1)))
        ((ModuleCat.Hom.hom (d₀₁.{u, u_1} A) : (a : (↑A : Type (max u u_1))) → G → (↑A : Type (max u u_1))) x x_1 :
          (↑A : Type (max u u_1)))
        (0 x_1 : (↑A : Type (max u u_1)))) ↔
    ∀ (g : G),
      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
⊢ x ∈ (ModuleCat.Hom.hom (d₀₁.{u, u_1} A)).ker ↔ x ∈ A.ρ.invariants

Tactic:
simp only [LinearMap.mem_ker, mem_invariants, ← @sub_eq_zero _ _ _ x, funext_iff]

Premises used: sub_eq_zero, funext_iff, Representation.mem_invariants, LinearMap.mem_ker
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))
⊢ (∀ (x_1 : G),
      Eq (α := (↑A : Type (max u u_1)))
        ((ModuleCat.Hom.hom (d₀₁.{u, u_1} A) : (a : (↑A : Type (max u u_1))) → G → (↑A : Type (max u u_1))) x x_1 :
          (↑A : Type (max u u_1)))
        (0 x_1 : (↑A : Type (max u u_1)))) ↔
    ∀ (g : G),
      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:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
hf :
  ∀ (x : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))) (x_1 : G),
    Eq (α := (↑A : Type (max u u_1)))
      ((ModuleCat.Hom.hom (d₀₁.{u, u_1} A) :
            (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))) →
              (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
          x x_1 :
        (↑A : Type (max u u_1)))
      ((ModuleCat.Hom.hom 0 :
            (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))) →
              (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
          x x_1 :
        (↑A : Type (max u u_1)))
⊢ d₀₁.{u, u_1} A = 0

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
x : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))
x_1 : G
hf :
  Eq (α := (↑A : Type (max u u_1))) (0 : (↑A : Type (max u u_1)))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
        x x_1 :
      (↑A : Type (max u u_1)))
⊢ Eq (α := (↑A : Type (max u u_1)))
    ((ModuleCat.Hom.hom (d₀₁.{u, u_1} A) :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
        x x_1 :
      (↑A : Type (max u u_1)))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
        x x_1 :
      (↑A : Type (max u u_1)))

Tactic:
rw [d₀₁_hom_apply, isTrivial_apply, sub_self]

Premises used: groupCohomology.d₀₁_hom_apply, sub_self, Representation.isTrivial_apply
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
x : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))
x_1 : G
⊢ Eq (α := (↑A : Type (max u u_1))) (0 : (↑A : Type (max u u_1)))
    ((ModuleCat.Hom.hom 0 :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
        x x_1 :
      (↑A : Type (max u u_1)))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
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)))
⊢ ModuleCat.ofHom A.ρ.invariants.subtype ≫ d₀₁.{u, u_1} A = 0

Tactic:
ext ⟨x, hx⟩ g
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
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
⊢ (((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
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
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
⊢ 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

Premises used: sub_eq_zero
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
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 :
  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
⊢ 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)))

Tactic:
hx
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
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 :
  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
⊢ 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)))

Tactic:
exact hx
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
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
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)
⊢ (((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

Tactic:
dsimp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
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
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)
⊢ (((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

Tactic:
dsimp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
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
rw₂ 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
⊢ 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:
rw [map_smul, smul_add, smul_sub]

Premises used: smul_sub, smul_add, map_smul
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
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
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))
⊢ (((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

Tactic:
dsimp