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
i : ℕ
hi : Odd i
⊢ (ComplexShape.up ℕ).Rel i ((ComplexShape.up ℕ).next i)

Tactic:
simp

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
x✝¹ : G
x✝ : Fin 1 → G
⊢ ((((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
          (Representation.ofMulAction k G (Fin 1 → G)) x✝¹) ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    (((Representation.trivial k G k) x✝¹ ∘ₗ (linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1

Tactic:
simp

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
x : L
hx : (Algebra.norm K) x = 1
xu : Lˣ := ⋯.unit
hx' : ↑(toMul (toAdditive ((Hom.hom (ofAlgebraAutOnUnits K L).norm) (toAdditive.symm (ofMul xu))))) = 1
⊢ Odd 1

Tactic:
simp

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
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:
simp

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:
simp

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

Goal state before:
pp: case h
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
x : L
hx : (Algebra.norm K) x = 1
xu : Lˣ := ⋯.unit
hx' : ↑(toMul (toAdditive ((Hom.hom (ofAlgebraAutOnUnits K L).norm) (toAdditive.symm (ofMul xu))))) = 1
this✝ :
  (CategoryTheory.ConcreteCategory.hom (FiniteCyclicGroup.groupCohomologyπOdd (ofAlgebraAutOnUnits K L) g hg 1 ⋯))
        ⟨toAdditive.symm (ofMul xu), ⋯⟩ =
      0 ↔
    ↑⟨toAdditive.symm (ofMul xu), ⋯⟩ ∈
      (Hom.hom
          ((ofAlgebraAutOnUnits K L).applyAsHom g - CategoryTheory.CategoryStruct.id (ofAlgebraAutOnUnits K L))).range
y : ↑(ofAlgebraAutOnUnits K L)
hy :
  (Hom.hom
          ((ofAlgebraAutOnUnits K L).applyAsHom g -
            CategoryTheory.CategoryStruct.id (ofAlgebraAutOnUnits K L))).toLinearMap
      y =
    ↑⟨toAdditive.symm (ofMul xu), ⋯⟩
this : ↑(toMul (((ofAlgebraAutOnUnits K L).ρ g) y - y)) = x
⊢ g ↑(toMul (toAdditive y)) / ↑(toMul (toAdditive y)) = ↑(toMul (((ofAlgebraAutOnUnits K L).ρ g) y) / toMul y)

Tactic:
simp

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:
simp

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
⊢ (ModuleCat.Hom.hom (d₀₁ X.X₃ ≫ (cochainsIso₁ X.X₃).inv)) ↑z = 0

Tactic:
simp

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 : ↑((inhomogeneousCochains A).X 1)
y : G × G
⊢ (ModuleCat.Hom.hom ((cochainsIso₁ A).hom ≫ d₁₂ A)) x y =
    (ModuleCat.Hom.hom ((inhomogeneousCochains A).d 1 2 ≫ (cochainsIso₂ A).hom)) x y

Tactic:
change A.ρ y.1 (x _) - x _ + x _ = _ + _

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) +
      ∑ j, (-1) ^ (↑j + 1) • x (j.contractNth (fun x1 x2 ↦ x1 * x2) ((piFinTwoEquiv fun x ↦ G).symm y))
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 ≫
      0 ≫ (A.coinvariantsTensorFreeLEquiv (Fin n → G)).toModuleIso.hom =
    0

Tactic:
simp

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

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

Tactic:
simp_rw [funext_iff, d₂₃_hom_apply, Prod.forall]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G × G → ↑A
⊢ (∀ (a a_1 b : G), (A.ρ a) (f (a_1, b)) - f (a * a_1, b) + f (a, a_1 * b) - f (a, a_1) = 0 (a, a_1, b)) ↔
    ∀ (g h j : G), (A.ρ g) (f (h, j)) - f (g * h, j) + f (g, h * j) - f (g, h) = 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
⊢ (ComplexShape.up ℕ).next 0 = 1

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₂ A)
⊢ (ConcreteCategory.hom (cochainsIso₂ A).inv) ⇑x =
    (ConcreteCategory.hom ((forget₂ (ModuleCat k) Ab).map (HomologicalComplex.iCycles (inhomogeneousCochains A) 2)))
      ((ConcreteCategory.hom (isoCocycles₂ A).inv) x)

Tactic:
simp

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
⊢ π A 0 ≫ (H0IsoOfIsTrivial A).hom = iCocycles A 0 ≫ (cochainsIso₀ A).hom

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ (ComplexShape.down ℕ).Rel ((ComplexShape.down ℕ).prev i) i

Tactic:
simp

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

Goal state before:
pp: case succ
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
n : ℕ
a✝ : ∀ [h₀ : NeZero n], Even n → (ComplexShape.down ℕ).Rel n ((ComplexShape.down ℕ).next n)
h₀ : NeZero (n + 1)
hi : Even (n + 1)
⊢ (ComplexShape.down ℕ).Rel (n + 1) ((ComplexShape.down ℕ).next (n + 1))

Tactic:
simp

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

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
⊢ (ComplexShape.down ℕ).Rel ((ComplexShape.down ℕ).prev i) i

Tactic:
simp

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

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
j : ℕ
⊢ (ComplexShape.down ℕ).Rel (2 * j + 1) ((ComplexShape.down ℕ).next (2 * j + 1))

Tactic:
simp

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ (↑e.symm).comp ↑e = MonoidHom.id G

Tactic:
simp

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ (↑e).comp ↑e.symm = MonoidHom.id H

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ cocyclesMap f φ 0 ≫ (cocyclesIso₀ B).hom ≫ (shortComplexH0 B).f =
    (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f ≫ Hom.toModuleCatHom φ

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ mapCocycles₁ f φ ≫ (shortComplexH1 B).moduleCatLeftHomologyData.i =
    (shortComplexH1 A).moduleCatLeftHomologyData.i ≫ cochainsMap₁ f φ

Tactic:
simp

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

Goal state before:
pp: case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
i : ℕ
x✝ : (Fin i → G) →₀ ↑X
a✝ : Fin i → G
⊢ ((Finsupp.mapRange.linearMap ((Rep.Hom.hom f).toLinearMap + (Rep.Hom.hom g).toLinearMap)) x✝) a✝ =
    ((Finsupp.mapRange.linearMap (Rep.Hom.hom f).toLinearMap + Finsupp.mapRange.linearMap (Rep.Hom.hom g).toLinearMap)
        x✝)
      a✝

Tactic:
simp

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

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
X✝ : Rep R G
Y✝ : Rep R G
X Y : Rep R G
⊢ (tateComplexFunctor R G).map 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
g : G
X : FDRep k G
x : ↑X.V.obj
⊢ (Hom.hom (InducedCategory.homMk (↟(X.ρ g)) ≫ InducedCategory.homMk (↟(X.ρ g⁻¹))).hom) x = (Hom.hom (𝟙 X.V).hom) x

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
g : G
X : FDRep k G
x : ↑X.V.obj
⊢ (Hom.hom (InducedCategory.homMk (↟(X.ρ g⁻¹)) ≫ InducedCategory.homMk (↟(X.ρ g))).hom) x = (Hom.hom (𝟙 X.V).hom) x

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝¹ : FDRep k G
x✝ : ↑((forget k G).obj x✝¹).obj
⊢ (Hom.hom ((LaxMonoidalFunctor.isoOfComponents (equivApp 1) ⋯ ⋯ ⋯).hom.hom.app x✝¹).hom) x✝ =
    (Hom.hom ((Iso.hom 1).hom.app x✝¹).hom) x✝

Tactic:
simp

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝¹ : FDRep k G
x✝ : ↑((forget k G).obj x✝¹).obj
⊢ 1 x✝ = (Hom.hom ((Iso.hom 1).hom.app x✝¹).hom) x✝
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝³ x✝² : G
x✝¹ : FDRep k G
x✝ : ↑((forget k G).obj x✝¹).obj
⊢ (Hom.hom ((LaxMonoidalFunctor.isoOfComponents (equivApp (x✝³ * x✝²)) ⋯ ⋯ ⋯).hom.hom.app x✝¹).hom) x✝ =
    (Hom.hom
        ((LaxMonoidalFunctor.isoOfComponents (equivApp x✝³) ⋯ ⋯ ⋯ *
                    LaxMonoidalFunctor.isoOfComponents (equivApp x✝²) ⋯ ⋯ ⋯).hom.hom.app
            x✝¹).hom)
      x✝

Tactic:
simp

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝³ x✝² : G
x✝¹ : FDRep k G
x✝ : ↑((forget k G).obj x✝¹).obj
⊢ (x✝¹.ρ x✝³ * x✝¹.ρ x✝²) x✝ =
    (Hom.hom
        ((LaxMonoidalFunctor.isoOfComponents (equivApp x✝³) ⋯ ⋯ ⋯ *
                    LaxMonoidalFunctor.isoOfComponents (equivApp x✝²) ⋯ ⋯ ⋯).hom.hom.app
            x✝¹).hom)
      x✝
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝¹ : G → k
x✝ : G
⊢ { toFun := fun f t ↦ f (t * 1), map_add' := ⋯, map_smul' := ⋯ } x✝¹ x✝ = 1 x✝¹ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
x✝¹ : G → k
x✝ : G
⊢ { toFun := fun f t ↦ f (1⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } x✝¹ x✝ = 1 x✝¹ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
X : FDRep k G
v : ↑X.V
⊢ ∑ s, single 1 1 s • (X.ρ s⁻¹) v = v

Tactic:
simp

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
⊢ mapCocycles₂ f φ ≫ (shortComplexH2 B).moduleCatLeftHomologyData.i =
    (shortComplexH2 A).moduleCatLeftHomologyData.i ≫ cochainsMap₂ f φ

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsDomain k
η : Aut (forget k G)
s : G
hs : (evalAlgHom k (fun a ↦ k) 1).comp (algHomOfRightFDRepComp η) = evalAlgHom k (fun i ↦ k) s
u t : G
nat :
  (forget k G).map (leftRegularFDRepHom t⁻¹) ≫ η.hom.hom.app rightFDRep =
    η.hom.hom.app rightFDRep ≫ (forget k G).map (leftRegularFDRepHom t⁻¹)
⊢ (Hom.hom (η.hom.hom.app (FDRep.of rightRegular)).hom) ((basisFun k G) u) t =
    (leftRegular t⁻¹) ((ConcreteCategory.hom (η.hom.hom.app rightFDRep).hom) (single u 1)) 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : 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
⊢ X i ∈ Set.range X

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: A : Type u_3
σ : Type u_4
inst✝ : CommRing A
I : Ideal (MvPolynomial σ A)
d : σ
⊢ (Ideal.Quotient.mkₐ A I) (X d) = (aeval fun d ↦ (Ideal.Quotient.mk I) (X d)) (X d)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: case ht
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq σ
x : τ →₀ ℕ
a✝ : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ a✝ ∈ {p | mapDomain f p.1 = x ∧ p.2 ∈ Finset.antidiagonal p.1} →
    a✝ ∈ ↑(⋯.toFinset.sup fun y ↦ {y}.product (Finset.antidiagonal y))

Tactic:
simp

Goal state after:
case ht
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq σ
x : τ →₀ ℕ
a✝ : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ mapDomain f a✝.1 = x → a✝.2.1 + a✝.2.2 = a✝.1 → ∃ a b, mapDomain f (a + b) = x ∧ (a + b, a, b) = a✝
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ span ↑{1} = ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: case ht
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq τ
x : τ →₀ ℕ
a✝ : ((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ a✝ ∈ {p | p.1 ∈ Finset.antidiagonal x ∧ p.2 ∈ ⋯.toFinset ×ˢ ⋯.toFinset} →
    a✝ ∈ ↑((Finset.antidiagonal x).sup fun q ↦ {q}.product (⋯.toFinset ×ˢ ⋯.toFinset))

Tactic:
simp

Goal state after:
case ht
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq τ
x : τ →₀ ℕ
a✝ : ((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ a✝.1.1 + a✝.1.2 = x →
    mapDomain f a✝.2.1 = a✝.1.1 →
      mapDomain f a✝.2.2 = a✝.1.2 →
        ∃ a b, mapDomain f a + mapDomain f b = x ∧ ((mapDomain f a, mapDomain f b), a, b) = a✝
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝² : TendstoCofinite f
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
x : τ →₀ ℕ
fst✝¹ fst✝ snd✝ : σ →₀ ℕ
⊢ (fst✝¹, fst✝, snd✝) ∈
      Finset.image
        (fun x ↦
          match x with
          | (fst, b) => (b.1 + b.2, b))
        ⋯.toFinset ↔
    (fst✝¹, fst✝, snd✝) ∈ ⋯.toFinset

Tactic:
simp

Goal state after:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝² : TendstoCofinite f
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
x : τ →₀ ℕ
fst✝¹ fst✝ snd✝ : σ →₀ ℕ
⊢ fst✝ + snd✝ = fst✝¹ → (mapDomain f fst✝ + mapDomain f snd✝ = x ↔ mapDomain f fst✝¹ = x)
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : Semiring R
p q : MvPowerSeries σ R
x : τ →₀ ℕ
⊢ ∀ (p : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)), p ∈ ⋯.toFinset ↔ p.1 ∈ ⋯.toFinset ∧ p.2 ∈ antidiagonal p.1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : Semiring R
p q : MvPowerSeries σ R
x : τ →₀ ℕ
⊢ ∀ (p : ((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)),
    p ∈ ⋯.toFinset ↔ p.1 ∈ antidiagonal x ∧ p.2 ∈ ⋯.toFinset ×ˢ ⋯.toFinset

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : Semiring R
p q : MvPowerSeries σ R
x : τ →₀ ℕ
x✝ : ((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ x✝ ∈ ↑⋯.toFinset →
    ∀ ⦃x₂ : ((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)⦄,
      x₂ ∈ ↑⋯.toFinset →
        ((match x✝ with
            | (fst, b) => (b.1 + b.2, b)) =
            match x₂ with
            | (fst, b) => (b.1 + b.2, b)) →
          x✝ = x₂

Tactic:
simp

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : Semiring R
p q : MvPowerSeries σ R
x : τ →₀ ℕ
x✝ : ((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ x✝.1.1 + x✝.1.2 = x →
    mapDomain f x✝.2.1 = x✝.1.1 →
      mapDomain f x✝.2.2 = x✝.1.2 →
        ∀ (a b : τ →₀ ℕ) (a_1 b_1 : σ →₀ ℕ),
          a + b = x →
            mapDomain f a_1 = a →
              mapDomain f b_1 = b → x✝.2.1 + x✝.2.2 = a_1 + b_1 → x✝.2 = (a_1, b_1) → x✝ = ((a, b), a_1, b_1)
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
f : σ → τ
g : τ → γ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : TendstoCofinite g
p : MvPowerSeries σ R
y : γ →₀ ℕ
⊢ ∀ (p : (τ →₀ ℕ) × (σ →₀ ℕ)),
    p ∈ Finset.image (fun u ↦ (mapDomain f u, u)) ⋯.toFinset ↔ p.1 ∈ ⋯.toFinset ∧ p.2 ∈ ⋯.toFinset

Tactic:
simp

Goal state after:
σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
f : σ → τ
g : τ → γ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : TendstoCofinite g
p : MvPowerSeries σ R
y : γ →₀ ℕ
⊢ ∀ (a : τ →₀ ℕ) (b : σ →₀ ℕ), mapDomain f b = a → (mapDomain (g ∘ f) b = y ↔ mapDomain g a = y)