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
x : Fin 2 → G
x_1 : (↑A : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
    ((ModuleCat.Hom.hom ((chainsIso₂ A).hom ≫ d₂₁ A) :
          (a : (Fin 2 → G) →₀ (↑A : Type u)) → (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
        (single x x_1) :
      (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
    ((ModuleCat.Hom.hom ((inhomogeneousChains A).d 2 1 ≫ (chainsIso₁ A).hom) :
          (a : (Fin 2 → G) →₀ (↑A : Type u)) → (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
        (single x x_1) :
      (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))

Tactic:
simp [chainsIso₁, add_assoc, chainsIso₂, d₂₁_single (G := G),
      -Finsupp.domLCongr_apply, domLCongr_single, sub_eq_add_neg, ChainComplex.of.d,
      Fin.contractNth, inhomogeneousChains.d_single (G := G)]

Premises used: add_assoc, sub_eq_add_neg, groupHomology.chainsIso₁, groupHomology.inhomogeneousChains.d_single, Finsupp.domLCongr_apply, ChainComplex.of.d, groupHomology.chainsIso₂, groupHomology.d₂₁_single, Fin.contractNth, Finsupp.domLCongr_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 2 1 = d₂₁ A ≫ (chainsIso₁ A).inv

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

Premises used: groupHomology.comp_d₂₁_eq, CategoryTheory.CommSq.horiz_inv, CategoryTheory.CommSq.mk, CategoryTheory.CommSq.w
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : Fin 3 → G
x_1 : (↑A : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u))
    ((ModuleCat.Hom.hom ((chainsIso₃ A).hom ≫ d₃₂ A) :
          (a : (Fin 3 → G) →₀ (↑A : Type u)) → (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u))
        (single x x_1) :
      (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u))
    ((ModuleCat.Hom.hom ((inhomogeneousChains A).d 3 2 ≫ (chainsIso₂ A).hom) :
          (a : (Fin 3 → G) →₀ (↑A : Type u)) → (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u))
        (single x x_1) :
      (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u))

Tactic:
simp [chainsIso₂, ChainComplex.of.d, pow_succ, chainsIso₃,
      -domLCongr_apply, domLCongr_single, d₃₂, Fin.sum_univ_three,
      Fin.contractNth, Fin.tail_def, sub_eq_add_neg, add_assoc,
      inhomogeneousChains.d_single (G := G), add_rotate' (-(single (_ * _, _) _)),
      add_left_comm (single (_, _ * _) _)]

Premises used: groupHomology.d₃₂, HMul.hMul, add_left_comm, pow_succ, add_assoc, sub_eq_add_neg, Prod.mk, Fin.sum_univ_three, groupHomology.inhomogeneousChains.d_single, add_rotate', Finsupp.domLCongr_apply, ChainComplex.of.d, groupHomology.chainsIso₂, Fin.tail_def, Fin.contractNth, groupHomology.chainsIso₃, Neg.neg, Finsupp.domLCongr_single, Finsupp.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 3 2 = d₃₂ A ≫ (chainsIso₂ A).inv

Tactic:
(CommSq.horiz_inv ⟨comp_d₃₂_eq A⟩).w

Premises used: CategoryTheory.CommSq.horiz_inv, CategoryTheory.CommSq.mk, CategoryTheory.CommSq.w, groupHomology.comp_d₃₂_eq
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
hf :
  ∀ (x : G × G) (g : (↑A : Type u)),
    Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      ((ModuleCat.Hom.hom (d₂₁ A ≫ d₁₀ A) ∘ₗ lsingle x :
            (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
          g :
        (↑(ModuleCat.of k (↑A : Type u)) : Type u))
      (((ModuleCat.Hom.hom 0 :
                (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u) →ₗ[k]
                  (↑(ModuleCat.of k (↑A : Type u)) : Type u)) ∘ₗ
              lsingle x :
            (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
          g :
        (↑(ModuleCat.of k (↑A : Type u)) : Type u))
⊢ d₂₁ A ≫ d₁₀ A = 0

Tactic:
ext x g
-- 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
g : (↑A : Type u)
⊢ Eq (α := (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    ((ModuleCat.Hom.hom (d₂₁ A ≫ d₁₀ A) ∘ₗ lsingle x : (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        g :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))
    (((ModuleCat.Hom.hom 0 :
              (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u) →ₗ[k] (↑(ModuleCat.of k (↑A : Type u)) : Type u)) ∘ₗ
            lsingle x :
          (a : (↑A : Type u)) → (↑(ModuleCat.of k (↑A : Type u)) : Type u))
        g :
      (↑(ModuleCat.of k (↑A : Type u)) : Type u))

Tactic:
simp [d₁₀, d₂₁, sum_add_index', sum_sub_index, sub_sub_sub_comm, add_sub_add_comm]

Premises used: sub_sub_sub_comm, Finsupp.sum_sub_index, Finsupp.sum_add_index', groupHomology.d₁₀, groupHomology.d₂₁, add_sub_add_comm
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ d₃₂ A ≫ d₂₁ A = 0

Tactic:
simp [← cancel_mono (chainsIso₁ A).inv, ← eq_d₂₁_comp_inv, ← eq_d₃₂_comp_inv_assoc,
    ChainComplex.of.d, inhomogeneousChains.d_comp_d]

Premises used: groupHomology.eq_d₂₁_comp_inv, CategoryTheory.cancel_mono, groupHomology.chainsIso₁, groupHomology.eq_d₃₂_comp_inv_assoc, ChainComplex.of.d, groupHomology.inhomogeneousChains.d_comp_d, CategoryTheory.Iso.inv
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : G →₀ (↑A : Type u)
change :
  Eq (α := (↑A : Type u))
      (x.sum fun (g : G) (a : (↑A : Type u)) ↦
        HSub.hSub (α := (↑A : Type u))
          ((((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 :
            (↑A : Type u))
          a)
      0 ↔
    Eq (α := (↑A : Type u))
      (x.sum fun (g : G) (a : (↑A : Type u)) ↦
        (((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)
      (x.sum fun (x : G) (a : (↑A : Type u)) ↦ a)
⊢ x ∈ cycles₁ A ↔
    Eq (α := (↑A : Type u))
      (x.sum fun (g : G) (a : (↑A : Type u)) ↦
        (((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)
      (x.sum fun (x : G) (a : (↑A : Type u)) ↦ a)

Tactic:
change x.sum (fun g a => A.ρ g⁻¹ a - a) = 0 ↔ _

Premises used: HSub.hSub, Finsupp.sum, Inv.inv, Rep.ρ, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : G →₀ (↑A : Type u)
rw :
  HSub.hSub (α := (↑A : Type u))
        (x.sum fun (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)))
        (x.sum fun (g : G) (a : (↑A : Type u)) ↦ a) =
      0 ↔
    Eq (α := (↑A : Type u))
      (x.sum fun (g : G) (a : (↑A : Type u)) ↦
        (((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)
      (x.sum fun (x : G) (a : (↑A : Type u)) ↦ a)
rw₁ rw₂ :
  Eq (α := (↑A : Type u))
      (x.sum fun (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)))
      (x.sum fun (g : G) (a : (↑A : Type u)) ↦ a) ↔
    Eq (α := (↑A : Type u))
      (x.sum fun (g : G) (a : (↑A : Type u)) ↦
        (((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)
      (x.sum fun (x : G) (a : (↑A : Type u)) ↦ a)
⊢ Eq (α := (↑A : Type u))
      (x.sum fun (g : G) (a : (↑A : Type u)) ↦
        HSub.hSub (α := (↑A : Type u))
          ((((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 :
            (↑A : Type u))
          a)
      0 ↔
    Eq (α := (↑A : Type u))
      (x.sum fun (g : G) (a : (↑A : Type u)) ↦
        (((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)
      (x.sum fun (x : G) (a : (↑A : Type u)) ↦ a)

Tactic:
rw [sum_sub, sub_eq_zero]

Premises used: sub_eq_zero, Finsupp.sum_sub
-- 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)
⊢ single g a ∈ cycles₁ A ↔
    (((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 =
      a

Tactic:
simp [mem_cycles₁_iff, ← (A.ρ.apply_bijective g).1.eq_iff (a := A.ρ g⁻¹ a), eq_comm]

Premises used: Function.Injective.eq_iff, Representation.apply_bijective, eq_comm, And.left, Rep.ρ, groupHomology.mem_cycles₁_iff
-- 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)
ha : a ∈ A.ρ.invariants
⊢ single g a ∈ cycles₁ A

Tactic:
(single_mem_cycles₁_iff g a).2 (ha g)

Premises used: Iff.mpr, groupHomology.single_mem_cycles₁_iff
-- 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)
⊢ Membership.mem (α := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) (cycles₁ 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))
        x :
      (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))

Tactic:
congr($(d₂₁_comp_d₁₀ A) x)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, id, groupHomology.d₂₁_comp_d₁₀, DFunLike.coe
-- 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
rw : (ModuleCat.Hom.hom (d₁₀ A)).ker = ⊤
rw₁ :
  Eq.{u + 1} (α := Submodule k (G →₀ (↑A : Type u)))
    (LinearMap.ker (R₂ := k) (M₂ := (↑(ModuleCat.of k (↑A : Type u)) : Type u)) (τ₁₂ := RingHom.id k)
        (ModuleCat.Hom.hom 0) :
      Submodule k (G →₀ (↑A : Type u)))
    (⊤ : Submodule k (G →₀ (↑A : Type u)))
rw₂ :
  Eq.{u + 1} (α := Submodule k (G →₀ (↑A : Type u)))
    (LinearMap.ker (R₂ := k) (M₂ := (↑(ModuleCat.of k (↑A : Type u)) : Type u)) (τ₁₂ := RingHom.id k) 0) ⊤
rw₃ rw₄ : Eq.{u + 1} (α := Submodule k (G →₀ (↑A : Type u))) ⊤ ⊤
⊢ cycles₁ A = ⊤

Tactic:
rw [cycles₁, d₁₀_eq_zero_of_isTrivial, ModuleCat.hom_zero, LinearMap.ker_zero]

Premises used: ModuleCat.hom_zero, LinearMap.ker_zero, groupHomology.cycles₁, groupHomology.d₁₀_eq_zero_of_isTrivial
-- 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
x : ↥(cycles₁ A)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (cycles₁IsoOfIsTrivial A).hom :
        (a : (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u)) → (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
      x =
    (↑x : G →₀ (↑A : Type u))

Tactic:
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
inst_2 : A.IsTrivial
x : G →₀ (↑A : Type u)
⊢ (↑((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (cycles₁IsoOfIsTrivial A).inv :
            (a : (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u)) → (↑(ModuleCat.of k ↥(cycles₁ A)) : Type u))
          x) :
      G →₀ (↑A : Type u)) =
    x

Tactic:
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 : G × G →₀ (↑A : Type u)
change :
  Eq (α := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
      (x.sum fun (g : G × G) (a : (↑A : Type u)) ↦
        ((fun (g : G × G) ↦
                HSub.hSub (α := (↑A : Type u) →ₗ[k] G →₀ (↑A : Type u))
                    (lsingle g.2 ∘ₗ (A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g.1⁻¹) (lsingle (g.1 * g.2)) +
                  lsingle g.1)
              g :
            (a : (↑A : Type u)) → G →₀ (↑A : Type u))
          a)
      0 ↔
    Eq (α := G →₀ (↑A : Type u))
      (x.sum fun (g : G × G) (a : (↑A : Type u)) ↦
        HAdd.hAdd (α := 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 a))
      (x.sum fun (g : G × G) (a : (↑A : Type u)) ↦ single (g.1 * g.2) a)
⊢ x ∈ cycles₂ A ↔
    Eq (α := G →₀ (↑A : Type u))
      (x.sum fun (g : G × G) (a : (↑A : Type u)) ↦
        HAdd.hAdd (α := 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 a))
      (x.sum fun (g : G × G) (a : (↑A : Type u)) ↦ single (g.1 * g.2) a)

Tactic:
change x.sum (fun g a => _) = 0 ↔ _

Premises used: Finsupp.sum
-- 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)
⊢ Eq (α := (↑(ModuleCat.of k (G →₀ (↑A : Type u))) : Type u))
      (x.sum fun (g : G × G) (a : (↑A : Type u)) ↦
        ((fun (g : G × G) ↦
                HSub.hSub (α := (↑A : Type u) →ₗ[k] G →₀ (↑A : Type u))
                    (lsingle g.2 ∘ₗ (A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g.1⁻¹) (lsingle (g.1 * g.2)) +
                  lsingle g.1)
              g :
            (a : (↑A : Type u)) → G →₀ (↑A : Type u))
          a)
      0 ↔
    Eq (α := G →₀ (↑A : Type u))
      (x.sum fun (g : G × G) (a : (↑A : Type u)) ↦
        HAdd.hAdd (α := 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 a))
      (x.sum fun (g : G × G) (a : (↑A : Type u)) ↦ single (g.1 * g.2) a)

Tactic:
simp [sub_add_eq_add_sub, sub_eq_zero]

Premises used: sub_eq_zero, sub_add_eq_add_sub
-- 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)
⊢ single g a ∈ cycles₂ A ↔
    HAdd.hAdd (α := 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 a) =
      single (g.1 * g.2) a

Tactic:
simp [mem_cycles₂_iff]

Premises used: groupHomology.mem_cycles₂_iff
-- 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)
rw :
  single g a ∈ cycles₂ A ↔
    Eq (α := G →₀ (↑A : Type u))
      (mapRange
        (⇑((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))
        ⋯
        (single (g.1 * 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)))
      (mapRange
        (⇑((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))
        ⋯
        (HAdd.hAdd (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single g.2 a)
          (single g.1
              ((((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 a ∈ cycles₂ A ↔
    single (g.1 * 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) =
      HAdd.hAdd (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single g.2 a)
        (single g.1
            ((((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))

Tactic:
rw [← (mapRange_injective (α := G) _ (map_zero _) (A.ρ.apply_bijective g.1⁻¹).1).eq_iff]

Premises used: Function.Injective.eq_iff, map_zero, Representation.apply_bijective, Finsupp.mapRange_injective, Prod.fst, Inv.inv, And.left, Rep.ρ
-- 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)
⊢ single g a ∈ cycles₂ A ↔
    Eq (α := G →₀ (↑A : Type u))
      (mapRange
        (⇑((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))
        ⋯
        (single (g.1 * 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)))
      (mapRange
        (⇑((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))
        ⋯
        (HAdd.hAdd (α := G →₀ (↑A : Type u)) (β := G →₀ (↑A : Type u)) (single g.2 a)
          (single g.1
              ((((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))))

Tactic:
simp [mem_cycles₂_iff, mapRange_add, eq_comm]

Premises used: groupHomology.mem_cycles₂_iff, eq_comm, Finsupp.mapRange_add
-- 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 × G →₀ (↑A : Type u)
⊢ Membership.mem (α := (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) (cycles₂ 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 × G →₀ (↑A : Type u))) : Type u)) →
            (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u))
        x :
      (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u))

Tactic:
congr($(d₃₂_comp_d₂₁ A) x)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, id, groupHomology.d₃₂_comp_d₂₁, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
f : G →₀ (↑A : Type u)
h : f ∈ boundaries₁ A
rcases :
  ∀ (x : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)),
    Membership.mem (α := G →₀ (↑A : Type u)) (cycles₁ A)
      ((ModuleCat.Hom.hom (d₂₁ A) : (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → G →₀ (↑A : Type u))
          x :
        G →₀ (↑A : Type u))
⊢ f ∈ 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 →₀ (↑A : Type u))) : Type u)
⊢ Membership.mem (α := G →₀ (↑A : Type u)) (cycles₁ A)
    ((ModuleCat.Hom.hom (d₂₁ A) : (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → G →₀ (↑A : Type u)) x :
      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 →₀ (↑A : Type u))) : Type u)
⊢ Membership.mem (α := G →₀ (↑A : Type u)) (cycles₁ A)
    ((ModuleCat.Hom.hom (d₂₁ A) : (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → G →₀ (↑A : Type u)) x :
      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 →₀ (↑A : Type u)) =
    (↑x : 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
a : (↑A : Type u)
h :
  Eq (α := G →₀ (↑A : Type u))
    ((ModuleCat.Hom.hom (d₂₁ A) : (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → G →₀ (↑A : Type u))
        (single (1, 1) a) :
      G →₀ (↑A : Type u))
    (single 1 a : G →₀ (↑A : Type u))
⊢ single 1 a ∈ boundaries₁ A

Tactic:
use single (1, 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
a : (↑A : Type u)
⊢ Eq (α := G →₀ (↑A : Type u))
    ((ModuleCat.Hom.hom (d₂₁ A) : (a : (↑(ModuleCat.of k (G × G →₀ (↑A : Type u))) : Type u)) → G →₀ (↑A : Type u))
        (single (1, 1) a) :
      G →₀ (↑A : Type u))
    (single 1 a : G →₀ (↑A : Type u))

Tactic:
simp [d₂₁]

Premises used: groupHomology.d₂₁