mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Goal state before:
pp: k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
⊢ inhomogeneousChains.d A (n + 1) ≫ inhomogeneousChains.d A n = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
⊢ (inhomogeneousChains A).d (n + 1) n = d A n

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
⊢ d A (n + 1) ≫ d A n = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Goal state before:
pp: k✝ G✝ : Type u
inst✝⁴ : CommRing k✝
inst✝³ : Group G✝
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
n : ℕ
inst✝ : DecidableEq G
⊢ inhomogeneousChains A ≅ HomologicalComplex.coinvariantsTensorObj A (barComplex k G)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
m n : ℕ
h : (ComplexShape.down ℕ).next m = n
f : (Fin m → G) →₀ ↑A
hf : (ConcreteCategory.hom ((inhomogeneousChains A).d m n)) f = 0
⊢ (ConcreteCategory.hom (iCycles A m)) (cyclesMk m n h f hf) = f

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
C : ↑(groupHomology A n) → Prop
x : ↑(groupHomology A n)
h : ∀ (x : ↑(cycles A n)), C ((ConcreteCategory.hom (π A n)) x)
⊢ C x

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (cochainsIso₂ A).hom ≫ d₂₃ A = (inhomogeneousCochains A).d 2 3 ≫ (cochainsIso₃ A).hom

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ d₀₁ A ≫ d₁₂ A = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ d₁₂ A ≫ d₂₃ A = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G → ↑A
⊢ (ModuleCat.Hom.hom (d₁₂ A)) f = 0 ↔ ∀ (g h : G), (A.ρ g) (f h) - f (g * h) + f g = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G → ↑A
⊢ f ∈ cocycles₁ A ↔ ∀ (g h : G), f (g * h) = (A.ρ g) (f h) + f g

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(cocycles₁ A)
⊢ f 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(cocycles₁ A)
g : G
⊢ (A.ρ g) (f g⁻¹) = -f g

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
f : ↥(cocycles₁ A)
g h : G
⊢ f (g * h) = f g + f h

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
f : Additive G →+ ↑A
g h : G
⊢ (⇑f ∘ ⇑Additive.ofMul) (g * h) = (A.ρ g) ((⇑f ∘ ⇑Additive.ofMul) h) + (⇑f ∘ ⇑Additive.ofMul) g

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G × G → ↑A
⊢ (ModuleCat.Hom.hom (d₂₃ A)) f = 0 ↔ ∀ (g h j : G), (A.ρ g) (f (h, j)) - f (g * h, j) + f (g, h * j) - f (g, h) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G × G → ↑A
⊢ f ∈ cocycles₂ A ↔ ∀ (g h j : G), f (g * h, j) + f (g, h) = (A.ρ g) (f (h, j)) + f (g, h * j)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(cocycles₂ A)
g : G
⊢ f (1, g) = f (1, 1)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(cocycles₂ A)
g : G
⊢ f (g, 1) = (A.ρ g) (f (1, 1))

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(cocycles₂ A)
g : G
⊢ (A.ρ g) (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ coboundaries₁ A ≤ cocycles₁ A

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ coboundaries₁ A = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ coboundaries₂ A ≤ cocycles₂ A

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Monoid G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G → A
hf : IsCocycle₁ f
⊢ f 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Monoid G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G × G → A
hf : IsCocycle₂ f
g : G
⊢ f (1, g) = f (1, 1)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Monoid G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G × G → A
hf : IsCocycle₂ f
g : G
⊢ f (g, 1) = g • f (1, 1)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G → A
hf : IsCocycle₁ f
g : G
⊢ g • f g⁻¹ = -f g

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G × G → A
hf : IsCocycle₂ f
g : G
⊢ g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
f : G → A
hf : f ∈ coboundaries₁ (Rep.ofDistribMulAction k G A)
⊢ IsCoboundary₁ f

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
f : G × G → A
hf : f ∈ coboundaries₂ (Rep.ofDistribMulAction k G A)
⊢ IsCoboundary₂ f

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : Monoid G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G → M
hf : IsMulCocycle₁ f
⊢ f 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : Monoid G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G × G → M
hf : IsMulCocycle₂ f
g : G
⊢ f (1, g) = f (1, 1)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : Monoid G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G × G → M
hf : IsMulCocycle₂ f
g : G
⊢ f (g, 1) = g • f (1, 1)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G → M
hf : IsMulCocycle₁ f
g : G
⊢ g • f g⁻¹ = (f g)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G × G → M
hf : IsMulCocycle₂ f
g : G
⊢ g • f (g⁻¹, g) / f (g, g⁻¹) = f (1, 1) / f (g, 1)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G M : Type
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulDistribMulAction G M
f : G → M
hf : f ∈ coboundaries₁ (Rep.ofMulDistribMulAction G M)
⊢ IsMulCoboundary₁ (⇑Additive.ofMul ∘ f)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G M : Type
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulDistribMulAction G M
f : G × G → M
hf : f ∈ coboundaries₂ (Rep.ofMulDistribMulAction G M)
⊢ IsMulCoboundary₂ (⇑Additive.toMul ∘ f)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ Mono (shortComplexH0 A).f

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (shortComplexH0 A).Exact

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (ComplexShape.up ℕ).next 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f = iCocycles A 0 ≫ (cochainsIso₀ A).hom

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (cocyclesIso₀ A).inv ≫ iCocycles A 0 = (shortComplexH0 A).f ≫ (cochainsIso₀ A).inv

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥A.ρ.invariants
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d A 0)) ((ConcreteCategory.hom (cochainsIso₀ A).inv) ↑x) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥A.ρ.invariants
⊢ (ConcreteCategory.hom (iCocycles A 0)) (cocyclesMk ((ConcreteCategory.hom (cochainsIso₀ A).inv) ↑x) ⋯) =
    (ConcreteCategory.hom (iCocycles A 0)) ((ConcreteCategory.hom (cocyclesIso₀ A).inv) x)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (ComplexShape.up ℕ).prev 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (ComplexShape.up ℕ).next 1 = 2

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (isoCocycles₁ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.i = iCocycles A 1 ≫ (cochainsIso₁ A).hom

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ toCocycles A 0 1 ≫ (isoCocycles₁ A).hom = (cochainsIso₀ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.f'

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₁ A)
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d A 1)) ((ConcreteCategory.hom (cochainsIso₁ A).inv) ⇑x) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₁ A)
⊢ cocyclesMk ((ConcreteCategory.hom (cochainsIso₁ A).inv) ⇑x) ⋯ = (ConcreteCategory.hom (isoCocycles₁ A).inv) x

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (ComplexShape.up ℕ).prev 2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (ComplexShape.up ℕ).next 2 = 3

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (isoCocycles₂ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.i = iCocycles A 2 ≫ (cochainsIso₂ A).hom

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ toCocycles A 1 2 ≫ (isoCocycles₂ A).hom = (cochainsIso₁ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.f'

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₂ A)
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d A 2)) ((ConcreteCategory.hom (cochainsIso₂ A).inv) ⇑x) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₂ A)
⊢ cocyclesMk ((ConcreteCategory.hom (cochainsIso₂ A).inv) ⇑x) ⋯ = (ConcreteCategory.hom (isoCocycles₂ A).inv) x

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ π A 0 ≫ (H0Iso A).hom = (cocyclesIso₀ A).hom

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
C : ↑(H0 A) → Prop
x : ↑(H0 A)
h : ∀ (x : ↥A.ρ.invariants), C ((ConcreteCategory.hom (H0Iso A).inv) x)
⊢ C x

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ π A 0 ≫ (H0IsoOfIsTrivial A).hom = iCocycles A 0 ≫ (cochainsIso₀ A).hom

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
x : ↑A
⊢ x ∈ A.ρ.invariants

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₁ A)
⊢ (ConcreteCategory.hom (H1π A)) x = 0 ↔ ⇑x ∈ coboundaries₁ A

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cocycles₁ A)
⊢ (ConcreteCategory.hom (H1π A)) x = (ConcreteCategory.hom (H1π A)) y ↔ ⇑x - ⇑y ∈ coboundaries₁ A

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
C : ↑(H1 A) → Prop
x : ↑(H1 A)
h : ∀ (x : ↥(cocycles₁ A)), C ((ConcreteCategory.hom (H1π A)) x)
y : ↑(cocycles A 1)
⊢ C ((ConcreteCategory.hom (π A 1)) y)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ π A 1 ≫ (H1Iso A).hom = (isoCocycles₁ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.π

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ (inhomogeneousCochains A).d 0 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ H1π A ≫ (H1IsoOfIsTrivial A).hom = (cocycles₁IsoOfIsTrivial A).hom

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
f : ↥(cocycles₁ A)
x : Additive G
⊢ ((ConcreteCategory.hom (H1IsoOfIsTrivial A).hom) ((ConcreteCategory.hom (H1π A)) f)) x = f (Additive.toMul x)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₂ A)
⊢ (ConcreteCategory.hom (H2π A)) x = 0 ↔ ⇑x ∈ coboundaries₂ A

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cocycles₂ A)
⊢ (ConcreteCategory.hom (H2π A)) x = (ConcreteCategory.hom (H2π A)) y ↔ ⇑x - ⇑y ∈ coboundaries₂ A

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
C : ↑(H2 A) → Prop
x : ↑(H2 A)
h : ∀ (x : ↥(cocycles₂ A)), C ((ConcreteCategory.hom (H2π A)) x)
y : ↑(cocycles A 2)
⊢ C ((ConcreteCategory.hom (π A 2)) y)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ π A 2 ≫ (H2Iso A).hom = (isoCocycles₂ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.π

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g✝ : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g✝
j : ℕ
a : ↑A
g : G
hj : Even (j + 1)
⊢ ∀ (i : G), i ∈ Finset.univ ↔ (MulEquiv.inv G) i ∈ Finset.univ

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g✝ : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g✝
j : ℕ
a : ↑A
g : G
hj : Even (j + 1)
⊢ ∀ i ∈ Finset.univ, (A.ρ (i * g⁻¹)) a = (A.ρ (((MulEquiv.inv G) i)⁻¹ * g⁻¹)) a

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g✝ : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g✝
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
a : ↑A
g : G
⊢ (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X i)).compr₂
            (ModuleCat.Hom.hom
              (A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom ≫ (moduleCatChainComplex A g✝).d i j)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1 =
    (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X i)).compr₂
            (ModuleCat.Hom.hom
              ((HomologicalComplex.coinvariantsTensorObj A (resolution k g✝⁻¹ ⋯).complex).d i j ≫
                A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ Coinvariants.ker A.ρ = (Hom.hom (A.applyAsHom g - 𝟙 A)).range

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f₁ f₂ : G →* H
h : f₁ = f₂
φ : res f₁ A ⟶ B
T : Type u_1
F : (f : G →* H) → (res f A ⟶ B) → T
⊢ F f₁ φ = F f₂ (h ▸ φ)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n i j : ℕ
hij : i + 1 = j
⊢ ModuleCat.ofHom ((Hom.hom φ).compLeft (Fin i → G) ∘ₗ LinearMap.funLeft k ↑A fun x ↦ ⇑f ∘ x) ≫
      (inhomogeneousCochains B).d i j =
    (inhomogeneousCochains A).d i j ≫
      ModuleCat.ofHom ((Hom.hom φ).compLeft (Fin j → G) ∘ₗ LinearMap.funLeft k ↑A fun x ↦ ⇑f ∘ x)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k H : Type u
inst✝¹ : CommRing k
inst✝ : Group H
A : Rep k H
⊢ cochainsMap (MonoidHom.id H) (𝟙 A) = 𝟙 (inhomogeneousCochains A)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k K
B : Rep k H
C : Rep k G
f : H →* K
g : G →* H
φ : res f A ⟶ B
ψ : res g B ⟶ C
⊢ cochainsMap (f.comp g) ((resFunctor g).map φ ≫ ψ) = cochainsMap f φ ≫ cochainsMap g ψ

Tactic:
by

Goal state after: