awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : ↥(cocycles₁ A)
g : G
rw :
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
    0
rw₁ :
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
    (f : (a : G) → (↑A : Type u_1)) 1
rw₂ :
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
    (f : (a : G) → (↑A : Type u_1)) (g * g⁻¹)
rw₃ rw₄ :
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
⊢ Eq.{u_1 + 1} (α := (↑A : Type u_1))
    ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
          (a : (↑A : Type u_1)) → (↑A : Type u_1))
        ((f : (a : G) → (↑A : Type u_1)) g⁻¹ : (↑A : Type u_1)) :
      (↑A : Type u_1))
    (-(f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))

Tactic:
rw [← add_eq_zero_iff_eq_neg, ← cocycles₁_map_one f, ← mul_inv_cancel g,
    (mem_cocycles₁_iff f).1 f.2 g g⁻¹]

Premises used: add_eq_zero_iff_eq_neg, groupCohomology.mem_cocycles₁_iff, Inv.inv, groupCohomology.cocycles₁_map_one, Iff.mp, mul_inv_cancel, DFunLike.coe, Subtype.property
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑A : Type (max u u_1))
⊢ Membership.mem (α := (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1))) (cocycles₁ A)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u u_1)) →ₗ[k] (↑x2 : Type (max u u_1)))
            (CC := ModuleCat.carrier) (d₀₁.{u, u_1} A) :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))
        x :
      (↑(ModuleCat.of k (G → (↑A : Type (max u u_1)))) : Type (max u u_1)))

Tactic:
d₀₁_comp_d₁₂_apply _ _

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, groupCohomology.d₀₁_comp_d₁₂_apply
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
x : ↥(cocycles₁ A)
⊢ Eq (α := (↑(ModuleCat.of k (G × G → (↑A : Type u_1))) : Type (max u u_1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u u_1)) →ₗ[k] (↑x2 : Type (max u u_1)))
            (CC := ModuleCat.carrier) (d₁₂ A) :
          (a : (↑(ModuleCat.of k (G → (↑A : Type u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G × G → (↑A : Type u_1))) : Type (max u u_1)))
        (⇑x : (a : G) → (↑A : Type u_1)) :
      (↑(ModuleCat.of k (G × G → (↑A : Type u_1))) : Type (max u u_1)))
    (0 : (↑(ModuleCat.of k (G × G → (↑A : Type u_1))) : Type (max u u_1)))

Tactic:
x.2

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, Subtype.property
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
inst_2 : A.IsTrivial
f : ↥(cocycles₁ A)
g h : G
rw :
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1))
rw₁ :
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1)) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1))
rw₂ rw₃ :
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1)) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1))
⊢ (f : (a : G) → (↑A : Type u_1)) (g * h) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G) → (↑A : Type u_1)) g : (↑A : Type u_1))
      ((f : (a : G) → (↑A : Type u_1)) h : (↑A : Type u_1))

Tactic:
rw [(mem_cocycles₁_iff f).1 f.2, isTrivial_apply A.ρ g (f h), add_comm]

Premises used: groupCohomology.mem_cocycles₁_iff, add_comm, Representation.isTrivial_apply, Rep.ρ, Iff.mp, DFunLike.coe, Subtype.property
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
inst_2 : A.IsTrivial
f : AddMonoidHom.{u, u_1} (Additive G) (↑A : Type u_1)
g h : G
⊢ Function.comp (β := Additive G) (⇑f : (a : Additive G) → (↑A : Type u_1)) (⇑Additive.ofMul : (a : G) → Additive G)
      (g * h) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          (Function.comp (β := Additive G) (⇑f : (a : Additive G) → (↑A : Type u_1))
            (⇑Additive.ofMul : (a : G) → Additive G) h) :
        (↑A : Type u_1))
      (Function.comp (β := Additive G) (⇑f : (a : Additive G) → (↑A : Type u_1))
          (⇑Additive.ofMul : (a : G) → Additive G) g :
        (↑A : Type u_1))

Tactic:
simp only [Function.comp_apply, ofMul_mul, map_add,
      isTrivial_apply A.ρ g (f (Additive.ofMul h)), add_comm (f (Additive.ofMul g))]

Premises used: map_add, Additive.ofMul, add_comm, Representation.isTrivial_apply, Rep.ρ, ofMul_mul, Function.comp_apply, DFunLike.coe
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : G × G → (↑A : Type u_1)
hf : f ∈ cocycles₂ A
⊢ (⇑(Subtype.mk (p := fun (x : G × G → (↑A : Type u_1)) ↦ x ∈ cocycles₂ A) f hf) : (a : G × G) → (↑A : Type u_1)) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : ↥(cocycles₂ A)
⊢ (↑f : G × G → (↑A : Type u_1)) = (⇑f : (a : G × G) → (↑A : Type u_1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f₁ f₂ : ↥(cocycles₂ A)
h :
  ∀ (g h : G),
    Eq.{u_1 + 1} (α := (↑A : Type u_1)) ((f₁ : (a : G × G) → (↑A : Type u_1)) (g, h) : (↑A : Type u_1))
      ((f₂ : (a : G × G) → (↑A : Type u_1)) (g, h) : (↑A : Type u_1))
⊢ f₁ = f₂

Tactic:
DFunLike.ext f₁ f₂ (Prod.forall.mpr h)

Premises used: Iff.mpr, DFunLike.ext, Prod.forall
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : G × G → (↑A : Type u_1)
simp_rw :
  (∀ (a a_1 b : G),
      HSub.hSub (α := (↑A : Type u_1))
              ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) a : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                    (a : (↑A : Type u_1)) → (↑A : Type u_1))
                  (f (a_1, b)) :
                (↑A : Type u_1))
              (f (a * a_1, b)) +
            f (a, a_1 * b) -
          f (a, a_1) =
        0 (a, a_1, b)) ↔
    ∀ (g h j : G),
      HSub.hSub (α := (↑A : Type u_1))
              ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                    (a : (↑A : Type u_1)) → (↑A : Type u_1))
                  (f (h, j)) :
                (↑A : Type u_1))
              (f (g * h, j)) +
            f (g, h * j) -
          f (g, h) =
        0
⊢ Eq (α := (↑(ModuleCat.of k (G × G × G → (↑A : Type u_1))) : Type (max u u_1)))
      ((ModuleCat.Hom.hom (d₂₃ A) :
            (a : G × G → (↑A : Type u_1)) → (↑(ModuleCat.of k (G × G × G → (↑A : Type u_1))) : Type (max u u_1)))
          f :
        (↑(ModuleCat.of k (G × G × G → (↑A : Type u_1))) : Type (max u u_1)))
      (0 : (↑(ModuleCat.of k (G × G × G → (↑A : Type u_1))) : Type (max u u_1))) ↔
    ∀ (g h j : G),
      HSub.hSub (α := (↑A : Type u_1))
              ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                    (a : (↑A : Type u_1)) → (↑A : Type u_1))
                  (f (h, j)) :
                (↑A : Type u_1))
              (f (g * h, j)) +
            f (g, h * j) -
          f (g, h) =
        0

Tactic:
simp_rw [funext_iff, d₂₃_hom_apply, Prod.forall]

Premises used: groupCohomology.d₂₃_hom_apply, funext_iff, Prod.forall
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : G × G → (↑A : Type u_1)
⊢ (∀ (a a_1 b : G),
      HSub.hSub (α := (↑A : Type u_1))
              ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) a : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                    (a : (↑A : Type u_1)) → (↑A : Type u_1))
                  (f (a_1, b)) :
                (↑A : Type u_1))
              (f (a * a_1, b)) +
            f (a, a_1 * b) -
          f (a, a_1) =
        0 (a, a_1, b)) ↔
    ∀ (g h j : G),
      HSub.hSub (α := (↑A : Type u_1))
              ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
                    (a : (↑A : Type u_1)) → (↑A : Type u_1))
                  (f (h, j)) :
                (↑A : Type u_1))
              (f (g * h, j)) +
            f (g, h * j) -
          f (g, h) =
        0

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : ↥(cocycles₂ A)
g : G
⊢ HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      (((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) 1 : (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G × G) → (↑A : Type u_1)) (1, g) : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (1, 1 * g) : (↑A : Type u_1)) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (HMul.hMul (α := G) 1 1, g) : (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (1, 1) : (↑A : Type u_1))

Tactic:
have := ((mem_cocycles₂_iff f).1 f.2 1 1 g).symm
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : ↥(cocycles₂ A)
g : G
this :
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      (((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) 1 : (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G × G) → (↑A : Type u_1)) (1, g) : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (1, 1 * g) : (↑A : Type u_1)) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (HMul.hMul (α := G) 1 1, g) : (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (1, 1) : (↑A : Type u_1))
⊢ Eq.{u_1 + 1} (α := (↑A : Type u_1)) ((f : (a : G × G) → (↑A : Type u_1)) (1, g) : (↑A : Type u_1))
    ((f : (a : G × G) → (↑A : Type u_1)) (1, 1) : (↑A : Type u_1))

Tactic:
simpa only [map_one, Module.End.one_apply, one_mul, add_right_inj, this]

Premises used: Module.End.one_apply, map_one, add_right_inj, one_mul
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : ↥(cocycles₂ A)
g : G
⊢ HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g * 1, 1) : (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, 1) : (↑A : Type u_1)) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G × G) → (↑A : Type u_1)) (1, 1) : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, HMul.hMul (α := G) 1 1) : (↑A : Type u_1))

Tactic:
have := (mem_cocycles₂_iff f).1 f.2 g 1 1
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : ↥(cocycles₂ A)
g : G
this :
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g * 1, 1) : (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, 1) : (↑A : Type u_1)) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G × G) → (↑A : Type u_1)) (1, 1) : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, HMul.hMul (α := G) 1 1) : (↑A : Type u_1))
⊢ Eq.{u_1 + 1} (α := (↑A : Type u_1)) ((f : (a : G × G) → (↑A : Type u_1)) (g, 1) : (↑A : Type u_1))
    ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
          (a : (↑A : Type u_1)) → (↑A : Type u_1))
        ((f : (a : G × G) → (↑A : Type u_1)) (1, 1) : (↑A : Type u_1)) :
      (↑A : Type u_1))

Tactic:
simpa only [mul_one, add_left_inj, this]

Premises used: add_left_inj, mul_one
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : ↥(cocycles₂ A)
g : G
⊢ HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g * g⁻¹, g) : (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, g⁻¹) : (↑A : Type u_1)) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G × G) → (↑A : Type u_1)) (g⁻¹, g) : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, g⁻¹ * g) : (↑A : Type u_1))

Tactic:
have := (mem_cocycles₂_iff f).1 f.2 g g⁻¹ g
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : ↥(cocycles₂ A)
g : G
this :
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g * g⁻¹, g) : (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, g⁻¹) : (↑A : Type u_1)) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G × G) → (↑A : Type u_1)) (g⁻¹, g) : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, g⁻¹ * g) : (↑A : Type u_1))
⊢ HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G × G) → (↑A : Type u_1)) (1, 1) : (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, g⁻¹) : (↑A : Type u_1)) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G × G) → (↑A : Type u_1)) (g⁻¹, g) : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, 1) : (↑A : Type u_1))

Tactic:
simp only [mul_inv_cancel, inv_mul_cancel, cocycles₂_map_one_fst _ g]
    at this

Premises used: inv_mul_cancel, groupCohomology.cocycles₂_map_one_fst, mul_inv_cancel
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : ↥(cocycles₂ A)
g : G
this :
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G × G) → (↑A : Type u_1)) (1, 1) : (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, g⁻¹) : (↑A : Type u_1)) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G × G) → (↑A : Type u_1)) (g⁻¹, g) : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, 1) : (↑A : Type u_1))
⊢ HSub.hSub (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G × G) → (↑A : Type u_1)) (g⁻¹, g) : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, g⁻¹) : (↑A : Type u_1)) =
    HSub.hSub (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (1, 1) : (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, 1) : (↑A : Type u_1))

Tactic:
sub_eq_sub_iff_add_eq_add.2 this.symm

Premises used: Iff.mpr, sub_eq_sub_iff_add_eq_add, Eq.symm
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
f : ↥(cocycles₂ A)
g : G
this :
  HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1)) ((f : (a : G × G) → (↑A : Type u_1)) (1, 1) : (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, g⁻¹) : (↑A : Type u_1)) =
    HAdd.hAdd (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G × G) → (↑A : Type u_1)) (g⁻¹, g) : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, 1) : (↑A : Type u_1))
⊢ HSub.hSub (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((((A.ρ : (a : G) → (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) g : (↑A : Type u_1) →ₗ[k] (↑A : Type u_1)) :
            (a : (↑A : Type u_1)) → (↑A : Type u_1))
          ((f : (a : G × G) → (↑A : Type u_1)) (g⁻¹, g) : (↑A : Type u_1)) :
        (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, g⁻¹) : (↑A : Type u_1)) =
    HSub.hSub (α := (↑A : Type u_1)) (β := (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (1, 1) : (↑A : Type u_1))
      ((f : (a : G × G) → (↑A : Type u_1)) (g, 1) : (↑A : Type u_1))

Tactic:
exact sub_eq_sub_iff_add_eq_add.2 this.symm

Premises used: Iff.mpr, sub_eq_sub_iff_add_eq_add, Eq.symm
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
x : G → (↑A : Type u_1)
⊢ Membership.mem (α := (↑(ModuleCat.of k (G × G → (↑A : Type u_1))) : Type (max u u_1))) (cocycles₂ A)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u u_1)) →ₗ[k] (↑x2 : Type (max u u_1)))
            (CC := ModuleCat.carrier) (d₁₂ A) :
          (a : (↑(ModuleCat.of k (G → (↑A : Type u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G × G → (↑A : Type u_1))) : Type (max u u_1)))
        x :
      (↑(ModuleCat.of k (G × G → (↑A : Type u_1))) : Type (max u u_1)))

Tactic:
d₁₂_comp_d₂₃_apply _ _

Premises used: groupCohomology.d₁₂_comp_d₂₃_apply, Set.Mem, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep.{u_1, u, u} k G
x : ↥(cocycles₂ A)
⊢ Eq (α := (↑(ModuleCat.of k (G × G × G → (↑A : Type u_1))) : Type (max u u_1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type (max u u_1)) →ₗ[k] (↑x2 : Type (max u u_1)))
            (CC := ModuleCat.carrier) (d₂₃ A) :
          (a : (↑(ModuleCat.of k (G × G → (↑A : Type u_1))) : Type (max u u_1))) →
            (↑(ModuleCat.of k (G × G × G → (↑A : Type u_1))) : Type (max u u_1)))
        (⇑x : (a : G × G) → (↑A : Type u_1)) :
      (↑(ModuleCat.of k (G × G × G → (↑A : Type u_1))) : Type (max u u_1)))
    (0 : (↑(ModuleCat.of k (G × G × G → (↑A : Type u_1))) : Type (max u u_1)))

Tactic:
x.2

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, Subtype.property
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
f : G → (↑A : Type (max u u_1))
hf : f ∈ coboundaries₁.{u, u_1} A
⊢ (⇑(Subtype.mk (p := fun (x : G → (↑A : Type (max u u_1))) ↦ x ∈ coboundaries₁.{u, u_1} A) f hf) :
      (a : G) → (↑A : Type (max u u_1))) =
    f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
f : ↥(coboundaries₁.{u, u_1} A)
⊢ (↑f : G → (↑A : Type (max u u_1))) = (⇑f : (a : G) → (↑A : Type (max u u_1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
f₁ f₂ : ↥(coboundaries₁.{u, u_1} A)
h :
  ∀ (g : G),
    Eq (α := (↑A : Type (max u u_1))) ((f₁ : (a : G) → (↑A : Type (max u u_1))) g : (↑A : Type (max u u_1)))
      ((f₂ : (a : G) → (↑A : Type (max u u_1))) g : (↑A : Type (max u u_1)))
⊢ f₁ = f₂

Tactic:
DFunLike.ext f₁ f₂ h

Premises used: DFunLike.ext
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))
⊢ Membership.mem (α := G → (↑A : Type (max u u_1))) (cocycles₁ A)
    ((ModuleCat.Hom.hom (d₀₁.{u, u_1} A) :
          (a : (↑(ModuleCat.of k (↑A : Type (max u u_1))) : Type (max u u_1))) → G → (↑A : Type (max u u_1)))
        x :
      G → (↑A : Type (max u u_1)))

Tactic:
d₀₁_apply_mem_cocycles₁ x

Premises used: Set.Mem, groupCohomology.d₀₁_apply_mem_cocycles₁