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 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:
exact d₀₁_apply_mem_cocycles₁ x

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

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, Set.range, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
simp_rw :
  Eq (α := Submodule k (G → (↑A : Type (max u u_1))))
    (LinearMap.range (R := k) (M := (↑A : Type (max u u_1))) (τ₁₂ := RingHom.id k) (ModuleCat.Hom.hom 0) :
      Submodule k (G → (↑A : Type (max u u_1))))
    (⊥ : Submodule k (G → (↑A : Type (max u u_1))))
⊢ coboundaries₁.{u, u_1} A = ⊥

Tactic:
simp_rw [coboundaries₁, d₀₁_eq_zero]

Premises used: groupCohomology.coboundaries₁, groupCohomology.d₀₁_eq_zero
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
⊢ Eq (α := Submodule k (G → (↑A : Type (max u u_1))))
    (LinearMap.range (R := k) (M := (↑A : Type (max u u_1))) (τ₁₂ := RingHom.id k) (ModuleCat.Hom.hom 0) :
      Submodule k (G → (↑A : Type (max u u_1))))
    (⊥ : Submodule k (G → (↑A : Type (max u u_1))))

Tactic:
LinearMap.range_eq_bot.2 rfl

Premises used: Iff.mpr, LinearMap.range_eq_bot, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
inst_2 : A.IsTrivial
⊢ Eq (α := Submodule k (G → (↑A : Type (max u u_1))))
    (LinearMap.range (R := k) (M := (↑A : Type (max u u_1))) (τ₁₂ := RingHom.id k) (ModuleCat.Hom.hom 0) :
      Submodule k (G → (↑A : Type (max u u_1))))
    (⊥ : Submodule k (G → (↑A : Type (max u u_1))))

Tactic:
exact LinearMap.range_eq_bot.2 rfl

Premises used: Iff.mpr, LinearMap.range_eq_bot, 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 : G × G → (↑A : Type u_1)
hf : f ∈ coboundaries₂ A
⊢ (⇑(Subtype.mk (p := fun (x : G × G → (↑A : Type u_1)) ↦ x ∈ coboundaries₂ 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 : ↥(coboundaries₂ 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₂ : ↥(coboundaries₂ 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
x : (↑(ModuleCat.of k (G → (↑A : Type u_1))) : Type (max u u_1))
⊢ Membership.mem (α := G × G → (↑A : Type u_1)) (cocycles₂ A)
    ((ModuleCat.Hom.hom (d₁₂ A) :
          (a : (↑(ModuleCat.of k (G → (↑A : Type u_1))) : Type (max u u_1))) → G × G → (↑A : Type u_1))
        x :
      G × G → (↑A : Type u_1))

Tactic:
d₁₂_apply_mem_cocycles₂ x

Premises used: Set.Mem, groupCohomology.d₁₂_apply_mem_cocycles₂
-- 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 : (↑(ModuleCat.of k (G → (↑A : Type u_1))) : Type (max u u_1))
⊢ Membership.mem (α := G × G → (↑A : Type u_1)) (cocycles₂ A)
    ((ModuleCat.Hom.hom (d₁₂ A) :
          (a : (↑(ModuleCat.of k (G → (↑A : Type u_1))) : Type (max u u_1))) → G × G → (↑A : Type u_1))
        x :
      G × G → (↑A : Type u_1))

Tactic:
exact d₁₂_apply_mem_cocycles₂ x

Premises used: groupCohomology.d₁₂_apply_mem_cocycles₂
-- 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 : ↥(coboundaries₂ A)
⊢ (⇑((coboundariesToCocycles₂ A : (a : ↥(coboundaries₂ A)) → ↥(cocycles₂ A)) x : ↥(cocycles₂ A)) :
      (a : G × G) → (↑A : Type u_1)) =
    (↑x : G × G → (↑A : Type u_1))

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, Set.range, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Monoid G
inst_1 : AddCommGroup A
inst_2 : MulAction G A
f : G → A
hf : IsCocycle₁ f
⊢ f 1 = 0

Tactic:
simpa only [mul_one, one_smul, left_eq_add] using hf 1 1

Premises used: left_eq_add, one_smul, mul_one, OfNat.ofNat
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Monoid G
inst_1 : AddCommGroup A
inst_2 : MulAction G A
f : G × G → A
hf : IsCocycle₂ f
g : G
⊢ f (1, g) = f (1, 1)

Tactic:
simpa only [one_smul, one_mul, mul_one, add_right_inj] using (hf 1 1 g).symm

Premises used: one_smul, mul_one, OfNat.ofNat, Eq.symm, add_right_inj, one_mul
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Monoid G
inst_1 : AddCommGroup A
inst_2 : MulAction G A
f : G × G → A
hf : IsCocycle₂ f
g : G
⊢ f (g, 1) = g • f (1, 1)

Tactic:
simpa only [mul_one, add_left_inj] using hf g 1 1

Premises used: add_left_inj, mul_one, OfNat.ofNat
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : MulAction G A
f : G → A
hf : IsCocycle₁ f
g : G
rw : g • f g⁻¹ + f g = 0
rw₁ : g • f g⁻¹ + f g = f 1
rw₂ : g • f g⁻¹ + f g = f (g * g⁻¹)
rw₃ rw₄ : g • f g⁻¹ + f g = g • f g⁻¹ + f g
⊢ g • f g⁻¹ = -f g

Tactic:
rw [← add_eq_zero_iff_eq_neg, ← map_one_of_isCocycle₁ hf, ← mul_inv_cancel g, hf g g⁻¹]

Premises used: groupCohomology.map_one_of_isCocycle₁, add_eq_zero_iff_eq_neg, Inv.inv, mul_inv_cancel
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : MulAction G A
f : G × G → A
hf : IsCocycle₂ f
g : G
⊢ f (g * g⁻¹, g) + f (g, g⁻¹) = g • f (g⁻¹, g) + f (g, g⁻¹ * g)

Tactic:
have := hf g g⁻¹ g
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : MulAction G A
f : G × G → A
hf : IsCocycle₂ f
g : G
this : f (g * g⁻¹, g) + f (g, g⁻¹) = g • f (g⁻¹, g) + f (g, g⁻¹ * g)
⊢ f (1, 1) + f (g, g⁻¹) = g • f (g⁻¹, g) + f (g, 1)

Tactic:
simp only [mul_inv_cancel, inv_mul_cancel, map_one_fst_of_isCocycle₂ hf g] at this

Premises used: inv_mul_cancel, mul_inv_cancel, groupCohomology.map_one_fst_of_isCocycle₂
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : MulAction G A
f : G × G → A
hf : IsCocycle₂ f
g : G
this : f (1, 1) + f (g, g⁻¹) = g • f (g⁻¹, g) + f (g, 1)
⊢ g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 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:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : MulAction G A
f : G × G → A
hf : IsCocycle₂ f
g : G
this : f (1, 1) + f (g, g⁻¹) = g • f (g⁻¹, g) + f (g, 1)
⊢ g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 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 A : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
f : G → A
hf :
  Membership.mem (γ := Submodule k (G → (↑(Rep.ofDistribMulAction k G A) : Type u)))
    (cocycles₁ (Rep.ofDistribMulAction k G A)) f
⊢ IsCocycle₁ f

Tactic:
fun _ _ => (mem_cocycles₁_iff (A := Rep.ofDistribMulAction k G A) f).1 hf _ _

Premises used: groupCohomology.IsCocycle₁, groupCohomology.mem_cocycles₁_iff, Iff.mp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G A : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
f : G → A
hf :
  Membership.mem (γ := Submodule k (G → (↑(Rep.ofDistribMulAction k G A) : Type u)))
    (coboundaries₁ (Rep.ofDistribMulAction k G A)) f
rcases :
  ∀ (a : (↑(ModuleCat.of k (↑(Rep.ofDistribMulAction k G A) : Type u)) : Type u)),
    IsCoboundary₁.{u, u} (G := G) (A := A)
      ((ModuleCat.Hom.hom (d₀₁ (Rep.ofDistribMulAction k G A)) :
          (a : (↑(ModuleCat.of k (↑(Rep.ofDistribMulAction k G A) : Type u)) : Type u)) →
            G → (↑(Rep.ofDistribMulAction k G A) : Type u))
        a)
⊢ IsCoboundary₁ f

Tactic:
rcases hf with ⟨a, rfl⟩

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G A : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
a : (↑(ModuleCat.of k (↑(Rep.ofDistribMulAction k G A) : Type u)) : Type u)
⊢ IsCoboundary₁.{u, u} (G := G) (A := A)
    ((ModuleCat.Hom.hom (d₀₁ (Rep.ofDistribMulAction k G A)) :
        (a : (↑(ModuleCat.of k (↑(Rep.ofDistribMulAction k G A) : Type u)) : Type u)) →
          G → (↑(Rep.ofDistribMulAction k G A) : Type u))
      a)

Tactic:
⟨a, fun _ => rfl⟩

Premises used: groupCohomology.IsCoboundary₁, Exists.intro, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G A : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
a : (↑(ModuleCat.of k (↑(Rep.ofDistribMulAction k G A) : Type u)) : Type u)
⊢ IsCoboundary₁.{u, u} (G := G) (A := A)
    ((ModuleCat.Hom.hom (d₀₁ (Rep.ofDistribMulAction k G A)) :
        (a : (↑(ModuleCat.of k (↑(Rep.ofDistribMulAction k G A) : Type u)) : Type u)) →
          G → (↑(Rep.ofDistribMulAction k G A) : Type u))
      a)

Tactic:
exact ⟨a, fun _ => rfl⟩
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G A : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
f : G × G → A
hf :
  Membership.mem (γ := Submodule k (G × G → (↑(Rep.ofDistribMulAction k G A) : Type u)))
    (cocycles₂ (Rep.ofDistribMulAction k G A)) f
⊢ IsCocycle₂ f

Tactic:
(mem_cocycles₂_iff (A := Rep.ofDistribMulAction k G A) f).1 hf

Premises used: groupCohomology.mem_cocycles₂_iff, Iff.mp, groupCohomology.IsCocycle₂
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G A : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
f : G × G → A
hf :
  Membership.mem (γ := Submodule k (G × G → (↑(Rep.ofDistribMulAction k G A) : Type u)))
    (coboundaries₂ (Rep.ofDistribMulAction k G A)) f
rcases :
  ∀ (a : (↑(ModuleCat.of k (G → (↑(Rep.ofDistribMulAction k G A) : Type u))) : Type u)),
    IsCoboundary₂.{u, u} (G := G) (A := A)
      ((ModuleCat.Hom.hom (d₁₂ (Rep.ofDistribMulAction k G A)) :
          (a : (↑(ModuleCat.of k (G → (↑(Rep.ofDistribMulAction k G A) : Type u))) : Type u)) →
            G × G → (↑(Rep.ofDistribMulAction k G A) : Type u))
        a)
⊢ IsCoboundary₂ f

Tactic:
rcases hf with ⟨a, rfl⟩

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G A : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
a : (↑(ModuleCat.of k (G → (↑(Rep.ofDistribMulAction k G A) : Type u))) : Type u)
⊢ IsCoboundary₂.{u, u} (G := G) (A := A)
    ((ModuleCat.Hom.hom (d₁₂ (Rep.ofDistribMulAction k G A)) :
        (a : (↑(ModuleCat.of k (G → (↑(Rep.ofDistribMulAction k G A) : Type u))) : Type u)) →
          G × G → (↑(Rep.ofDistribMulAction k G A) : Type u))
      a)

Tactic:
⟨a, fun _ _ => rfl⟩

Premises used: Exists.intro, groupCohomology.IsCoboundary₂, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G A : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : AddCommGroup A
inst_3 : Module k A
inst_4 : DistribMulAction G A
inst_5 : SMulCommClass G k A
a : (↑(ModuleCat.of k (G → (↑(Rep.ofDistribMulAction k G A) : Type u))) : Type u)
⊢ IsCoboundary₂.{u, u} (G := G) (A := A)
    ((ModuleCat.Hom.hom (d₁₂ (Rep.ofDistribMulAction k G A)) :
        (a : (↑(ModuleCat.of k (G → (↑(Rep.ofDistribMulAction k G A) : Type u))) : Type u)) →
          G × G → (↑(Rep.ofDistribMulAction k G A) : Type u))
      a)

Tactic:
exact ⟨a, fun _ _ => rfl⟩
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G : Type u_1
M : Type u_2
inst : Monoid G
inst_1 : CommGroup M
inst_2 : MulAction G M
f : G → M
hf : IsMulCocycle₁ f
⊢ f 1 = 1

Tactic:
simpa only [mul_one, one_smul, left_eq_mul] using hf 1 1

Premises used: one_smul, left_eq_mul, mul_one, OfNat.ofNat
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G : Type u_1
M : Type u_2
inst : Monoid G
inst_1 : CommGroup M
inst_2 : MulAction G M
f : G × G → M
hf : IsMulCocycle₂ f
g : G
⊢ f (1, g) = f (1, 1)

Tactic:
simpa only [one_smul, one_mul, mul_one, mul_right_inj] using (hf 1 1 g).symm

Premises used: one_smul, mul_right_inj, mul_one, OfNat.ofNat, Eq.symm, one_mul
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G : Type u_1
M : Type u_2
inst : Monoid G
inst_1 : CommGroup M
inst_2 : MulAction G M
f : G × G → M
hf : IsMulCocycle₂ f
g : G
⊢ f (g, 1) = g • f (1, 1)

Tactic:
simpa only [mul_one, mul_left_inj] using hf g 1 1

Premises used: mul_left_inj, mul_one, OfNat.ofNat
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : CommGroup M
inst_2 : MulAction G M
f : G → M
hf : IsMulCocycle₁ f
g : G
rw : g • f g⁻¹ * f g = 1
rw₁ : g • f g⁻¹ * f g = f 1
rw₂ : g • f g⁻¹ * f g = f (g * g⁻¹)
rw₃ rw₄ : g • f g⁻¹ * f g = g • f g⁻¹ * f g
⊢ g • f g⁻¹ = (f g)⁻¹

Tactic:
rw [← mul_eq_one_iff_eq_inv, ← map_one_of_isMulCocycle₁ hf, ← mul_inv_cancel g, hf g g⁻¹]

Premises used: groupCohomology.map_one_of_isMulCocycle₁, mul_eq_one_iff_eq_inv, Inv.inv, mul_inv_cancel
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : CommGroup M
inst_2 : MulAction G M
f : G × G → M
hf : IsMulCocycle₂ f
g : G
⊢ f (g * g⁻¹, g) * f (g, g⁻¹) = g • f (g⁻¹, g) * f (g, g⁻¹ * g)

Tactic:
have := hf g g⁻¹ g
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : CommGroup M
inst_2 : MulAction G M
f : G × G → M
hf : IsMulCocycle₂ f
g : G
this : f (g * g⁻¹, g) * f (g, g⁻¹) = g • f (g⁻¹, g) * f (g, g⁻¹ * g)
⊢ f (1, 1) * f (g, g⁻¹) = g • f (g⁻¹, g) * f (g, 1)

Tactic:
simp only [mul_inv_cancel, inv_mul_cancel, map_one_fst_of_isMulCocycle₂ hf g] at this

Premises used: inv_mul_cancel, groupCohomology.map_one_fst_of_isMulCocycle₂, mul_inv_cancel
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : CommGroup M
inst_2 : MulAction G M
f : G × G → M
hf : IsMulCocycle₂ f
g : G
this : f (1, 1) * f (g, g⁻¹) = g • f (g⁻¹, g) * f (g, 1)
⊢ g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)

Tactic:
div_eq_div_iff_mul_eq_mul.2 this.symm

Premises used: Iff.mpr, div_eq_div_iff_mul_eq_mul, Eq.symm
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G : Type u_1
M : Type u_2
inst : Group G
inst_1 : CommGroup M
inst_2 : MulAction G M
f : G × G → M
hf : IsMulCocycle₂ f
g : G
this : f (1, 1) * f (g, g⁻¹) = g • f (g⁻¹, g) * f (g, 1)
⊢ g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)

Tactic:
exact div_eq_div_iff_mul_eq_mul.2 this.symm

Premises used: Iff.mpr, div_eq_div_iff_mul_eq_mul, Eq.symm
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G M : Type
inst : Group G
inst_1 : CommGroup M
inst_2 : MulDistribMulAction G M
f : G → M
hf :
  Membership.mem (γ := Submodule ℤ (G → (↑(Rep.ofMulDistribMulAction G M) : Type)))
    (cocycles₁ (Rep.ofMulDistribMulAction G M)) f
⊢ IsMulCocycle₁ (M := M) ((⇑Additive.toMul : (a : Additive M) → M) ∘ f)

Tactic:
(mem_cocycles₁_iff (A := Rep.ofMulDistribMulAction G M) f).1 hf

Premises used: Additive, groupCohomology.IsMulCocycle₁, groupCohomology.mem_cocycles₁_iff, Iff.mp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G M : Type
inst : Group G
inst_1 : CommGroup M
inst_2 : MulDistribMulAction G M
f : G → M
hf :
  Membership.mem (γ := Submodule ℤ (G → (↑(Rep.ofMulDistribMulAction G M) : Type)))
    (coboundaries₁ (Rep.ofMulDistribMulAction G M)) f
rcases :
  ∀ (x : (↑(ModuleCat.of ℤ (↑(Rep.ofMulDistribMulAction G M) : Type)) : Type)),
    IsMulCoboundary₁ (G := G) (M := M)
      (Function.comp (β := M) (⇑Additive.ofMul : (a : M) → Additive M)
        ((ModuleCat.Hom.hom (d₀₁ (Rep.ofMulDistribMulAction G M)) :
            (a : (↑(ModuleCat.of ℤ (↑(Rep.ofMulDistribMulAction G M) : Type)) : Type)) →
              G → (↑(Rep.ofMulDistribMulAction G M) : Type))
          x))
⊢ IsMulCoboundary₁ (M := M) ((⇑Additive.ofMul : (a : M) → Additive M) ∘ f)

Tactic:
rcases hf with ⟨x, rfl⟩

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G M : Type
inst : Group G
inst_1 : CommGroup M
inst_2 : MulDistribMulAction G M
x : (↑(ModuleCat.of ℤ (↑(Rep.ofMulDistribMulAction G M) : Type)) : Type)
⊢ IsMulCoboundary₁ (G := G) (M := M)
    (Function.comp (β := M) (⇑Additive.ofMul : (a : M) → Additive M)
      ((ModuleCat.Hom.hom (d₀₁ (Rep.ofMulDistribMulAction G M)) :
          (a : (↑(ModuleCat.of ℤ (↑(Rep.ofMulDistribMulAction G M) : Type)) : Type)) →
            G → (↑(Rep.ofMulDistribMulAction G M) : Type))
        x))

Tactic:
⟨x, fun _ =>  rfl⟩

Premises used: groupCohomology.IsMulCoboundary₁, Exists.intro, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G M : Type
inst : Group G
inst_1 : CommGroup M
inst_2 : MulDistribMulAction G M
x : (↑(ModuleCat.of ℤ (↑(Rep.ofMulDistribMulAction G M) : Type)) : Type)
⊢ IsMulCoboundary₁ (G := G) (M := M)
    (Function.comp (β := M) (⇑Additive.ofMul : (a : M) → Additive M)
      ((ModuleCat.Hom.hom (d₀₁ (Rep.ofMulDistribMulAction G M)) :
          (a : (↑(ModuleCat.of ℤ (↑(Rep.ofMulDistribMulAction G M) : Type)) : Type)) →
            G → (↑(Rep.ofMulDistribMulAction G M) : Type))
        x))

Tactic:
exact ⟨x, fun _ =>  rfl⟩
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G M : Type
inst : Group G
inst_1 : CommGroup M
inst_2 : MulDistribMulAction G M
f : G × G → M
hf :
  Membership.mem (γ := Submodule ℤ (G × G → (↑(Rep.ofMulDistribMulAction G M) : Type)))
    (cocycles₂ (Rep.ofMulDistribMulAction G M)) f
⊢ IsMulCocycle₂ (M := M) ((⇑Additive.toMul : (a : Additive M) → M) ∘ f)

Tactic:
(mem_cocycles₂_iff (A := Rep.ofMulDistribMulAction G M) f).1 hf

Premises used: Additive, groupCohomology.mem_cocycles₂_iff, groupCohomology.IsMulCocycle₂, Iff.mp
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G M : Type
inst : Group G
inst_1 : CommGroup M
inst_2 : MulDistribMulAction G M
f : G × G → M
hf :
  Membership.mem (γ := Submodule ℤ (G × G → (↑(Rep.ofMulDistribMulAction G M) : Type)))
    (coboundaries₂ (Rep.ofMulDistribMulAction G M)) f
rcases :
  ∀ (x : (↑(ModuleCat.of ℤ (G → (↑(Rep.ofMulDistribMulAction G M) : Type))) : Type)),
    IsMulCoboundary₂ (G := G) (M := M)
      (Function.comp (β := Additive M) (⇑Additive.toMul : (a : Additive M) → M)
        ((ModuleCat.Hom.hom (d₁₂ (Rep.ofMulDistribMulAction G M)) :
            (a : (↑(ModuleCat.of ℤ (G → (↑(Rep.ofMulDistribMulAction G M) : Type))) : Type)) →
              G × G → (↑(Rep.ofMulDistribMulAction G M) : Type))
          x))
⊢ IsMulCoboundary₂ (M := M) ((⇑Additive.toMul : (a : Additive M) → M) ∘ f)

Tactic:
rcases hf with ⟨x, rfl⟩

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G M : Type
inst : Group G
inst_1 : CommGroup M
inst_2 : MulDistribMulAction G M
x : (↑(ModuleCat.of ℤ (G → (↑(Rep.ofMulDistribMulAction G M) : Type))) : Type)
⊢ IsMulCoboundary₂ (G := G) (M := M)
    (Function.comp (β := Additive M) (⇑Additive.toMul : (a : Additive M) → M)
      ((ModuleCat.Hom.hom (d₁₂ (Rep.ofMulDistribMulAction G M)) :
          (a : (↑(ModuleCat.of ℤ (G → (↑(Rep.ofMulDistribMulAction G M) : Type))) : Type)) →
            G × G → (↑(Rep.ofMulDistribMulAction G M) : Type))
        x))

Tactic:
⟨x, fun _ _ => rfl⟩

Premises used: Exists.intro, groupCohomology.IsMulCoboundary₂, rfl
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
G M : Type
inst : Group G
inst_1 : CommGroup M
inst_2 : MulDistribMulAction G M
x : (↑(ModuleCat.of ℤ (G → (↑(Rep.ofMulDistribMulAction G M) : Type))) : Type)
⊢ IsMulCoboundary₂ (G := G) (M := M)
    (Function.comp (β := Additive M) (⇑Additive.toMul : (a : Additive M) → M)
      ((ModuleCat.Hom.hom (d₁₂ (Rep.ofMulDistribMulAction G M)) :
          (a : (↑(ModuleCat.of ℤ (G → (↑(Rep.ofMulDistribMulAction G M) : Type))) : Type)) →
            G × G → (↑(Rep.ofMulDistribMulAction G M) : Type))
        x))

Tactic:
exact ⟨x, fun _ _ => rfl⟩
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
rw :
  Function.Injective (α := (↑(shortComplexH0.{u, u_1} A).X₁ : Type (max u u_1))) (β :=
    (↑(shortComplexH0.{u, u_1} A).X₂ : 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) (shortComplexH0.{u, u_1} A).f) :
      (a : (↑(shortComplexH0 A).X₁ : Type (max u u_1))) → (↑(shortComplexH0 A).X₂ : Type (max u u_1)))
⊢ Mono (shortComplexH0.{u, u_1} A).f

Tactic:
rw [ModuleCat.mono_iff_injective]

Premises used: ModuleCat.mono_iff_injective
-- Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
⊢ Function.Injective (α := (↑(shortComplexH0.{u, u_1} A).X₁ : Type (max u u_1))) (β :=
    (↑(shortComplexH0.{u, u_1} A).X₂ : 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) (shortComplexH0.{u, u_1} A).f) :
      (a : (↑(shortComplexH0 A).X₁ : Type (max u u_1))) → (↑(shortComplexH0 A).X₂ : Type (max u u_1)))

Tactic:
apply Submodule.injective_subtype

Premises used: Submodule.injective_subtype