mathlib-initiative/mathlib-tactics huggingface dataset:
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) - x (g.1 * g.2) + ((A.ρ g.1) (y g.2) - y (g.1 * g.2)) + (x g.1 + y g.1) =
    (A.ρ g.1) (x g.2) - x (g.1 * g.2) + ((A.ρ g.1) (y g.2) - y (g.1 * g.2)) + (x g.1 + y g.1)

Tactic:
]

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

Goal state before:
pp: case refine_2
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ˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η * ↑g ((algebraMap B L) a) = (algebraMap B L) a
⊢ η * ((galRestrict A K L B) g) a = a

Tactic:
]

Goal state after:
case refine_2
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ˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η * ↑g ((algebraMap B L) a) = (algebraMap B L) a
⊢ η * ((galRestrict A K L B) g) a = a
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
⊢ (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 : ↥(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
⊢ (ModuleCat.Hom.hom (d₁₂ X.X₃ ≫ (cochainsIso₂ X.X₃).inv)) ⇑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
r : k
x : G → ↑A
g : G × G
⊢ r • (A.ρ g.1) (x g.2) - r • x (g.1 * g.2) + r • x g.1 = r • (A.ρ g.1) (x g.2) - r • x (g.1 * g.2) + r • x g.1

Tactic:
]

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

Goal state before:
pp: case refine_2
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ˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η * ↑g ((algebraMap B L) a) = (algebraMap B L) a
⊢ (algebraMap B L) η * (algebraMap B L) (((galRestrict A K L B) g) a) = (algebraMap B L) η * ↑g ((algebraMap B L) a)

Tactic:
]

Goal state after:
case refine_2
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ˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η * ↑g ((algebraMap B L) a) = (algebraMap B L) a
⊢ (algebraMap B L) η * (algebraMap B L) (((galRestrict A K L B) g) a) = (algebraMap B L) η * ↑g ((algebraMap B L) a)
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 + 1) → G
⊢ (⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₂ X.X₁).inv) x) g =
    (ModuleCat.Hom.hom (d₁₂ X.X₂ ≫ (cochainsIso₂ X.X₂).inv)) y 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 + 1) → G
⊢ (⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₂ X.X₁).inv) x) g =
    (ModuleCat.Hom.hom (d₁₂ X.X₂ ≫ (cochainsIso₂ X.X₂).inv)) 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
x y : G × G → ↑A
g : G × G × 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)) +
      ((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))) =
    (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)) +
      ((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)))

Tactic:
]

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

Goal state before:
pp: case refine_2
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ˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η = 0
e : g (IsLocalization.mk' L a b) = 0
⊢ False

Tactic:
]

Goal state after:
case refine_2
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ˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η = 0
e : g (IsLocalization.mk' L a b) = 0
⊢ False
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: case refine_2
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
hη : 0 = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : 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
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η = 0
e : g (IsLocalization.mk' L a b) = 0
⊢ False

Tactic:
]

Goal state after:
case refine_2
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
hη : 0 = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : 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
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η = 0
e : g (IsLocalization.mk' L a b) = 0
⊢ False
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 : Fin 0 → G
a : ↑A
y : G
⊢ (A.ρ y) (Pi.single x a default) - Pi.single x a default =
    (A.ρ y) (Pi.single x a default) - Pi.single x a ((fun a ↦ default) (uniqueElim y))

Tactic:
]

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

Tactic:
]

Goal state after:
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 : ℕ
⊢ ((A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G)).toModuleIso.inv ≫
        (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
          (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G)).toModuleIso.hom) ≫
      (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 =
    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 : ↑((inhomogeneousCochains A).X 1)
y : G × G
⊢ (A.ρ y.1) (x ((Equiv.funUnique (Fin 1) G).symm y.2)) - x ((Equiv.funUnique (Fin 1) G).symm (y.1 * y.2)) +
      x ((Equiv.funUnique (Fin 1) G).symm y.1) =
    (A.ρ ((piFinTwoEquiv fun x ↦ G).symm y 0)) (x fun i ↦ (piFinTwoEquiv fun x ↦ G).symm y i.succ) +
      ((-1) ^ (↑0 + 1) • x (Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2) ((piFinTwoEquiv fun x ↦ G).symm y)) +
        (-1) ^ (↑1 + 1) • x (Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2) ((piFinTwoEquiv fun x ↦ G).symm y)))

Tactic:
]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
⊢ (A.ρ y.1) (x ((Equiv.funUnique (Fin 1) G).symm y.2)) - x ((Equiv.funUnique (Fin 1) G).symm (y.1 * y.2)) +
      x ((Equiv.funUnique (Fin 1) G).symm y.1) =
    (A.ρ ((piFinTwoEquiv fun x ↦ G).symm y 0)) (x fun i ↦ (piFinTwoEquiv fun x ↦ G).symm y i.succ) +
      ((-1) ^ (↑0 + 1) • x (Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2) ((piFinTwoEquiv fun x ↦ G).symm y)) +
        (-1) ^ (↑1 + 1) • x (Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2) ((piFinTwoEquiv fun x ↦ G).symm y)))
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: case e_a.e_6
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
i : Fin 1
⊢ (Equiv.funUnique (Fin 1) G).symm y.2 0 = (piFinTwoEquiv fun x ↦ G).symm y (Fin.succ 0)

Tactic:
]

Goal state after:
case e_a.e_6
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
i : Fin 1
⊢ (Equiv.funUnique (Fin 1) G).symm y.2 0 = (piFinTwoEquiv fun x ↦ G).symm y (Fin.succ 0)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: case e_a.e_a
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
i : Fin 1
⊢ (Equiv.funUnique (Fin 1) G).symm (y.1 * y.2) 0 =
    Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2) ((piFinTwoEquiv fun x ↦ G).symm y) 0

Tactic:
]

Goal state after:
case e_a.e_a
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
i : Fin 1
⊢ (Equiv.funUnique (Fin 1) G).symm (y.1 * y.2) 0 =
    Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2) ((piFinTwoEquiv fun x ↦ G).symm y) 0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: case e_a.e_a
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
i : Fin 1
⊢ (Equiv.funUnique (Fin 1) G).symm y.1 0 = Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2) ((piFinTwoEquiv fun x ↦ G).symm y) 0

Tactic:
]

Goal state after:
case e_a.e_a
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 1)
y : G × G
i : Fin 1
⊢ (Equiv.funUnique (Fin 1) G).symm y.1 0 = Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2) ((piFinTwoEquiv fun x ↦ G).symm y) 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 : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (A.ρ y.1) (x ((piFinTwoEquiv fun x ↦ G).symm (y.2.1, y.2.2))) -
          x ((piFinTwoEquiv fun x ↦ G).symm (y.1 * y.2.1, y.2.2)) +
        x ((piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1 * y.2.2)) -
      x ((piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1)) =
    (A.ρ ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y) 0))
        (x fun i ↦ (Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y) i.succ) +
      ((-1) ^ (↑0 + 1) •
            x
              (Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2)
                ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y))) +
          (-1) ^ (↑1 + 1) •
            x
              (Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2)
                ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y))) +
        (-1) ^ (↑2 + 1) •
          x
            (Fin.contractNth 2 (fun x1 x2 ↦ x1 * x2)
              ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y))))

Tactic:
]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (A.ρ y.1) (x ((piFinTwoEquiv fun x ↦ G).symm (y.2.1, y.2.2))) -
          x ((piFinTwoEquiv fun x ↦ G).symm (y.1 * y.2.1, y.2.2)) +
        x ((piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1 * y.2.2)) -
      x ((piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1)) =
    (A.ρ ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y) 0))
        (x fun i ↦ (Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y) i.succ) +
      ((-1) ^ (↑0 + 1) •
            x
              (Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2)
                ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y))) +
          (-1) ^ (↑1 + 1) •
            x
              (Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2)
                ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y))) +
        (-1) ^ (↑2 + 1) •
          x
            (Fin.contractNth 2 (fun x1 x2 ↦ x1 * x2)
              ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y))))
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 = (A.ρ g) (f g⁻¹) + f g

Tactic:
]

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 + f h = f g + f h

Tactic:
]

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 = g • f g⁻¹ + f g

Tactic:
]

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 = g • f g⁻¹ * f g

Tactic:
]

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
⊢ Function.Injective ⇑(ConcreteCategory.hom (shortComplexH0 A).f)

Tactic:
]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ Function.Injective ⇑(ConcreteCategory.hom (shortComplexH0 A).f)
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:
rw [ModuleCat.mono_iff_injective]
  apply Submodule.injective_subtype

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₂ : ↑(shortComplexH0 A).X₂),
    (ConcreteCategory.hom (shortComplexH0 A).g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom (shortComplexH0 A).f) x₁ = x₂

Tactic:
]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ ∀ (x₂ : ↑(shortComplexH0 A).X₂),
    (ConcreteCategory.hom (shortComplexH0 A).g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom (shortComplexH0 A).f) 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
x : ↑A
hx : (ConcreteCategory.hom (d₀₁ A)) x = 0
g : G
⊢ (A.ρ g) x - x = 0

Tactic:
]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A
hx : (ConcreteCategory.hom (d₀₁ A)) x = 0
g : G
⊢ (A.ρ g) x - x = 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
⊢ (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f = iCocycles A 0 ≫ (cochainsIso₀ A).hom

Tactic:
dsimp [cocyclesIso₀]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (KernelFork.ofι (HomologicalComplex.iCycles (inhomogeneousCochains A) 0) ⋯).mapOfIsLimit ⋯.fIsKernel
        (dArrowIso₀₁ A).hom ≫
      (shortComplexH0 A).f =
    iCocycles A 0 ≫ (cochainsIso₀ A).hom
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

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

Tactic:
]

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 (cochainsIso₀ A).inv) ↑x =
    (ConcreteCategory.hom (iCocycles A 0)) ((ConcreteCategory.hom (cocyclesIso₀ A).inv) x)

Tactic:
]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥A.ρ.invariants
⊢ (ConcreteCategory.hom (cochainsIso₀ A).inv) ↑x =
    (ConcreteCategory.hom (iCocycles A 0)) ((ConcreteCategory.hom (cocyclesIso₀ 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
x : ↥(cocycles₁ A)
⊢ 0 = 0

Tactic:
]

Goal state after: