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
g : G
a : (↑A : Type u)
rw :
  Membership.mem (α := G →₀ (↑A : Type u)) (boundaries₁ 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, 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⁻¹, g * 1) a)) :
      (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
⊢ 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) ∈
    boundaries₁ A

Tactic:
rw [← d₂₁_single_ρ_add_single_inv_mul g 1]

Premises used: OfNat.ofNat, groupHomology.d₂₁_single_ρ_add_single_inv_mul
-- 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)
⊢ Membership.mem (α := G →₀ (↑A : Type u)) (boundaries₁ 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, 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⁻¹, g * 1) a)) :
      (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))

Tactic:
Set.mem_range_self _

Premises used: Set.mem_range_self, Set.Mem, setOf, Set.range
-- 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)
⊢ Membership.mem (α := G →₀ (↑A : Type u)) (boundaries₁ 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, 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⁻¹, g * 1) a)) :
      (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))

Tactic:
exact Set.mem_range_self _

Premises used: Set.mem_range_self
-- 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)
rw :
  Membership.mem (α := G →₀ (↑A : Type u)) (boundaries₁ 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 * 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, 1) a)) :
      (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
⊢ 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) ∈
    boundaries₁ A

Tactic:
rw [← d₂₁_single_inv_mul_ρ_add_single g 1]

Premises used: groupHomology.d₂₁_single_inv_mul_ρ_add_single, OfNat.ofNat
-- 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)
⊢ Membership.mem (α := G →₀ (↑A : Type u)) (boundaries₁ 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 * 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, 1) a)) :
      (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))

Tactic:
Set.mem_range_self _

Premises used: Set.mem_range_self, Set.Mem, setOf, Set.range
-- 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)
⊢ Membership.mem (α := G →₀ (↑A : Type u)) (boundaries₁ 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 * 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, 1) a)) :
      (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))

Tactic:
exact Set.mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : G × G →₀ (↑A : Type u)
h : x ∈ boundaries₂ A
rcases :
  ∀ (x : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)),
    Membership.mem (α := G × G →₀ (↑A : Type u)) (cycles₂ A)
      ((ModuleCat.Hom.hom (d₃₂ A) :
            (a : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)) → G × G →₀ (↑A : Type u))
          x :
        G × G →₀ (↑A : Type u))
⊢ x ∈ cycles₂ A

Tactic:
rcases h with ⟨x, rfl⟩

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)
⊢ Membership.mem (α := G × G →₀ (↑A : Type u)) (cycles₂ A)
    ((ModuleCat.Hom.hom (d₃₂ A) :
          (a : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)) → G × G →₀ (↑A : Type u))
        x :
      G × G →₀ (↑A : Type u))

Tactic:
d₃₂_apply_mem_cycles₂ x

Premises used: Set.Mem, groupHomology.d₃₂_apply_mem_cycles₂
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)
⊢ Membership.mem (α := G × G →₀ (↑A : Type u)) (cycles₂ A)
    ((ModuleCat.Hom.hom (d₃₂ A) :
          (a : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)) → G × G →₀ (↑A : Type u))
        x :
      G × G →₀ (↑A : Type u))

Tactic:
exact d₃₂_apply_mem_cycles₂ x

Premises used: groupHomology.d₃₂_apply_mem_cycles₂
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ boundaries₂ A ≤ cycles₂ A

Tactic:
mem_cycles₂_of_mem_boundaries₂

Premises used: groupHomology.mem_cycles₂_of_mem_boundaries₂
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(boundaries₂ A)
⊢ (↑((boundariesToCycles₂ A : (a : ↥(boundaries₂ A)) → ↥(cycles₂ A)) x) : G × G →₀ (↑A : Type u)) =
    (↑x : G × G →₀ (↑A : Type u))

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, Set.range, rfl
-- 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)
h₁ :
  (ModuleCat.Hom.hom (d₃₂ A) : (a : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)) → G × G →₀ (↑A : Type u))
      (single (1, g, h) a) =
    HSub.hSub (α := G × G →₀ (↑A : Type u)) (single (1, g * h) a) (single (1, g) a)
⊢ HSub.hSub (α := G × G →₀ (↑A : Type u)) (single (1, g * h) a) (single (1, g) a) ∈ boundaries₂ A

Tactic:
use single (1, g, h) a

Premises used: Prod.mk, OfNat.ofNat, Finsupp.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)
⊢ (ModuleCat.Hom.hom (d₃₂ A) : (a : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)) → G × G →₀ (↑A : 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)
h₁ :
  (ModuleCat.Hom.hom (d₃₂ A) : (a : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)) → G × G →₀ (↑A : 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)
⊢ 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) ∈
    boundaries₂ A

Tactic:
use single (g, 1, h) a

Premises used: Prod.mk, OfNat.ofNat, Finsupp.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)
⊢ (ModuleCat.Hom.hom (d₃₂ A) : (a : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)) → G × G →₀ (↑A : 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)
h₁ :
  (ModuleCat.Hom.hom (d₃₂ A) : (a : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)) → G × G →₀ (↑A : Type u))
      (single (g, 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))) =
    HSub.hSub (α := G × G →₀ (↑A : Type u)) (β := G × G →₀ (↑A : Type u))
      (single (g, 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 (1, h) a)
⊢ HSub.hSub (α := G × G →₀ (↑A : Type u)) (β := G × G →₀ (↑A : Type u))
      (single (g, 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 (1, h) a) ∈
    boundaries₂ A

Tactic:
use single (g, 1, h) (A.ρ g (-a))

Premises used: Prod.mk, Rep.ρ, OfNat.ofNat, DFunLike.coe, Neg.neg, Finsupp.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)
⊢ (ModuleCat.Hom.hom (d₃₂ A) : (a : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)) → G × G →₀ (↑A : Type u))
      (single (g, 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))) =
    HSub.hSub (α := G × G →₀ (↑A : Type u)) (β := G × G →₀ (↑A : Type u))
      (single (g, 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 (1, h) a)

Tactic:
simp [d₃₂_single (G := G)]

Premises used: 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)
h₁ :
  (ModuleCat.Hom.hom (d₃₂ A) : (a : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)) → G × G →₀ (↑A : 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)
⊢ 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) ∈
    boundaries₂ A

Tactic:
use single (g, h, 1) a

Premises used: Prod.mk, OfNat.ofNat, Finsupp.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)
⊢ (ModuleCat.Hom.hom (d₃₂ A) : (a : (↑(ModuleCat.of k (G × G × G →₀ (↑A : Type u))) : Type u)) → G × G →₀ (↑A : 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:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
g : G
a : A
rw : IsCycle₁ (single g a) ↔ g⁻¹ • g • a = g⁻¹ • a
⊢ IsCycle₁ (single g a) ↔ g • a = a

Tactic:
rw [← (MulAction.bijective g⁻¹).1.eq_iff]

Premises used: MulAction.bijective, Function.Injective.eq_iff, Inv.inv, And.left
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
g : G
a : A
⊢ IsCycle₁ (single g a) ↔ g⁻¹ • g • a = g⁻¹ • a

Tactic:
simp [IsCycle₁, eq_comm]

Premises used: groupHomology.IsCycle₁, eq_comm
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
g : G
a : A
ha : a ∈ MulAction.fixedPoints G A
⊢ IsCycle₁ (single g a)

Tactic:
simp_all [IsCycle₁]

Premises used: groupHomology.IsCycle₁
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
g : G × G
a : A
⊢ IsCycle₂ (single g a) ↔ HAdd.hAdd (α := G →₀ A) (single g.2 (g.1⁻¹ • a)) (single g.1 a) = single (g.1 * g.2) a

Tactic:
simp [IsCycle₂]

Premises used: groupHomology.IsCycle₂
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
g : G × G
a : A
rw :
  IsCycle₂ (single g a) ↔
    mapRange (HSMul.hSMul g.1⁻¹) ⋯ (HAdd.hAdd (α := G →₀ A) (single g.2 a) (single g.1 (g.1 • a))) =
      mapRange (HSMul.hSMul g.1⁻¹) ⋯ (single (g.1 * g.2) (g.1 • a))
⊢ IsCycle₂ (single g a) ↔ HAdd.hAdd (α := G →₀ A) (single g.2 a) (single g.1 (g.1 • a)) = single (g.1 * g.2) (g.1 • a)

Tactic:
rw [← (Finsupp.mapRange_injective (α := G) _ (smul_zero _) (MulAction.bijective g.1⁻¹).1).eq_iff]

Premises used: Function.Injective.eq_iff, smul_zero, Finsupp.mapRange_injective
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
g : G × G
a : A
⊢ IsCycle₂ (single g a) ↔
    mapRange (HSMul.hSMul g.1⁻¹) ⋯ (HAdd.hAdd (α := G →₀ A) (single g.2 a) (single g.1 (g.1 • a))) =
      mapRange (HSMul.hSMul g.1⁻¹) ⋯ (single (g.1 * g.2) (g.1 • a))

Tactic:
simp [mapRange_add, IsCycle₂]

Premises used: groupHomology.IsCycle₂, Finsupp.mapRange_add
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
a : A
mp : IsBoundary₀ G a → ∃ (x : G →₀ A), (x.sum fun (g : G) (z : A) ↦ g • z - z) = a
mpr : (∃ (x : G →₀ A), (x.sum fun (g : G) (z : A) ↦ g • z - z) = a) → IsBoundary₀ G a
⊢ IsBoundary₀ G a ↔ ∃ (x : G →₀ A), (x.sum fun (g : G) (z : A) ↦ g • z - z) = a

Tactic:
constructor
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
a : A
x : G →₀ A
hx : (x.sum fun (g : G) (z : A) ↦ g⁻¹ • z - z) = a
h : (sum (x.sum fun (g : G) (a : A) ↦ single g (-(g⁻¹ • a))) fun (g : G) (z : A) ↦ g • z - z) = a
⊢ ∃ (x : G →₀ A), (x.sum fun (g : G) (z : A) ↦ g • z - z) = a

Tactic:
use x.sum (fun g a => single g (-(g⁻¹ • a)))

Premises used: Finsupp.sum, Inv.inv, HSMul.hSMul, Neg.neg, Finsupp.single
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
a : A
x : G →₀ A
hx : (x.sum fun (g : G) (z : A) ↦ g⁻¹ • z - z) = a
⊢ (sum (x.sum fun (g : G) (a : A) ↦ single g (-(g⁻¹ • a))) fun (g : G) (z : A) ↦ g • z - z) = a

Tactic:
simp_all [sum_neg_index, sum_sum_index, neg_add_eq_sub]

Premises used: neg_add_eq_sub, Finsupp.sum_neg_index, Finsupp.sum_sum_index
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
a : A
x : G →₀ A
hx : (x.sum fun (g : G) (z : A) ↦ g • z - z) = a
h : (sum (x.sum fun (g : G) (a : A) ↦ single g (-(g • a))) fun (g : G) (z : A) ↦ g⁻¹ • z - z) = a
⊢ IsBoundary₀ G a

Tactic:
use x.sum (fun g a => single g (-(g • a)))

Premises used: Finsupp.sum, HSMul.hSMul, Neg.neg, Finsupp.single
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
a : A
x : G →₀ A
hx : (x.sum fun (g : G) (z : A) ↦ g • z - z) = a
⊢ (sum (x.sum fun (g : G) (a : A) ↦ single g (-(g • a))) fun (g : G) (z : A) ↦ g⁻¹ • z - z) = a

Tactic:
simp_all [sum_neg_index, sum_sum_index, neg_add_eq_sub]

Premises used: neg_add_eq_sub, Finsupp.sum_neg_index, Finsupp.sum_sum_index
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
x : G →₀ A
mp :
  IsBoundary₁ x →
    ∃ (y : Finsupp.{u_1, u_2} (G × G) A),
      (y.sum fun (g : G × G) (a : A) ↦
          HSub.hSub (α := G →₀ A) (single g.2 a) (single (g.1 * g.2) (g.1 • a)) + single g.1 (g.1 • a)) =
        x
mpr :
  (∃ (y : Finsupp.{u_1, u_2} (G × G) A),
      (y.sum fun (g : G × G) (a : A) ↦
          HSub.hSub (α := G →₀ A) (single g.2 a) (single (g.1 * g.2) (g.1 • a)) + single g.1 (g.1 • a)) =
        x) →
    IsBoundary₁ x
⊢ IsBoundary₁ x ↔
    ∃ (y : Finsupp.{u_1, u_2} (G × G) A),
      (y.sum fun (g : G × G) (a : A) ↦
          HSub.hSub (α := G →₀ A) (single g.2 a) (single (g.1 * g.2) (g.1 • a)) + single g.1 (g.1 • a)) =
        x

Tactic:
constructor
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
x : G →₀ A
y : Finsupp.{u_1, u_2} (G × G) A
hy :
  (y.sum fun (g : G × G) (a : A) ↦
      HSub.hSub (α := G →₀ A) (single g.2 (g.1⁻¹ • a)) (single (g.1 * g.2) a) + single g.1 a) =
    x
h :
  (sum (y.sum fun (g : G × G) (a : A) ↦ single g (g.1⁻¹ • a)) fun (g : G × G) (a : A) ↦
      HSub.hSub (α := G →₀ A) (single g.2 a) (single (g.1 * g.2) (g.1 • a)) + single g.1 (g.1 • a)) =
    x
⊢ ∃ (y : Finsupp.{u_1, u_2} (G × G) A),
    (y.sum fun (g : G × G) (a : A) ↦
        HSub.hSub (α := G →₀ A) (single g.2 a) (single (g.1 * g.2) (g.1 • a)) + single g.1 (g.1 • a)) =
      x

Tactic:
use y.sum (fun g a => single g (g.1⁻¹ • a))

Premises used: Finsupp.sum, Prod.fst, Inv.inv, HSMul.hSMul, Finsupp.single
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
x : G →₀ A
y : Finsupp.{u_1, u_2} (G × G) A
hy :
  (y.sum fun (g : G × G) (a : A) ↦
      HSub.hSub (α := G →₀ A) (single g.2 (g.1⁻¹ • a)) (single (g.1 * g.2) a) + single g.1 a) =
    x
⊢ (sum (y.sum fun (g : G × G) (a : A) ↦ single g (g.1⁻¹ • a)) fun (g : G × G) (a : A) ↦
      HSub.hSub (α := G →₀ A) (single g.2 a) (single (g.1 * g.2) (g.1 • a)) + single g.1 (g.1 • a)) =
    x

Tactic:
simp_all [sum_sum_index]

Premises used: Finsupp.sum_sum_index
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
x_1 : G →₀ A
x : Finsupp.{u_1, u_2} (G × G) A
hx :
  (x.sum fun (g : G × G) (a : A) ↦
      HSub.hSub (α := G →₀ A) (single g.2 a) (single (g.1 * g.2) (g.1 • a)) + single g.1 (g.1 • a)) =
    x_1
h :
  (sum (x.sum fun (g : G × G) (a : A) ↦ single g (g.1 • a)) fun (g : G × G) (a : A) ↦
      HSub.hSub (α := G →₀ A) (single g.2 (g.1⁻¹ • a)) (single (g.1 * g.2) a) + single g.1 a) =
    x_1
⊢ IsBoundary₁ x_1

Tactic:
use x.sum (fun g a => single g (g.1 • a))

Premises used: Finsupp.sum, Prod.fst, HSMul.hSMul, Finsupp.single