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

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A✝ : Rep.{?u.16, u, v} k G
B : Rep.{max w t, u, w} k H
A : Rep.{max w t, u, v} k G
f : B ⟶ coind.{u, v, w, max t w} φ A
g : G
x : ↑B
this : (A.ρ g) (↑((Hom.hom f) x) 1) = ↑((Hom.hom f) x) (φ g * 1)
⊢ ((LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ (MonoidHom.comp B.ρ φ) g)
      x =
    (A.ρ g ∘ₗ LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap) x

Tactic:
have := hom_comm_apply f (φ g) x

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A✝ : Rep.{?u.16, u, v} k G
B : Rep.{max w t, u, w} k H
A : Rep.{max w t, u, v} k G
f : B ⟶ coind.{u, v, w, max t w} φ A
g : G
x : ↑B
this✝ : (A.ρ g) (↑((Hom.hom f) x) 1) = ↑((Hom.hom f) x) (φ g * 1)
this : (Hom.hom f) ((B.ρ (φ g)) x) = ((coind.{u, v, w, max t w} φ A).ρ (φ g)) ((Hom.hom f) x)
⊢ ((LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap) ∘ₗ (MonoidHom.comp B.ρ φ) g)
      x =
    (A.ρ g ∘ₗ LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap) x
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
A B x✝ : Rep k G
⊢ ModuleCat.ofHom (Coinvariants.map x✝.ρ x✝.ρ (Hom.hom (𝟙 x✝))) = 𝟙 (ModuleCat.of k x✝.ρ.Coinvariants)

Tactic:
by simp

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) μ
⊢ UniformIntegrable (fun n ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i) p μ

Tactic:
apply uniformIntegrable_average hp

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg : ∀ (n : ℕ), AEStronglyMeasurable (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) μ
⊢ UniformIntegrable X p μ
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹³ : Monoid G
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : IsTopologicalAddGroup W
inst✝⁴ : Module R W
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
g : G
⊢ ContinuousLinearMap.id R V ∘SL π₁ g = π₁ g ∘SL ContinuousLinearMap.id R V

Tactic:
by simp

Goal state after:
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹³ : Monoid G
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : IsTopologicalAddGroup W
inst✝⁴ : Module R W
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
⊢ ∀ (g : G), 0 ∘SL π₁ g = π₂ g ∘SL 0

Tactic:
by simp

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Semiring k
inst✝ : Monoid G
A B C : Rep k G
f : A ⟶ B
g : B ⟶ C
a : ↑A
⊢ (ConcreteCategory.hom (f ≫ g)) a = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) a)

Tactic:
by simp

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Semiring k
inst✝ : Monoid G
A B : Rep k G
e : A ≅ B
x : ↑A
⊢ (Hom.hom e.inv) ((Hom.hom e.hom) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Semiring k
inst✝ : Monoid G
A B : Rep k G
e : A ≅ B
x : ↑B
⊢ (Hom.hom e.hom) ((Hom.hom e.inv) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝⁷ : Semiring k
inst✝⁶ : Monoid G
X Y : Type w
inst✝⁵ : AddCommGroup X
inst✝⁴ : AddCommGroup Y
inst✝³ : Module k X
inst✝² : Module k Y
ρ : Representation k G X
σ : Representation k G Y
A B C : Rep k G
Z : Type w
inst✝¹ : AddCommGroup Z
inst✝ : Module k Z
τ : Representation k G Z
i : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝⁷ : Semiring k
inst✝⁶ : Monoid G
X Y : Type w
inst✝⁵ : AddCommGroup X
inst✝⁴ : AddCommGroup Y
inst✝³ : Module k X
inst✝² : Module k Y
ρ : Representation k G X
σ : Representation k G Y
A B C : Rep k G
Z : Type w
inst✝¹ : AddCommGroup Z
inst✝ : Module k Z
τ : Representation k G Z
i : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom i.hom) ((ConcreteCategory.hom i.inv) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹³ : Monoid G
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : IsTopologicalAddGroup W
inst✝⁴ : Module R W
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
τ : ContRepresentation R G U
φ : ρ.Equiv σ
⊢ ∀ (g : G), ↑(ContinuousLinearEquiv.refl R V) ∘SL ρ g = ρ g ∘SL ↑(ContinuousLinearEquiv.refl R V)

Tactic:
by simp

Goal state after:
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹³ : Monoid G
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : IsTopologicalAddGroup W
inst✝⁴ : Module R W
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
π : ContRepresentation R G V
⊢ 0 ∈ {v | ∀ (g : G), (π g) v = v}

Tactic:
by simp

Goal state after:
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: R : Type u_1
G✝ : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝²¹ : Monoid G✝
inst✝²⁰ : Ring R
inst✝¹⁹ : AddCommGroup V
inst✝¹⁸ : TopologicalSpace V
inst✝¹⁷ : IsTopologicalAddGroup V
inst✝¹⁶ : Module R V
inst✝¹⁵ : AddCommGroup W
inst✝¹⁴ : TopologicalSpace W
inst✝¹³ : IsTopologicalAddGroup W
inst✝¹² : Module R W
inst✝¹¹ : AddCommGroup U
inst✝¹⁰ : Module R U
inst✝⁹ : TopologicalSpace U
inst✝⁸ : IsTopologicalAddGroup U
H✝ : Type u_6
inst✝⁷ : Monoid H✝
π✝ : ContRepresentation R G✝ V
π' : ContRepresentation R H✝ W
G : Type u_7
H : Type u_8
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace R
inst✝³ : ContinuousSMul R V
inst✝² : ContinuousSMul R W
inst✝¹ : Group H
inst✝ : TopologicalSpace H
φ : G →ₜ* H
π : ContRepresentation R G V
⊢ 0 ∈ {f | ∀ (g : G) (h : H), f (φ g * h) = (π g) (f h)}

Tactic:
by simp

Goal state after:
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: R : Type u_1
G✝ : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝²³ : Monoid G✝
inst✝²² : Ring R
inst✝²¹ : AddCommGroup V
inst✝²⁰ : TopologicalSpace V
inst✝¹⁹ : IsTopologicalAddGroup V
inst✝¹⁸ : Module R V
inst✝¹⁷ : AddCommGroup W
inst✝¹⁶ : TopologicalSpace W
inst✝¹⁵ : IsTopologicalAddGroup W
inst✝¹⁴ : Module R W
inst✝¹³ : AddCommGroup U
inst✝¹² : Module R U
inst✝¹¹ : TopologicalSpace U
inst✝¹⁰ : IsTopologicalAddGroup U
H✝ : Type u_6
inst✝⁹ : Monoid H✝
π✝¹ : ContRepresentation R G✝ V
π' : ContRepresentation R H✝ W
G : Type u_7
H : Type u_8
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalSpace R
inst✝⁵ : ContinuousSMul R V
inst✝⁴ : ContinuousSMul R W
inst✝³ : Group H
inst✝² : TopologicalSpace H
φ : G →ₜ* H
π✝ : ContRepresentation R G V
inst✝¹ : IsTopologicalGroup G
inst✝ : IsTopologicalGroup H
π : ContRepresentation R G V
h : H
x✝¹ x✝ : ↥(coindV φ π)
⊢ (match x✝¹ + x✝ with
    | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight h), ⋯⟩) =
    (match x✝¹ with
      | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight h), ⋯⟩) +
      match x✝ with
      | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight h), ⋯⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: R : Type u_1
G✝ : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝²³ : Monoid G✝
inst✝²² : Ring R
inst✝²¹ : AddCommGroup V
inst✝²⁰ : TopologicalSpace V
inst✝¹⁹ : IsTopologicalAddGroup V
inst✝¹⁸ : Module R V
inst✝¹⁷ : AddCommGroup W
inst✝¹⁶ : TopologicalSpace W
inst✝¹⁵ : IsTopologicalAddGroup W
inst✝¹⁴ : Module R W
inst✝¹³ : AddCommGroup U
inst✝¹² : Module R U
inst✝¹¹ : TopologicalSpace U
inst✝¹⁰ : IsTopologicalAddGroup U
H✝ : Type u_6
inst✝⁹ : Monoid H✝
π✝¹ : ContRepresentation R G✝ V
π' : ContRepresentation R H✝ W
G : Type u_7
H : Type u_8
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalSpace R
inst✝⁵ : ContinuousSMul R V
inst✝⁴ : ContinuousSMul R W
inst✝³ : Group H
inst✝² : TopologicalSpace H
φ : G →ₜ* H
π✝ : ContRepresentation R G V
inst✝¹ : IsTopologicalGroup G
inst✝ : IsTopologicalGroup H
π : ContRepresentation R G V
h : H
x✝¹ : R
x✝ : ↥(coindV φ π)
⊢ (match x✝¹ • x✝ with
    | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight h), ⋯⟩) =
    (RingHom.id R) x✝¹ •
      match x✝ with
      | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight h), ⋯⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝⁵ x✝⁴ x✝³ : Rep k G
x✝² : ↑x✝⁵
x✝¹ : ↑x✝⁴
x✝ : ↑x✝³
⊢ (Hom.hom
          ((α_ x✝⁵ x✝⁴ x✝³).hom ≫
            (mkIso (Representation.TensorProduct.comm x✝⁵.ρ (x✝⁴ ⊗ x✝³).ρ)).hom ≫ (α_ x✝⁴ x✝³ x✝⁵).hom)).toLinearMap
      (x✝² ⊗ₜ[k] x✝¹ ⊗ₜ[k] x✝) =
    (Hom.hom
          ((mkIso (Representation.TensorProduct.comm x✝⁵.ρ x✝⁴.ρ)).hom ▷ x✝³ ≫
            (α_ x✝⁴ x✝⁵ x✝³).hom ≫ x✝⁴ ◁ (mkIso (Representation.TensorProduct.comm x✝⁵.ρ x✝³.ρ)).hom)).toLinearMap
      (x✝² ⊗ₜ[k] x✝¹ ⊗ₜ[k] x✝)

Tactic:
by simp

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: 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
g : G
x✝² : ↑A
x✝¹ : ↥S
x✝ : G
⊢ (A.indToCoindAux g) x✝² (S.subtype x✝¹ * x✝) = (A.ρ x✝¹) ((A.indToCoindAux g) x✝² x✝)

Tactic:
by simp

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: 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
x✝³ x✝² : ↑(coind.{u, v, v, w} S.subtype A)
z : Quotient (QuotientGroup.rightRel S)
x✝¹ : z ∈ Finset.univ
x✝ : G
⊢ ⟦x✝⟧.liftOn
      (fun g ↦
        (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
            (MonoidAlgebra.single g 1 ⊗ₜ[k] ↑x✝³ g) +
          (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
            (MonoidAlgebra.single g 1 ⊗ₜ[k] ↑x✝² g))
      ⋯ =
    ⟦x✝⟧.liftOn
        (fun g ↦
          (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
            (MonoidAlgebra.single g 1 ⊗ₜ[k] ↑x✝³ g))
        ⋯ +
      ⟦x✝⟧.liftOn
        (fun g ↦
          (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
            (MonoidAlgebra.single g 1 ⊗ₜ[k] ↑x✝² g))
        ⋯

Tactic:
by simp

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: 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
x✝³ : k
x✝² : ↑(coind.{u, v, v, w} S.subtype A)
z : Quotient (QuotientGroup.rightRel S)
x✝¹ : z ∈ Finset.univ
x✝ : G
⊢ ⟦x✝⟧.liftOn
      (fun g ↦
        x✝³ •
          (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
            (MonoidAlgebra.single g 1 ⊗ₜ[k] ↑x✝² g))
      ⋯ =
    x✝³ •
      ⟦x✝⟧.liftOn
        (fun g ↦
          (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
            (MonoidAlgebra.single g 1 ⊗ₜ[k] ↑x✝² g))
        ⋯

Tactic:
by simp

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

Goal state before:
pp: 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
α : V
⊢ (ρ g - LinearMap.id) 0 = (fun gv ↦ (ρ gv.1) gv.2 - gv.2) ((fun x ↦ g ^ x) 0, α)

Tactic:
by simp

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

Goal state before:
pp: 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
⊢ ∀ (i : G), i ∈ Finset.univ ↔ g⁻¹ * i ∈ Finset.univ

Tactic:
by simp

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
this✝ : Fintype G
x : MonoidAlgebra k G
hx : x ∈ ((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker
this : x = x.coeff.sum fun g r ↦ MonoidAlgebra.single g r - MonoidAlgebra.single 1 r
g : G
x✝ : x.coeff g ≠ 0
⊢ ((leftRegular k G) g) (MonoidAlgebra.single 1 (x.coeff g)) - MonoidAlgebra.single 1 (x.coeff g) =
    MonoidAlgebra.single g (x.coeff g) - MonoidAlgebra.single 1 (x.coeff g)

Tactic:
by simp

Goal state after:
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
⊢ (ComplexShape.up ℕ).next 0 = 1

Tactic:
by simp

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
m : ℕ
a✝ : QuasiIsoAt (resolution.π k g) m
⊢ (ComplexShape.down ℕ).prev (m + 1) = m + 2

Tactic:
by simp

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
m : ℕ
a✝ : QuasiIsoAt (resolution.π k g) m
⊢ (ComplexShape.down ℕ).next (m + 1) = m

Tactic:
by simp

Goal state after:
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 : ℕ
f : (Fin n → G) → ↑A
h : (ConcreteCategory.hom (d A n)) f = 0
⊢ (ComplexShape.up ℕ).next n = n + 1

Tactic:
by simp

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
f : (Fin n → G) → ↑A
h : (ConcreteCategory.hom (d A n)) f = 0
⊢ (ComplexShape.up ℕ).next n = n + 1

Tactic:
by simp

Goal state after:
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
⊢ (((Representation.ind φ A.ρ).tprod B.ρ) h) ((IndV.mk φ A.ρ h) a ⊗ₜ[k] b) - (IndV.mk φ A.ρ h) a ⊗ₜ[k] 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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

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

Tactic:
by
      have : LinearMap.range X.f.hom.toLinearMap = LinearMap.ker X.g.hom.toLinearMap :=
        (hX.exact.map (forget₂ (Rep k G) (ModuleCat k))).moduleCat_range_eq_ker
      simp [moduleCat_exact_iff_range_eq_ker, LinearMap.range_compLeft,
        LinearMap.ker_compLeft, this]

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 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 0 = 1

Tactic:
by 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:
by 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:
by 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
⊢ (isoCocycles₁ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.i = iCocycles A 1 ≫ (cochainsIso₁ A).hom

Tactic:
simp [isoCocycles₁, iCocycles, HomologicalComplex.iCycles, iCycles]

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:
by 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:
by 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
⊢ π A 0 ≫ (H0Iso A).hom = (cocyclesIso₀ A).hom

Tactic:
by
  simp [H0Iso]

Goal state after: