mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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
x✝ : ↑A
⊢ x✝ ∈ A.ρ.invariants ↔ x✝ ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).ker

Tactic:
;

Goal state after:
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
x✝ : ↑A
⊢ x✝ ∈ A.ρ.invariants ↔ x✝ ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).ker
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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 : ℕ
h₀ : NeZero i
hi : Even i
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝

Tactic:
;

Goal state after:
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 : ℕ
h₀ : NeZero i
hi : Even i
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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 : ℕ
h₀ : NeZero i
hi : Even i
⊢ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap = 0

Tactic:
by ext; simp [sub_hom]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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 : ℕ
h₀ : NeZero i
hi : Even i
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝

Tactic:
;

Goal state after:
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 : ℕ
h₀ : NeZero i
hi : Even i
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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 : ℕ
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 ext; simp [sub_hom]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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 : ℕ
inst✝ : NeZero i
hi : Even i
x y : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ ↑(x - y) ∈ (Hom.hom A.norm).range ↔ ↑x - ↑y ∈ (Hom.hom A.norm).range

Tactic:
;

Goal state after:
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 : ℕ
inst✝ : NeZero i
hi : Even i
x y : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ ↑(x - y) ∈ (Hom.hom A.norm).range ↔ ↑x - ↑y ∈ (Hom.hom A.norm).range
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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 : ℕ
hi : Odd i
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝

Tactic:
;

Goal state after:
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 : ℕ
hi : Odd i
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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 : ℕ
hi : Odd i
⊢ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap = 0

Tactic:
by ext; simp [sub_hom]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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 : ℕ
hi : Odd i
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝

Tactic:
;

Goal state after:
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 : ℕ
hi : Odd i
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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 : ℕ
hi : Odd i
⊢ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap = 0

Tactic:
by ext; simp [sub_hom]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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 : ℕ
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev (2 * j + 1)) (2 * j + 1)

Tactic:
;

Goal state after:
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 : ℕ
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev (2 * j + 1)) (2 * j + 1)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : Gal(L/K) → Lˣ
x y : Gal(L/K)
h : (fun f ↦ ↑f) x = (fun f ↦ ↑f) y
a✝ : L
⊢ x a✝ = y a✝

Tactic:
;

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : Gal(L/K) → Lˣ
x y : Gal(L/K)
h : (fun f ↦ ↑f) x = (fun f ↦ ↑f) y
a✝ : L
⊢ x a✝ = y a✝
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
n✝ : SimplexCategoryᵒᵖ
⊢ ((𝟭 (SimplicialObject (Type u))).map (CechNerveTerminalFrom.iso G ≪≫ cechNerveTerminalFromIsoCompForget G).hom ≫
          (compForgetAugmented G).hom).app
      n✝ =
    ((Arrow.mk (terminal.from G)).augmentedCechNerve.hom ≫
          (SimplicialObject.const (Type u)).map
            (Iso.refl (Arrow.mk (terminal.from G)).augmentedCechNerve.right).hom).app
      n✝

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
n✝ : SimplexCategoryᵒᵖ
⊢ ((𝟭 (SimplicialObject (Type u))).map (CechNerveTerminalFrom.iso G ≪≫ cechNerveTerminalFromIsoCompForget G).hom ≫
          (compForgetAugmented G).hom).app
      n✝ =
    ((Arrow.mk (terminal.from G)).augmentedCechNerve.hom ≫
          (SimplicialObject.const (Type u)).map
            (Iso.refl (Arrow.mk (terminal.from G)).augmentedCechNerve.right).hom).app
      n✝
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
f : k[Fin (n + 1 + 1) → G]
⊢ (d k G (n + 1)) f = (d k G (n + 1)) f

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
f : k[Fin (n + 1 + 1) → G]
⊢ (d k G (n + 1)) f = (d k G (n + 1)) f
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: case e_m
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
⊢ (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) = Fin.partialProd i ∘ Fin.succ

Tactic:
;

Goal state after:
case e_m
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
⊢ (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) = Fin.partialProd i ∘ Fin.succ
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i : ℕ
z : (Fin i → G) → ↑X.X₃
y : (Fin i → G) → ↑X.X₂
hy : (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f i)) y = z
hz : (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d i (i + 1))) z = 0
x : (Fin (i + 1) → G) → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d i (i + 1))) y
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d X.X₃ i)) z = 0

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i : ℕ
z : (Fin i → G) → ↑X.X₃
y : (Fin i → G) → ↑X.X₂
hy : (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f i)) y = z
hz : (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d i (i + 1))) z = 0
x : (Fin (i + 1) → G) → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d i (i + 1))) y
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d X.X₃ i)) z = 0
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 : ↑A
g : G
⊢ (A.ρ g) x - x + ((A.ρ g) y - y) = ((fun g ↦ (A.ρ g) x - x) + fun g ↦ (A.ρ g) y - y) g

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↑A
g : G
⊢ (A.ρ g) x - x + ((A.ρ g) y - y) = ((fun g ↦ (A.ρ g) x - x) + fun g ↦ (A.ρ g) y - y) g
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : ↑A
g : G
⊢ (A.ρ g) (r • x) - r • x = r • ((A.ρ g) x - x)

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : ↑A
g : G
⊢ (A.ρ g) (r • x) - r • x = r • ((A.ρ g) x - x)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
⊢ (ModuleCat.Hom.hom (d₀₁ X.X₃ ≫ (cochainsIso₁ X.X₃).inv)) ↑z = 0

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
⊢ (ModuleCat.Hom.hom (d₀₁ X.X₃ ≫ (cochainsIso₁ X.X₃).inv)) ↑z = 0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
g✝ : Fin 0 → G
⊢ (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f 0)) ((ConcreteCategory.hom (cochainsIso₀ X.X₂).inv) y)
      g✝ =
    (ConcreteCategory.hom (cochainsIso₀ X.X₃).inv) (↑z) g✝

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
g✝ : Fin 0 → G
⊢ (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f 0)) ((ConcreteCategory.hom (cochainsIso₀ X.X₂).inv) y)
      g✝ =
    (ConcreteCategory.hom (cochainsIso₀ X.X₃).inv) (↑z) g✝
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 : G → ↑A
g : G × G
⊢ (A.ρ g.1) (x g.2 + y g.2) - (x (g.1 * g.2) + y (g.1 * g.2)) + (x g.1 + y g.1) =
    (A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1 + ((A.ρ g.1) (y g.2) - y (g.1 * g.2) + y g.1)

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : G → ↑A
g : G × G
⊢ (A.ρ g.1) (x g.2 + y g.2) - (x (g.1 * g.2) + y (g.1 * g.2)) + (x g.1 + y g.1) =
    (A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1 + ((A.ρ g.1) (y g.2) - y (g.1 * g.2) + y g.1)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : G → ↑A
g : G × G
⊢ (A.ρ g.1) (r • x g.2) - r • x (g.1 * g.2) + r • x g.1 = r • ((A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1)

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : G → ↑A
g : G × G
⊢ (A.ρ g.1) (r • x g.2) - r • x (g.1 * g.2) + r • x g.1 = r • ((A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
g✝ : Fin 1 → G
⊢ (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f 1)) ((ConcreteCategory.hom (cochainsIso₁ X.X₂).inv) y)
      g✝ =
    (ConcreteCategory.hom (cochainsIso₁ X.X₃).inv) (⇑z) g✝

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
g✝ : Fin 1 → G
⊢ (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f 1)) ((ConcreteCategory.hom (cochainsIso₁ X.X₂).inv) y)
      g✝ =
    (ConcreteCategory.hom (cochainsIso₁ X.X₃).inv) (⇑z) g✝
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : G × G → ↑A
g : G × G × G
⊢ (A.ρ g.1) (r • x (g.2.1, g.2.2)) - r • x (g.1 * g.2.1, g.2.2) + r • x (g.1, g.2.1 * g.2.2) - r • x (g.1, g.2.1) =
    r • ((A.ρ g.1) (x (g.2.1, g.2.2)) - x (g.1 * g.2.1, g.2.2) + x (g.1, g.2.1 * g.2.2) - x (g.1, g.2.1))

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : G × G → ↑A
g : G × G × G
⊢ (A.ρ g.1) (r • x (g.2.1, g.2.2)) - r • x (g.1 * g.2.1, g.2.2) + r • x (g.1, g.2.1 * g.2.2) - r • x (g.1, g.2.1) =
    r • ((A.ρ g.1) (x (g.2.1, g.2.2)) - x (g.1 * g.2.1, g.2.2) + x (g.1, g.2.1 * g.2.2) - x (g.1, g.2.1))
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
S : Subgroup G
A✝ : Rep.{?u.12, u, u} k ↥S
P : ProjectiveResolution (Rep.trivial k G k)
A : Rep.{u, u, u} k ↥S
x✝⁴ x✝³ : ℕ
x✝² : (ComplexShape.up ℕ).Rel x✝⁴ x✝³
f : ↑((((resFunctor S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A).X x✝⁴)
x✝¹ : ↑(Opposite.unop (Opposite.op (P.complex.X x✝³)))
x✝ : G
⊢ ↑((Hom.hom
              ((ModuleCat.Hom.hom
                  ((resCoindHomEquiv.{u, u, u, u} S.subtype (P.complex.X x✝⁴) A).toModuleIso.hom ≫
                    (P.complex.linearYonedaObj k (coind.{u, u, u, u} S.subtype A)).d x✝⁴ x✝³))
                f)).toLinearMap
          x✝¹)
      x✝ =
    ↑((Hom.hom
              ((ModuleCat.Hom.hom
                  ((((resFunctor S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A).d x✝⁴ x✝³ ≫
                    (resCoindHomEquiv.{u, u, u, u} S.subtype (P.complex.X x✝³) A).toModuleIso.hom))
                f)).toLinearMap
          x✝¹)
      x✝

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
S : Subgroup G
A✝ : Rep.{?u.12, u, u} k ↥S
P : ProjectiveResolution (Rep.trivial k G k)
A : Rep.{u, u, u} k ↥S
x✝⁴ x✝³ : ℕ
x✝² : (ComplexShape.up ℕ).Rel x✝⁴ x✝³
f : ↑((((resFunctor S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A).X x✝⁴)
x✝¹ : ↑(Opposite.unop (Opposite.op (P.complex.X x✝³)))
x✝ : G
⊢ ↑((Hom.hom
              ((ModuleCat.Hom.hom
                  ((resCoindHomEquiv.{u, u, u, u} S.subtype (P.complex.X x✝⁴) A).toModuleIso.hom ≫
                    (P.complex.linearYonedaObj k (coind.{u, u, u, u} S.subtype A)).d x✝⁴ x✝³))
                f)).toLinearMap
          x✝¹)
      x✝ =
    ↑((Hom.hom
              ((ModuleCat.Hom.hom
                  ((((resFunctor S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A).d x✝⁴ x✝³ ≫
                    (resCoindHomEquiv.{u, u, u, u} S.subtype (P.complex.X x✝³) A).toModuleIso.hom))
                f)).toLinearMap
          x✝¹)
      x✝
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:
have := (mem_cocycles₁_def f).1 f.2 1 1

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(cocycles₁ A)
this : (A.ρ 1) (f 1) - f (1 * 1) + f 1 = 0
⊢ f 1 = 0
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
g : Fin (0 + 1) → G
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d A 0)) ((ConcreteCategory.hom (cochainsIso₀ A).inv) ↑x) g = 0 g

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥A.ρ.invariants
g : Fin (0 + 1) → G
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d A 0)) ((ConcreteCategory.hom (cochainsIso₀ A).inv) ↑x) g = 0 g
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 (cochainsIso₂ A).inv) ⇑x =
    (ConcreteCategory.hom ((shortComplexH2 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₂ A).inv)) x

Tactic:
;

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₂ A)
⊢ (ConcreteCategory.hom (cochainsIso₂ A).inv) ⇑x =
    (ConcreteCategory.hom ((shortComplexH2 A).moduleCatLeftHomologyData.i ≫ (cochainsIso₂ A).inv)) x
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
i✝ : Fin 0 → G
x✝ : ↑A
g✝ : Fin 1 → G
⊢ (ModuleCat.Hom.hom ((inhomogeneousCochains A).d 0 1) ∘ₗ LinearMap.single k (fun i ↦ ↑A) i✝) x✝ g✝ =
    (ModuleCat.Hom.hom 0 ∘ₗ LinearMap.single k (fun i ↦ ↑A) i✝) x✝ g✝

Tactic:
;

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
i✝ : Fin 0 → G
x✝ : ↑A
g✝ : Fin 1 → G
⊢ (ModuleCat.Hom.hom ((inhomogeneousCochains A).d 0 1) ∘ₗ LinearMap.single k (fun i ↦ ↑A) i✝) x✝ g✝ =
    (ModuleCat.Hom.hom 0 ∘ₗ LinearMap.single k (fun i ↦ ↑A) i✝) x✝ g✝
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
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝

Tactic:
;

Goal state after:
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
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝
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
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝

Tactic:
;

Goal state after:
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
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝
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
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ cochainsMap f φ = cochainsMap f ψ

Tactic:
;

Goal state after:
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
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ cochainsMap f φ = cochainsMap f ψ
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
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ φ = ψ

Tactic:
;

Goal state after:
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
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
⊢ φ = ψ
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
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
x✝ : ↑(res f A)
⊢ (Hom.hom φ).toLinearMap x✝ = (Hom.hom ψ).toLinearMap x✝

Tactic:
;

Goal state after:
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
hφψ : (Hom.hom φ).toLinearMap = (Hom.hom ψ).toLinearMap
x✝ : ↑(res f A)
⊢ (Hom.hom φ).toLinearMap x✝ = (Hom.hom ψ).toLinearMap x✝