awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
a : G
x : (↑A : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom (d₁₀ A) ∘ₗ lsingle a : (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u)) x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    (((ModuleCat.Hom.hom 0 :
              (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u) →ₗ[k] (↑(ModuleCat.of k (↑A : Type u)) : Type u)) ∘ₗ
            lsingle a :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        x :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))

Tactic:
simp [d₁₀]

Premises used: groupHomology.d₁₀
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g : G × G
a : (↑A : Type u)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₂₁ A) :
        (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
      (single g a) =
    HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u))
        (single g.2
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g.1⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              a) :
          G →₀ (↑A : Type u))
        (single (g.1 * g.2) a) +
      single g.1 a

Tactic:
simp [d₂₁]

Premises used: groupHomology.d₂₁
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g : G
a : (↑A : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (d₂₁ A) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
        (single (1, g) a) :
      (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
    (single 1 a : G →₀ (↑A : Type u))

Tactic:
simp [d₂₁]

Premises used: groupHomology.d₂₁
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g : G
a : (↑A : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (d₂₁ A) :
          (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
        (single (g, 1) a) :
      (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
    (single 1
        ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
            (a : (↑A : Type u)) → (↑A : Type u))
          a) :
      G →₀ (↑A : Type u))

Tactic:
simp [d₂₁]

Premises used: groupHomology.d₂₁
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g : G
a : (↑A : Type u)
simp :
  HAdd.hAdd (β := G →₀ (↑A : Type u))
        (HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single g a)
          (single 1
              ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                a) :
            G →₀ (↑A : Type u)))
        (single g⁻¹
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              a) :
          G →₀ (↑A : Type u)) -
      (HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u))
          (single g⁻¹
              ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                a) :
            G →₀ (↑A : Type u))
          (single 1 a) +
        single g a) =
    HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single 1 a)
      (single 1
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a) :
        G →₀ (↑A : Type u))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₂₁ A) :
        (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
      (HSub.hSub (α := G × G →₀ (↑A : Type u)) (β := G × G →₀ (↑A : Type u))
        (single (g⁻¹, g)
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              a) :
          G × G →₀ (↑A : Type u))
        (single (g, g⁻¹) a)) =
    HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single 1 a)
      (single 1
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a) :
        G →₀ (↑A : Type u))

Tactic:
simp only [map_sub, d₂₁_single (G := G), inv_inv, self_inv_apply, inv_mul_cancel,
    mul_inv_cancel]

Premises used: inv_mul_cancel, map_sub, inv_inv, Representation.self_inv_apply, mul_inv_cancel, groupHomology.d₂₁_single
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g : G
a : (↑A : Type u)
⊢ HAdd.hAdd (β := G →₀ (↑A : Type u))
        (HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single g a)
          (single 1
              ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                a) :
            G →₀ (↑A : Type u)))
        (single g⁻¹
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              a) :
          G →₀ (↑A : Type u)) -
      (HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u))
          (single g⁻¹
              ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                a) :
            G →₀ (↑A : Type u))
          (single 1 a) +
        single g a) =
    HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single 1 a)
      (single 1
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a) :
        G →₀ (↑A : Type u))

Tactic:
abel
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g : G
a : (↑A : Type u)
simp :
  HAdd.hAdd (β := G →₀ (↑A : Type u))
        (HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single g⁻¹ a)
          (single 1
              ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                a) :
            G →₀ (↑A : Type u)))
        (single g
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              a) :
          G →₀ (↑A : Type u)) -
      (HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u))
          (single g
              ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                a) :
            G →₀ (↑A : Type u))
          (single 1 a) +
        single g⁻¹ a) =
    HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single 1 a)
      (single 1
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a) :
        G →₀ (↑A : Type u))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₂₁ A) :
        (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
      (HSub.hSub (α := G × G →₀ (↑A : Type u)) (β := G × G →₀ (↑A : Type u))
        (single (g, g⁻¹)
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              a) :
          G × G →₀ (↑A : Type u))
        (single (g⁻¹, g) a)) =
    HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single 1 a)
      (single 1
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a) :
        G →₀ (↑A : Type u))

Tactic:
simp only [map_sub, d₂₁_single (G := G), inv_self_apply, mul_inv_cancel, inv_inv,
    inv_mul_cancel]

Premises used: inv_mul_cancel, map_sub, inv_inv, mul_inv_cancel, groupHomology.d₂₁_single, Representation.inv_self_apply
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g : G
a : (↑A : Type u)
⊢ HAdd.hAdd (β := G →₀ (↑A : Type u))
        (HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single g⁻¹ a)
          (single 1
              ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                a) :
            G →₀ (↑A : Type u)))
        (single g
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              a) :
          G →₀ (↑A : Type u)) -
      (HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u))
          (single g
              ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                a) :
            G →₀ (↑A : Type u))
          (single 1 a) +
        single g⁻¹ a) =
    HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single 1 a)
      (single 1
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a) :
        G →₀ (↑A : Type u))

Tactic:
abel
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g h : G
a : (↑A : Type u)
simp :
  HAdd.hAdd (β := G →₀ (↑A : Type u))
        (HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single h a)
          (single (g * h)
              ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                a) :
            G →₀ (↑A : Type u)))
        (single g
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              a) :
          G →₀ (↑A : Type u)) +
      (HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u))
          (single (g * h)
              ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                a) :
            G →₀ (↑A : Type u))
          (single h a) +
        single g⁻¹ a) =
    HAdd.hAdd (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u))
      (single g
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a) :
        G →₀ (↑A : Type u))
      (single g⁻¹ a)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₂₁ A) :
        (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
      (HAdd.hAdd (α := G × G →₀ (↑A : Type u)) (β := G × G →₀ (↑A : Type u))
        (single (g, h)
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              a) :
          G × G →₀ (↑A : Type u))
        (single (g⁻¹, g * h) a)) =
    HAdd.hAdd (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u))
      (single g
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a) :
        G →₀ (↑A : Type u))
      (single g⁻¹ a)

Tactic:
simp only [map_add, d₂₁_single (G := G), inv_self_apply, inv_inv, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left, map_add, inv_inv, groupHomology.d₂₁_single, Representation.inv_self_apply
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g h : G
a : (↑A : Type u)
⊢ HAdd.hAdd (β := G →₀ (↑A : Type u))
        (HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single h a)
          (single (g * h)
              ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                a) :
            G →₀ (↑A : Type u)))
        (single g
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              a) :
          G →₀ (↑A : Type u)) +
      (HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u))
          (single (g * h)
              ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                a) :
            G →₀ (↑A : Type u))
          (single h a) +
        single g⁻¹ a) =
    HAdd.hAdd (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u))
      (single g
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a) :
        G →₀ (↑A : Type u))
      (single g⁻¹ a)

Tactic:
abel
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g h : G
a : (↑A : Type u)
simp :
  HAdd.hAdd (β := G →₀ (↑A : Type u))
        (HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single (g * h) a)
          (single h
              ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                a) :
            G →₀ (↑A : Type u)))
        (single g⁻¹
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              a) :
          G →₀ (↑A : Type u)) +
      (HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u))
          (single h
              ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                a) :
            G →₀ (↑A : Type u))
          (single (g * h) a) +
        single g a) =
    HAdd.hAdd (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u))
      (single g⁻¹
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a) :
        G →₀ (↑A : Type u))
      (single g a)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₂₁ A) :
        (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
      (HAdd.hAdd (α := G × G →₀ (↑A : Type u)) (β := G × G →₀ (↑A : Type u))
        (single (g⁻¹, g * h)
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              a) :
          G × G →₀ (↑A : Type u))
        (single (g, h) a)) =
    HAdd.hAdd (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u))
      (single g⁻¹
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a) :
        G →₀ (↑A : Type u))
      (single g a)

Tactic:
simp only [map_add, d₂₁_single (G := G), inv_inv, self_inv_apply, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left, map_add, inv_inv, Representation.self_inv_apply, groupHomology.d₂₁_single
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g h : G
a : (↑A : Type u)
⊢ HAdd.hAdd (β := G →₀ (↑A : Type u))
        (HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single (g * h) a)
          (single h
              ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                a) :
            G →₀ (↑A : Type u)))
        (single g⁻¹
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                (a : (↑A : Type u)) → (↑A : Type u))
              a) :
          G →₀ (↑A : Type u)) +
      (HSub.hSub (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u))
          (single h
              ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                a) :
            G →₀ (↑A : Type u))
          (single (g * h) a) +
        single g a) =
    HAdd.hAdd (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u))
      (single g⁻¹
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a) :
        G →₀ (↑A : Type u))
      (single g a)

Tactic:
abel
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g : G × G × G
a : (↑A : Type u)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₃₂ A) :
        (a : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)) →
          (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u))
      (single g a) =
    HSub.hSub (α := G × G →₀ (↑A : Type u)) (β := G × G →₀ (↑A : Type u))
          (single (g.2.1, g.2.2)
              ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g.1⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                a) :
            G × G →₀ (↑A : Type u))
          (single (g.1 * g.2.1, g.2.2) a) +
        single (g.1, g.2.1 * g.2.2) a -
      single (g.1, g.2.1) a

Tactic:
simp [d₃₂]

Premises used: groupHomology.d₃₂
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g h : G
a : (↑A : Type u)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₃₂ A) :
        (a : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)) →
          (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u))
      (single (1, g, h) a) =
    HSub.hSub (α := G × G →₀ (↑A : Type u)) (single (1, g * h) a) (single (1, g) a)

Tactic:
simp [d₃₂]

Premises used: groupHomology.d₃₂
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g h : G
a : (↑A : Type u)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₃₂ A) :
        (a : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)) →
          (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u))
      (single (g, 1, h) a) =
    HSub.hSub (α := G × G →₀ (↑A : Type u)) (β := G × G →₀ (↑A : Type u))
      (single (1, h)
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a) :
        G × G →₀ (↑A : Type u))
      (single (g, 1) a)

Tactic:
simp [d₃₂]

Premises used: groupHomology.d₃₂
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g h : G
a : (↑A : Type u)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (d₃₂ A) :
        (a : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)) →
          (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u))
      (single (g, h, 1) a) =
    HSub.hSub (α := G × G →₀ (↑A : Type u)) (β := G × G →₀ (↑A : Type u))
      (single (h, 1)
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
              (a : (↑A : Type u)) → (↑A : Type u))
            a) :
        G × G →₀ (↑A : Type u))
      (single (g * h, 1) a)

Tactic:
simp [d₃₂]

Premises used: groupHomology.d₃₂
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : Fin 1 → G
x_1 : (↑A : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom ((chainsIso₁ A).hom ≫ d₁₀ A) :
          (a : (Fin 1 → G) →₀ (↑A : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        (single x x_1) :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom ((inhomogeneousChains A).d 1 0 ≫ (chainsIso₀ A).hom) :
          (a : (Fin 1 → G) →₀ (↑A : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        (single x x_1) :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))

Tactic:
simp [chainsIso₀, chainsIso₁, d₁₀_single (G := G), ChainComplex.of.d,
      Unique.eq_default (α := Fin 0 → G), sub_eq_add_neg, inhomogeneousChains.d_single (G := G)]

Premises used: sub_eq_add_neg, groupHomology.chainsIso₁, groupHomology.inhomogeneousChains.d_single, Unique.eq_default, ChainComplex.of.d, groupHomology.chainsIso₀, groupHomology.d₁₀_single
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ (chainsIso₁ A).inv ≫ (inhomogeneousChains A).d 1 0 = d₁₀ A ≫ (chainsIso₀ A).inv

Tactic:
(CommSq.horiz_inv ⟨comp_d₁₀_eq A⟩).w

Premises used: CategoryTheory.CommSq.horiz_inv, groupHomology.comp_d₁₀_eq, CategoryTheory.CommSq.mk, CategoryTheory.CommSq.w