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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
m : ℕ
f : Fin m → G
g : G
r : k
step1 :
  (Hom.hom (leftRegularTensorTrivialIsoFree k G (Fin m → G)).inv) (single f (MonoidAlgebra.single g r)) =
    MonoidAlgebra.single g 1 ⊗ₜ[k] MonoidAlgebra.single f r
key₁ :
  (Representation.linearizeMap (Action.diagonalSuccIsoTensorTrivial G m).inv) (MonoidAlgebra.single (g, f) (1 * r)) =
    MonoidAlgebra.single ((ConcreteCategory.hom (Action.diagonalSuccIsoTensorTrivial G m).inv.hom) (g, f)) (1 * r)
⊢ (Representation.linearizeMap (Action.diagonalSuccIsoTensorTrivial G m).inv)
      ((Representation.LinearizeMonoidal.μ (Action.leftRegular G) (Action.trivial G (Fin m → G)))
        ((LinearEquiv.refl k k[(Action.ofMulAction G G).V]) (MonoidAlgebra.single g 1) ⊗ₜ[k]
          MonoidAlgebra.single f r)) =
    MonoidAlgebra.single (g • Fin.partialProd f) r

Tactic:
have key₂ := Representation.LinearizeMonoidal.μ_apply_single_single (k := k)
        (X := Action.leftRegular G) (Y := Action.trivial G (Fin m → G)) g f 1 r

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
m : ℕ
f : Fin m → G
g : G
r : k
step1 :
  (Hom.hom (leftRegularTensorTrivialIsoFree k G (Fin m → G)).inv) (single f (MonoidAlgebra.single g r)) =
    MonoidAlgebra.single g 1 ⊗ₜ[k] MonoidAlgebra.single f r
key₁ :
  (Representation.linearizeMap (Action.diagonalSuccIsoTensorTrivial G m).inv) (MonoidAlgebra.single (g, f) (1 * r)) =
    MonoidAlgebra.single ((ConcreteCategory.hom (Action.diagonalSuccIsoTensorTrivial G m).inv.hom) (g, f)) (1 * r)
key₂ :
  (Representation.LinearizeMonoidal.μ (Action.leftRegular G) (Action.trivial G (Fin m → G)))
      (MonoidAlgebra.single g 1 ⊗ₜ[k] MonoidAlgebra.single f r) =
    MonoidAlgebra.single (g, f) (1 * r)
⊢ (Representation.linearizeMap (Action.diagonalSuccIsoTensorTrivial G m).inv)
      ((Representation.LinearizeMonoidal.μ (Action.leftRegular G) (Action.trivial G (Fin m → G)))
        ((LinearEquiv.refl k k[(Action.ofMulAction G G).V]) (MonoidAlgebra.single g 1) ⊗ₜ[k]
          MonoidAlgebra.single f r)) =
    MonoidAlgebra.single (g • Fin.partialProd f) r
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
m : ℕ
f : Fin m → G
g : G
r : k
step1 :
  (Hom.hom (leftRegularTensorTrivialIsoFree k G (Fin m → G)).inv) (single f (MonoidAlgebra.single g r)) =
    MonoidAlgebra.single g 1 ⊗ₜ[k] MonoidAlgebra.single f r
key₁ :
  (Representation.linearizeMap (Action.diagonalSuccIsoTensorTrivial G m).inv) (MonoidAlgebra.single (g, f) (1 * r)) =
    MonoidAlgebra.single ((ConcreteCategory.hom (Action.diagonalSuccIsoTensorTrivial G m).inv.hom) (g, f)) (1 * r)
key₂ :
  (Representation.LinearizeMonoidal.μ (Action.leftRegular G) (Action.trivial G (Fin m → G)))
      (MonoidAlgebra.single g 1 ⊗ₜ[k] MonoidAlgebra.single f r) =
    MonoidAlgebra.single (g, f) (1 * r)
⊢ MonoidAlgebra.single ((ConcreteCategory.hom (Action.diagonalSuccIsoTensorTrivial G m).inv.hom) (g, f)) (1 * r) =
    MonoidAlgebra.single (g • Fin.partialProd f) r

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
⊢ ∀ (m : ℕ) (f : Fin m → G) (g : G) (r : k),
    (Hom.hom (diagonalSuccIsoFree k G m).inv) (single f (MonoidAlgebra.single g r)) =
      MonoidAlgebra.single (g • Fin.partialProd f) r

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
⊢ (Hom.hom (d k G n ≫ (diagonalSuccIsoFree k G n).inv)) (single i (MonoidAlgebra.single 1 1)) =
    (Hom.hom ((diagonalSuccIsoFree k G (n + 1)).inv ≫ (standardComplex k G).d (n + 1) n))
      (single i (MonoidAlgebra.single 1 1))

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
m : ℕ
⊢ (barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ (diagonalSuccIsoFree k G m).inv = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
m : ℕ
key : (barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ (diagonalSuccIsoFree k G m).inv = 0
⊢ (barComplex.d k G (m + 1) ≫ barComplex.d k G m) ≫ (diagonalSuccIsoFree k G m).inv =
    0 ≫ (diagonalSuccIsoFree k G m).inv

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

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

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

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

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel i j →
    (diagonalSuccIsoFree k G i).symm.hom ≫ (standardComplex k G).d i j =
      (barComplex k G).d i j ≫ (diagonalSuccIsoFree k G j).symm.hom

Tactic:
by

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

Goal state before:
pp: K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
g : Gal(L/K)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x : L
hx : (Algebra.norm K) x = 1
⊢ ∃ y, ↑y / g ↑y = x

Tactic:
by

Goal state after:
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 : ℕ
⊢ ((X.map (cochainsFunctor k G)).map (HomologicalComplex.eval (ModuleCat k) (ComplexShape.up ℕ) i)).Exact

Tactic:
by

Goal state after:
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 j : ℕ
y : (Fin i → G) → ↑X.X₂
x : (Fin j → G) → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d i j)) y
⊢ (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map ((X.map (cochainsFunctor k G)).f.f j))) x =
    (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map ((X.map (cochainsFunctor k G)).X₂.d i j))) y

Tactic:
by

Goal state after:
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 j : ℕ
y : (Fin i → G) → ↑X.X₂
x : (Fin j → G) → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d i j)) y
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d X.X₁ j)) x = 0

Tactic:
by

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

Goal state before:
pp: K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
⊢ Module.IsTorsionFree A L

Tactic:
by

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

Goal state before:
pp: K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝ : Module.IsTorsionFree A L
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
h : (algebraMap B L) η = 0
⊢ False

Tactic:
by

Goal state after:
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 j : ℕ
hij : i + 1 = j
z : (Fin i → G) → ↑X.X₃
hz : (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d i j)) z = 0
y : (Fin i → G) → ↑X.X₂
hy : (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f i)) y = z
x : (Fin j → G) → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d i j)) y
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d X.X₃ i)) z = 0

Tactic:
by

Goal state after:
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 j : ℕ
hij : i + 1 = j
z : (Fin i → G) → ↑X.X₃
hz : (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d i j)) z = 0
y : (Fin i → G) → ↑X.X₂
hy : (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f i)) y = z
x : (Fin j → G) → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d i j)) y
⊢ (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map ((X.map (cochainsFunctor k G)).f.f j))) x =
    (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map ((X.map (cochainsFunctor k G)).X₂.d i j))) y

Tactic:
by

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

Goal state before:
pp: K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝ : Module.IsTorsionFree A L
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
hε : ↑ε / g ↑ε = (algebraMap B L) η
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
⊢ t • IsLocalization.mk' L a b = (algebraMap B L) a

Tactic:
by

Goal state after:
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 j : ℕ
hij : i + 1 = j
z : (Fin i → G) → ↑X.X₃
hz : (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d i j)) z = 0
y : (Fin i → G) → ↑X.X₂
hy : (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f i)) y = z
x : (Fin j → G) → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d i j)) y
⊢ (ComplexShape.up ℕ).next j = j + 1

Tactic:
by

Goal state after:
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 j : ℕ
hij : i + 1 = j
z : (Fin i → G) → ↑X.X₃
hz : (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d i j)) z = 0
y : (Fin i → G) → ↑X.X₂
hy : (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f i)) y = z
x : (Fin j → G) → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d i j)) y
⊢ (ConcreteCategory.hom (δ hX i j hij)) ((ConcreteCategory.hom (π X.X₃ i)) (cocyclesMk z ⋯)) =
    (ConcreteCategory.hom (π X.X₁ j)) (cocyclesMkOfCompEqD hX hx)

Tactic:
by

Goal state after:
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
y : ↑X.X₂
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
⊢ x ∈ cocycles₁ X.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 y : ↑A
g : G
⊢ (A.ρ g) (x + y) - (x + y) = ((fun g ↦ (A.ρ g) x - x) + fun g ↦ (A.ρ g) y - y) 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
r : k
x : ↑A
g : G
⊢ (A.ρ g) (r • x) - r • x = ((RingHom.id k) r • fun g ↦ (A.ρ g) x - x) g

Tactic:
by

Goal state after:
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
⊢ (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d 0 (0 + 1)))
      ((ConcreteCategory.hom (cochainsIso₀ X.X₃).inv) ↑z) =
    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
⊢ (ModuleCat.Hom.hom (d₀₁ A)).ker = A.ρ.invariants

Tactic:
by

Goal state after:
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
⊢ (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f 0)) ((ConcreteCategory.hom (cochainsIso₀ X.X₂).inv) y) =
    (ConcreteCategory.hom (cochainsIso₀ X.X₃).inv) ↑z

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
⊢ 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
⊢ ModuleCat.ofHom A.ρ.invariants.subtype ≫ d₀₁ A = 0

Tactic:
by

Goal state after:
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
⊢ ⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₁ X.X₁).inv) x =
    (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d 0 (0 + 1))) ((ConcreteCategory.hom (cochainsIso₀ X.X₂).inv) y)

Tactic:
by

Goal state after:
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
⊢ (ConcreteCategory.hom (δ hX 0 1 ⋯)) ((ConcreteCategory.hom (H0Iso X.X₃).inv) z) =
    (ConcreteCategory.hom (H1π X.X₁)) ⟨x, ⋯⟩

Tactic:
by

Goal state after:
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
y : G → ↑X.X₂
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
⊢ x ∈ cocycles₂ X.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 y : G → ↑A
g : G × G
⊢ (A.ρ g.1) ((x + y) g.2) - (x + y) (g.1 * g.2) + (x + y) g.1 =
    ((fun g ↦ (A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1) + fun g ↦ (A.ρ g.1) (y g.2) - y (g.1 * g.2) + y g.1) 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
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 =
    ((RingHom.id k) r • fun g ↦ (A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1) g

Tactic:
by

Goal state after:
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
⊢ (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d 1 (1 + 1)))
      ((ConcreteCategory.hom (cochainsIso₁ X.X₃).inv) ⇑z) =
    0

Tactic:
by

Goal state after:
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
⊢ (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f 1)) ((ConcreteCategory.hom (cochainsIso₁ X.X₂).inv) y) =
    (ConcreteCategory.hom (cochainsIso₁ X.X₃).inv) ⇑z

Tactic:
by

Goal state after:
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
⊢ ⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₂ X.X₁).inv) x =
    (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d 1 (1 + 1))) ((ConcreteCategory.hom (cochainsIso₁ X.X₂).inv) 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
x y : G × G → ↑A
g : G × G × G
⊢ (A.ρ g.1) ((x + y) (g.2.1, g.2.2)) - (x + y) (g.1 * g.2.1, g.2.2) + (x + y) (g.1, g.2.1 * g.2.2) -
      (x + y) (g.1, g.2.1) =
    ((fun g ↦ (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)) + fun g ↦
        (A.ρ g.1) (y (g.2.1, g.2.2)) - y (g.1 * g.2.1, g.2.2) + y (g.1, g.2.1 * g.2.2) - y (g.1, g.2.1))
      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
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) =
    ((RingHom.id k) r • fun g ↦
        (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))
      g

Tactic:
by

Goal state after:
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
⊢ (ConcreteCategory.hom (δ hX 1 2 ⋯)) ((ConcreteCategory.hom (H1π X.X₃)) z) = (ConcreteCategory.hom (H2π X.X₁)) ⟨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 0 1 ≫ (cochainsIso₁ A).hom

Tactic:
by

Goal state after:
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✝²)
⊢ 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) =
    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)

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 : ℕ
g : Fin (n + 1) → G
a : ↑A
⊢ (ConcreteCategory.hom (d A n)) (single g a) =
    single (fun i ↦ g i.succ) ((A.ρ (g 0)⁻¹) a) +
      ∑ j, (-1) ^ (↑j + 1) • single (j.contractNth (fun x1 x2 ↦ x1 * x2) g) a

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 : ℕ
inst✝ : DecidableEq G
⊢ d A n =
    (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G)).toModuleIso.inv ≫
      (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n ≫
        (A.coinvariantsTensorFreeLEquiv (Fin n → G)).toModuleIso.hom

Tactic:
by

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

Goal state before:
pp: K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) 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
⊢ (cochainsIso₁ A).hom ≫ d₁₂ A = (inhomogeneousCochains A).d 1 2 ≫ (cochainsIso₂ A).hom

Tactic:
by

Goal state after: