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

Goal state before:
pp: case refine_2
k : Type u_1
G : Type u_2
inst✝⁴ : CommRing k
inst✝³ : Group G
V : Type u_4
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
g : G
inst✝ : Finite G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
y : V
⊢ (ρ g - LinearMap.id) y ∈ Coinvariants.ker ρ

Tactic:
simpa using

Goal state after:
case refine_2
k : Type u_1
G : Type u_2
inst✝⁴ : CommRing k
inst✝³ : Group G
V : Type u_4
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
g : G
inst✝ : Finite G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
y : V
⊢ (ρ g) y - y ∈ Coinvariants.ker ρ
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: case refine_1
k : Type u_1
G : Type u_2
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
this : Fintype G
g : G
y : MonoidAlgebra k G
⊢ (fun gv ↦ ((leftRegular k G) gv.1) gv.2 - gv.2) (g, y) ∈
    ↑((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker

Tactic:
simpa using

Goal state after:
case refine_1
k : Type u_1
G : Type u_2
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
this : Fintype G
g : G
y : MonoidAlgebra k G
⊢ ∑ x, y.coeff (g⁻¹ * x) = ∑ x, y.coeff x
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case hx
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
a : ↑A
x : G
hx : x ∉ MulAction.orbit (↥S) g
⊢ x ∉
    Function.support
      ↑(A.indToCoind
          ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
            ((MonoidAlgebra.lsingle g) 1 ⊗ₜ[k] a)))

Tactic:
simpa using

Goal state after:
case hx
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
a : ↑A
x : G
hx : x ∉ MulAction.orbit (↥S) g
⊢ (A.indToCoindAux g) a x = 0
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
σ : ↑(X.homogeneousCochains.X 0).toModuleCat
g : G
hσ : ↑σ g⁻¹ = ↑σ 1
⊢ (X.ρ g) (↑σ 1) = ↑σ 1

Tactic:
simpa using

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
σ : ↑(X.homogeneousCochains.X 0).toModuleCat
g : G
hσ : ↑σ g⁻¹ = ↑σ 1
⊢ (X.ρ g) (↑σ 1) = ↑σ 1
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
x✝ : ↥(↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
x : C(G, ↑X)
hx' : x ∈ (X.resolution'.X 0).ρ.invariants
hx✝ : ⟨x, hx'⟩ ∈ (↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
g : G
hx : ContinuousMap.const G x = (↑X.ρ.coind₁ι).comp x
⊢ x 1 = x g

Tactic:
simpa using

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
x✝ : ↥(↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
x : C(G, ↑X)
hx' : x ∈ (X.resolution'.X 0).ρ.invariants
hx✝ : ⟨x, hx'⟩ ∈ (↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
g : G
hx : ContinuousMap.const G x = (↑X.ρ.coind₁ι).comp x
⊢ x 1 = x g
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic

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

Tactic:
rw [d_eq, d_eq]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
⊢ ((freeLiftLEquiv k G (Fin n → G) A).toModuleIso.inv ≫
        ((barComplex k G).linearYonedaObj k A).d n (n + 1) ≫ (freeLiftLEquiv k G (Fin (n + 1) → G) A).toModuleIso.hom) ≫
      (freeLiftLEquiv k G (Fin (n + 1) → G) A).toModuleIso.inv ≫
        ((barComplex k G).linearYonedaObj k A).d (n + 1) (n + 1 + 1) ≫
          (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A).toModuleIso.hom =
    0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic

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

Tactic:
simpa using

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
⊢ d A n ≫ d A (n + 1) = 0
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A✝ : Rep k G
B✝ : Rep k H
A : Rep k G
B : Rep k H
f : ind φ A ⟶ B
h : H
a : ↑A
⊢ ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom
                  ((fun f ↦
                      ofHom
                        {
                          toLinearMap :=
                            Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                              (TensorProduct.lift
                                (((lift (↑A →ₗ[k] ↑B) k H) fun h ↦ B.ρ h⁻¹ ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ
                                  ↑(MonoidAlgebra.coeffLinearEquiv k)))
                              ⋯,
                          isIntertwining' := ⋯ })
                    ((fun f ↦ ofHom { toLinearMap := (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1, isIntertwining' := ⋯ })
                      f))).toLinearMap ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
          MonoidAlgebra.lsingle h)
        1)
      a =
    ((TensorProduct.AlgebraTensorModule.curry
            ((Hom.hom f).toLinearMap ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
          MonoidAlgebra.lsingle h)
        1)
      a

Tactic:
simpa using

Goal state after:
k : Type u
G : Type v
H : Type v'
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A✝ : Rep k G
B✝ : Rep k H
A : Rep k G
B : Rep k H
f : ind φ A ⟶ B
h : H
a : ↑A
⊢ (B.ρ h⁻¹)
      ((Hom.hom f)
        ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ))
          (MonoidAlgebra.single 1 1 ⊗ₜ[k] a))) =
    (Hom.hom f)
      ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ))
        (MonoidAlgebra.single h 1 ⊗ₜ[k] a))
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
s : G
x : ↑A
y : ↑B
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
            TensorProduct.map (A.ρ s) (B.ρ (φ s))))
        x)
      y =
    ((TensorProduct.AlgebraTensorModule.curry
          (TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1)))
        x)
      y

Tactic:
simpa using

Goal state after:
k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
s : G
x : ↑A
y : ↑B
⊢ (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ))
          (MonoidAlgebra.single 1 1 ⊗ₜ[k] (A.ρ s) x) ⊗ₜ[k]
        (B.ρ (φ s)) y -
      (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ))
          (MonoidAlgebra.single 1 1 ⊗ₜ[k] x) ⊗ₜ[k]
        y ∈
    Coinvariants.ker ((Representation.ind φ A.ρ).tprod B.ρ)
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
h : H
a : ↑A
b : ↑B
⊢ (((TensorProduct.AlgebraTensorModule.curry
              (((ind φ A).coinvariantsTensorMk B).compr₂
                  (ModuleCat.Hom.hom (coinvariantsTensorIndHom φ A B ≫ coinvariantsTensorIndInv φ A B)) ∘ₗ
                Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
            MonoidAlgebra.lsingle h)
          1)
        a)
      b =
    (((TensorProduct.AlgebraTensorModule.curry
              (((ind φ A).coinvariantsTensorMk B).compr₂
                  (ModuleCat.Hom.hom (𝟙 (((coinvariantsTensor k H).obj (ind φ A)).obj B))) ∘ₗ
                Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
            MonoidAlgebra.lsingle h)
          1)
        a)
      b

Tactic:
simpa using

Goal state after:
k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
h : H
a : ↑A
b : ↑B
⊢ (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ))
          (MonoidAlgebra.single 1 1 ⊗ₜ[k] a) ⊗ₜ[k]
        (B.ρ h) b -
      (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ))
          (MonoidAlgebra.single h 1 ⊗ₜ[k] a) ⊗ₜ[k]
        b ∈
    Coinvariants.ker ((Representation.ind φ A.ρ).tprod B.ρ)
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:
simpa using

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
⊢ (∀ (g : G), (A.ρ g) x✝ = x✝) ↔ (A.ρ g) x✝ = x✝
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:
simpa using

Goal state after:
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 ≫
        ofHom ↑(Representation.leftRegularTensorTrivialIsoFree (Fin m → G)).symm ≫
          MonoidalCategoryStruct.tensorHom (ofHom ↑(Representation.linearizeOfMulActionIso k G G).symm)
              (ofHom ↑(Representation.linearizeTrivialIso k G (Fin m → G)).symm) ≫
            Functor.LaxMonoidal.μ (linearization k G) (Action.leftRegular G) (Action.trivial G (Fin m → G)) ≫
              ofHom (Representation.linearizeMap (Action.diagonalSuccIsoTensorTrivial G m).inv) ≫
                ofHom ↑(Representation.linearizeOfMulActionIso k G (Fin (m + 1) → G)).symm =
    0
Module: Mathlib.RepresentationTheory.Homological.Resolution

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

Tactic:
d_comp_diagonalSuccIsoFree_inv_eq

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
j : ℕ
⊢ (diagonalSuccIsoFree k G (j + 1)).inv ≫ (standardComplex k G).d (j + 1) j =
    (diagonalSuccIsoFree k G (j + 1)).inv ≫ (standardComplex k G).d (j + 1) j
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
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap A K))

Tactic:
exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)

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:
simpa using

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
⊢ d A (n + 1) ≫ d A n = 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
f : ↥(cocycles₁ A)
this : (A.ρ 1) (f 1) - f (1 * 1) + f 1 = 0
⊢ f 1 = 0

Tactic:
simpa using

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: 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:
simpa using

Goal state after:
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
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:
simpa using

Goal state after:
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)
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:
simpa using

Goal state after:
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)
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:
simpa using

Goal state after:
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
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:
simpa using

Goal state after:
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)
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:
simpa using

Goal state after:
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)
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:
simpa using

Goal state after:
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
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:
simpa using

Goal state after:
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)
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:
rw [← sub_eq_zero, ← map_sub, H2π_eq_zero_iff]
  rfl

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:
simpa using

Goal state after:
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)
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:
simpa [H2π] using h ((isoCocycles₂ A).hom y)

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

Goal state before:
pp: case pos
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)
⊢ (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              (A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom ≫ (moduleCatChainComplex A g✝).d (j + 1) j)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1 =
    (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              ((HomologicalComplex.coinvariantsTensorObj A (resolution k g✝⁻¹ ⋯).complex).d (j + 1) j ≫
                A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1

Tactic:
simpa using

Goal state after:
case pos
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)
⊢ ∑ x, (A.ρ (x * g⁻¹)) a = ∑ c, (A.ρ (c⁻¹ * g⁻¹)) a
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 : ℕ
x : ↑(shortComplexH1 A).X₁
g : G
⊢ (ModuleCat.Hom.hom (Hom.toModuleCatHom φ ≫ (shortComplexH1 B).f)) x g =
    (ModuleCat.Hom.hom ((shortComplexH1 A).f ≫ cochainsMap₁ f φ)) x g

Tactic:
simpa using

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
n : ℕ
x : ↑(shortComplexH1 A).X₁
g : G
⊢ (B.ρ g) ((Hom.hom φ) x) = (Hom.hom φ) ((A.ρ (f g)) 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
n : ℕ
x : ↑(shortComplexH1 A).X₂
g : G × G
⊢ (ModuleCat.Hom.hom (cochainsMap₁ f φ ≫ (shortComplexH1 B).g)) x g =
    (ModuleCat.Hom.hom ((shortComplexH1 A).g ≫ cochainsMap₂ f φ)) x g

Tactic:
simpa using

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
n : ℕ
x : ↑(shortComplexH1 A).X₂
g : G × G
⊢ (B.ρ g.1) ((Hom.hom φ) (x (f g.2))) = (Hom.hom φ) ((A.ρ (f g.1)) (x (f g.2)))
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η₁ η₂ : Aut (forget k G)
h : η₁.hom.hom.app rightFDRep = η₂.hom.hom.app rightFDRep
this : Fintype G
X : FDRep k G
v : ↑((forget k G).obj X).obj
h1 : (forget k G).map (ofRightFDRep X v) ≫ η₁.hom.hom.app X = (forget k G).map (ofRightFDRep X v) ≫ η₂.hom.hom.app X
h2 :
  (forget k G).map (ofRightFDRep X v) ≫ η₂.hom.hom.app X =
    η₂.hom.hom.app rightFDRep ≫ (forget k G).map (ofRightFDRep X v)
⊢ (Hom.hom (η₁.hom.hom.app X).hom) v = (Hom.hom (η₂.hom.hom.app X).hom) v

Tactic:
simpa using

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η₁ η₂ : Aut (forget k G)
h : η₁.hom.hom.app rightFDRep = η₂.hom.hom.app rightFDRep
this : Fintype G
X : FDRep k G
v : ↑((forget k G).obj X).obj
h1 : (forget k G).map (ofRightFDRep X v) ≫ η₁.hom.hom.app X = (forget k G).map (ofRightFDRep X v) ≫ η₂.hom.hom.app X
h2 :
  (forget k G).map (ofRightFDRep X v) ≫ η₂.hom.hom.app X =
    η₂.hom.hom.app rightFDRep ≫ (forget k G).map (ofRightFDRep X v)
⊢ (Hom.hom (η₁.hom.hom.app X).hom) v = (Hom.hom (η₂.hom.hom.app X).hom) v
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
c : σ →₀ ℕ
hx : c + single i 1 ∈ ⇑degree ⁻¹' Set.Ici 1
hi : i ∈ (c + single i 1).support
⊢ c + single i 1 ∈ (fun x ↦ (monomial x) 1) ⁻¹' ↑(Submodule.restrictScalars R (idealOfVars σ R))

Tactic:
simpa using

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
c : σ →₀ ℕ
hx : c + single i 1 ∈ ⇑degree ⁻¹' Set.Ici 1
hi : i ∈ (c + single i 1).support
⊢ (monomial c) 1 * X i ∈ idealOfVars σ R
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
h : ¬r = 0
⊢ C r ∈ idealOfVars σ R ^ n ↔ r = 0 ∨ n = 0

Tactic:
simpa using

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
h : ¬r = 0
⊢ C r ∈ idealOfVars σ R ^ n ↔ n = 0
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
p : MvPowerSeries σ R
x : σ →₀ ℕ
⊢ ∀ b ∈ ⋯.toFinset, b ≠ x → (coeff b) p = 0

Tactic:
simpa using

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
p : MvPowerSeries σ R
x : σ →₀ ℕ
⊢ ∀ (b : σ →₀ ℕ), mapDomain (⇑e) b = embDomain e x → ¬b = x → (coeff b) p = 0
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
x✝ : MvPowerSeries σ R
y : σ →₀ ℕ
⊢ (coeff y) ((rename id) x✝) = (coeff y) ((AlgHom.id R (MvPowerSeries σ R)) x✝)

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
x✝ : MvPowerSeries σ R
y : σ →₀ ℕ
⊢ ∑ x ∈ ⋯.toFinset, (coeff x) x✝ = (coeff y) x✝
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
a₁✝ a₂✝ : MvPowerSeries σ R
h : (rename ⇑e) a₁✝ = (rename ⇑e) a₂✝
x : σ →₀ ℕ
⊢ (coeff x) a₁✝ = (coeff x) a₂✝

Tactic:
simpa using

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
a₁✝ a₂✝ : MvPowerSeries σ R
h : (rename ⇑e) a₁✝ = (rename ⇑e) a₂✝
x : σ →₀ ℕ
⊢ (coeff x) a₁✝ = (coeff x) a₂✝