awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k 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))
      (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))
have 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))
Tactic: simp only [map_sub, d₂₁_single (G := G), inv_self_apply, mul_inv_cancel, inv_inv,
    inv_mul_cancel]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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 →₀ (↑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)
have 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)
Tactic: simp only [map_add, d₂₁_single (G := G), inv_self_apply, inv_inv, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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 →₀ (↑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)
have 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)
Tactic: simp only [map_add, d₂₁_single (G := G), inv_inv, self_inv_apply, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ d₂₁ A ≫ d₁₀ A = 0
have 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))
Tactic: ext x g
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : G →₀ (↑A : Type u)
⊢ 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)
have 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)
Tactic: change x.sum (fun g a => A.ρ g⁻¹ a - a) = 0 ↔ _
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : G →₀ (↑A : Type u)
⊢ 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)
have 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)
Tactic: rw [sum_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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)
⊢ 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)
have 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)
Tactic: rw [sum_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
⊢ cycles₁ A = ⊤
have rw : (ModuleCat.Hom.hom (d₁₀ A)).ker = ⊤
Tactic: rw [cycles₁, d₁₀_eq_zero_of_isTrivial, ModuleCat.hom_zero, LinearMap.ker_zero]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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 = ⊤
⊢ cycles₁ A = ⊤
have 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)))
Tactic: rw [cycles₁, d₁₀_eq_zero_of_isTrivial, ModuleCat.hom_zero, LinearMap.ker_zero]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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)))
⊢ cycles₁ A = ⊤
have 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) ⊤
Tactic: rw [cycles₁, d₁₀_eq_zero_of_isTrivial, ModuleCat.hom_zero, LinearMap.ker_zero]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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) ⊤
⊢ cycles₁ A = ⊤
have rw₃ : Eq.{u + 1} (α := Submodule k (G →₀ (↑A : Type u))) ⊤ ⊤
Tactic: rw [cycles₁, d₁₀_eq_zero_of_isTrivial, ModuleCat.hom_zero, LinearMap.ker_zero]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : G × G →₀ (↑A : Type u)
⊢ 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)
have 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)
Tactic: change x.sum (fun g a => _) = 0 ↔ _
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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 ↔
    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))
have 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))
      sorry
      (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))
      sorry
      (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]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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
⊢ f ∈ cycles₁ A
have 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))
Tactic: rcases h with ⟨x, rfl⟩
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
a : (↑A : Type u)
⊢ single 1 a ∈ boundaries₁ A
have 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))
Tactic: use single (1, 1) a
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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)) (β := 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
have 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))
Tactic: rw [← d₂₁_single_ρ_add_single_inv_mul g 1]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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)) (β := 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
have 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))
Tactic: rw [← d₂₁_single_inv_mul_ρ_add_single g 1]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
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
⊢ x ∈ cycles₂ A
have 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))
Tactic: rcases h with ⟨x, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g h : G
a : (↑A : Type u)
⊢ HSub.hSub (α := G × G →₀ (↑A : Type u)) (single (1, g * h) a) (single (1, g) a) ∈ boundaries₂ A
have 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)
Tactic: use single (1, g, h) a
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
g h : G
a : (↑A : Type u)
⊢ 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
have 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)
Tactic: use single (g, 1, h) a