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

Goal state before:
pp: k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
A B C : Rep k G
f : B ⟶ (ihom A).obj C
⊢ (Hom.hom ((linearHomEquiv A B C).symm f)).toLinearMap =
    (TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Hom.hom f).flip

Tactic:
by

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

Goal state before:
pp: k✝ : Type u
G✝ : Type v
inst✝⁴ : CommRing k✝
inst✝³ : Monoid G✝
k : Type u
inst✝² : Semiring k
G : Type v
inst✝¹ : Group G
inst✝ : Fintype G
A : Rep k G
g : G
⊢ A.ρ.norm ∘ₗ A.ρ g = A.ρ g ∘ₗ A.ρ.norm

Tactic:
by

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

Goal state before:
pp: k : Type u
inst✝² : Semiring k
G : Type v
inst✝¹ : Group G
inst✝ : Fintype G
A B : Rep k G
f : A ⟶ B
⊢ f ≫ B.norm = A.norm ≫ f

Tactic:
by

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
α : Type u'
A : Rep k G
f g : free k G α ⟶ A
h : ∀ (i : α), (Hom.hom f) (single i (MonoidAlgebra.single 1 1)) = (Hom.hom g) (single i (MonoidAlgebra.single 1 1))
⊢ f = g

Tactic:
by

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✝ Y✝ Z : Action (Type u) G
f : X✝ ⟶ Y✝
⊢ (linearization k G).obj Z ◁ (linearization k G).map f ≫ ofHom (μ Z Y✝) =
    ofHom (μ Z X✝) ≫ (linearization k G).map (Z ◁ f)

Tactic:
by

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 Y Z : Action (Type u) G
⊢ ofHom (μ X Y) ▷ (linearization k G).obj Z ≫ ofHom (μ (X ⊗ Y) Z) ≫ (linearization k G).map (α_ X Y Z).hom =
    (α_ ((linearization k G).obj X) ((linearization k G).obj Y) ((linearization k G).obj Z)).hom ≫
      (linearization k G).obj X ◁ ofHom (μ Y Z) ≫ ofHom (μ X (Y ⊗ Z))

Tactic:
by

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 Y Z : Action (Type u) G
⊢ Hom.hom
      (ofHom (δ (X ⊗ Y) Z) ≫
        ofHom (δ X Y) ▷ (linearization k G).obj Z ≫
          (α_ ((linearization k G).obj X) ((linearization k G).obj Y) ((linearization k G).obj Z)).hom) =
    Hom.hom ((linearization k G).map (α_ X Y Z).hom ≫ ofHom (δ X (Y ⊗ Z)) ≫ (linearization k G).obj X ◁ ofHom (δ Y Z))

Tactic:
by

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
A : Rep k G
x : ↑A
g : G
⊢ (Hom.hom (A.leftRegularHomEquiv.symm x)) (MonoidAlgebra.single g 1) = (A.ρ g) x

Tactic:
by

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

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
n : ℕ
⊢ X.d n ≫ X.d (n + 1) = 0

Tactic:
by

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

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
i : ℕ
⊢ X.homogeneousCochains.d i (i + 1) = (invariantsFunctor k G).map (X.d (i + 1))

Tactic:
by

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

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
i : ℕ
σ : ↑(X.homogeneousCochains.X i).toModuleCat
⊢ ↑((TopModuleCat.Hom.hom (X.homogeneousCochains.d i (i + 1))) σ) = (Hom.hom (X.d (i + 1))) ↑σ

Tactic:
by

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₁ : G
h : (QuotientGroup.rightRel S) g₁ g
⊢ g₁ * g⁻¹ ∈ S

Tactic:
by

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
a : ↑A
⊢ (A.indToCoindAux g) a g = a

Tactic:
by

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₁ : G
a : ↑A
h : ¬(QuotientGroup.rightRel S) g₁ g
⊢ (A.indToCoindAux g) a g₁ = 0

Tactic:
by

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₁ : G
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₁ g
x✝ : (QuotientGroup.rightRel S) (↑s * g₁) g
s₁ : ↥S
hs₁ : (fun m ↦ m • g) s₁ = ↑s * g₁
⊢ (fun m ↦ m • g) (s⁻¹ * s₁) = g₁

Tactic:
by

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₁ : G
a : ↑A
s : ↥S
⊢ (A.indToCoindAux g) a (↑s * g₁) = (A.ρ s) ((A.indToCoindAux g) a g₁)

Tactic:
by

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
a : ↑A
s s₁ : ↥S
⊢ (fun m ↦ m • (↑s * g₁)) (s₁ * s⁻¹) = s₁ • g₁

Tactic:
by

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₂ : G
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₂ g₁
x✝ : (QuotientGroup.rightRel S) g₂ (↑s * g₁)
s₁ : ↥S
hs₁ : (fun m ↦ m • (↑s * g₁)) s₁ = g₂
⊢ (fun m ↦ m • g₁) (s₁ * s) = g₂

Tactic:
by

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₂ : G
a : ↑A
s : ↥S
⊢ (A.indToCoindAux (↑s * g₁)) ((A.ρ s) a) g₂ = (A.indToCoindAux g₁) a g₂

Tactic:
by

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₂ g₃ : G
a : ↑A
h : ¬(QuotientGroup.rightRel S) (g₂ * g₃⁻¹) g₁
x✝ : (QuotientGroup.rightRel S) g₂ (g₁ * g₃)
s : ↥S
hs : (fun m ↦ m • (g₁ * g₃)) s = g₂
⊢ (fun m ↦ m • g₁) s = g₂ * g₃⁻¹

Tactic:
by

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₂ g₃ : G
a : ↑A
⊢ (A.indToCoindAux g₁) a (g₂ * g₃⁻¹) = (A.indToCoindAux (g₁ * g₃)) a g₂

Tactic:
by

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₂ g₃ : G
a : ↑A
⊢ (A.indToCoindAux (g₁ * g₂⁻¹)) a g₃ = (A.indToCoindAux g₁) a (g₃ * g₂)

Tactic:
by

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 B : Rep.{u_1, u, v} k ↥S
f : A ⟶ B
g₁ g₂ : G
a : ↑A
⊢ (B.indToCoindAux g₁) ((Hom.hom f) a) g₂ = (Hom.hom f) ((A.indToCoindAux g₁) a g₂)

Tactic:
by

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

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
x✝ : ↥S
⊢ TensorProduct.lift
        ((linearCombination k fun g ↦ LinearMap.codRestrict (coindV S.subtype A.ρ) (A.indToCoindAux g) ⋯) ∘ₗ
          ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
      (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ) x✝ =
    TensorProduct.lift
      ((linearCombination k fun g ↦ LinearMap.codRestrict (coindV S.subtype A.ρ) (A.indToCoindAux g) ⋯) ∘ₗ
        ↑(MonoidAlgebra.coeffLinearEquiv k))

Tactic:
by

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
f : ↑(coind.{u, v, v, w} S.subtype A)
g : Quotient (QuotientGroup.rightRel S)
g₁ g₂ : G
x✝ : g₁ ≈ g₂
s : ↥S
hs : ↑s * g₂ = g₁
⊢ ((tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ) s) (MonoidAlgebra.single g₂ 1 ⊗ₜ[k] ↑f g₂) -
      MonoidAlgebra.single g₂ 1 ⊗ₜ[k] ↑f g₂ =
    ((TensorProduct.mk k (MonoidAlgebra k G) ↑A) (MonoidAlgebra.single g₁ 1)) (↑f g₁) -
      ((TensorProduct.mk k (MonoidAlgebra k G) ↑A) (MonoidAlgebra.single g₂ 1)) (↑f g₂)

Tactic:
by

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

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)
⊢ ∑ g, g.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑(x✝¹ + x✝) g)) ⋯ =
    ∑ g, g.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑x✝¹ g)) ⋯ +
      ∑ g, g.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑x✝ g)) ⋯

Tactic:
by

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

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)
⊢ ∑ g, g.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑(x✝¹ • x✝) g)) ⋯ =
    (RingHom.id k) x✝¹ • ∑ g, g.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑x✝ g)) ⋯

Tactic:
by

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
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
b : G
a✝ : ⟦b⟧ ∈ Finset.univ
hb : ⟦b⟧ ≠ ⟦g⟧
⊢ ↑f b = 0

Tactic:
by

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
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
⊢ A.coindToInd f = (IndV.mk S.subtype A.ρ g) (↑f g)

Tactic:
by

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

Goal state before:
pp: k : Type u
G : Type v
inst✝⁴ : Ring k
inst✝³ : TopologicalSpace k
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
i : ℕ
⊢ resolutionMap (ContinuousMonoidHom.id G) (𝟙 X) i = 𝟙 (X.resolutionX i)

Tactic:
by

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

Goal state before:
pp: k : Type u
G H K : Type v
inst✝¹⁰ : Ring k
inst✝⁹ : TopologicalSpace k
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalGroup H
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : IsTopologicalGroup K
X : TopRep k G
Y : TopRep k H
Z : TopRep k K
φ : H →ₜ* G
ψ : K →ₜ* H
f : res (↑φ) X ⟶ Y
g : res (↑ψ) Y ⟶ Z
i : ℕ
⊢ resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) i =
    (resFunctor ↑ψ).map (resolutionMap φ f i) ≫ resolutionMap ψ g i

Tactic:
by

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

Goal state before:
pp: k : Type u
G H : Type v
inst✝⁷ : Ring k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
X : TopRep k G
Y : TopRep k H
φ : H →ₜ* G
f : res (↑φ) X ⟶ Y
i : ℕ
⊢ resolutionMap φ f i ≫ Y.d i = (resFunctor ↑φ).map (X.d i) ≫ resolutionMap φ f (i + 1)

Tactic:
by

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

Goal state before:
pp: k : Type u
G H K : Type v
inst✝¹⁰ : Ring k
inst✝⁹ : TopologicalSpace k
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalGroup H
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : IsTopologicalGroup K
X : TopRep k G
Y : TopRep k H
Z : TopRep k K
φ : H →ₜ* G
f : res (↑φ) X ⟶ Y
i j : ℕ
hij : i + 1 = j
⊢ invariantsResMap (↑φ) (resolutionMap φ f (i + 1)) ≫ Y.homogeneousCochains.d i j =
    X.homogeneousCochains.d i j ≫ invariantsResMap (↑φ) (resolutionMap φ f (j + 1))

Tactic:
by

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

Goal state before:
pp: k : Type u
G : Type v
inst✝⁴ : Ring k
inst✝³ : TopologicalSpace k
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
⊢ cochainsMap (ContinuousMonoidHom.id G) (𝟙 X) = 𝟙 X.homogeneousCochains

Tactic:
by

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

Goal state before:
pp: k : Type u
G H K : Type v
inst✝¹⁰ : Ring k
inst✝⁹ : TopologicalSpace k
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalGroup H
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : IsTopologicalGroup K
X : TopRep k G
Y : TopRep k H
Z : TopRep k K
φ : H →ₜ* G
ψ : K →ₜ* H
f : res (↑φ) X ⟶ Y
g : res (↑ψ) Y ⟶ Z
⊢ cochainsMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) = cochainsMap φ f ≫ cochainsMap ψ g

Tactic:
by

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

Goal state before:
pp: k : Type u
G : Type v
inst✝⁴ : Ring k
inst✝³ : TopologicalSpace k
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
n : ℕ
⊢ cocyclesMap (ContinuousMonoidHom.id G) (𝟙 X) n = 𝟙 (cocycles X n)

Tactic:
by

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

Goal state before:
pp: k : Type u
G H K : Type v
inst✝¹⁰ : Ring k
inst✝⁹ : TopologicalSpace k
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalGroup H
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : IsTopologicalGroup K
X : TopRep k G
Y : TopRep k H
Z : TopRep k K
φ : H →ₜ* G
ψ : K →ₜ* H
f : res (↑φ) X ⟶ Y
g : res (↑ψ) Y ⟶ Z
n : ℕ
⊢ cocyclesMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) n = cocyclesMap φ f n ≫ cocyclesMap ψ g n

Tactic:
by

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

Goal state before:
pp: k : Type u
G H : Type v
inst✝⁷ : Ring k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
X : TopRep k G
Y : TopRep k H
φ : H →ₜ* G
f : res (↑φ) X ⟶ Y
n : ℕ
⊢ π X n ≫ map φ f n = cocyclesMap φ f n ≫ π Y n

Tactic:
by

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

Goal state before:
pp: k : Type u
G : Type v
inst✝⁴ : Ring k
inst✝³ : TopologicalSpace k
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
n : ℕ
⊢ map (ContinuousMonoidHom.id G) (𝟙 X) n = 𝟙 (continuousCohomology n X)

Tactic:
by

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

Goal state before:
pp: k : Type u
G H K : Type v
inst✝¹⁰ : Ring k
inst✝⁹ : TopologicalSpace k
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalGroup H
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : IsTopologicalGroup K
X : TopRep k G
Y : TopRep k H
Z : TopRep k K
φ : H →ₜ* G
ψ : K →ₜ* H
f : res (↑φ) X ⟶ Y
g : res (↑ψ) Y ⟶ Z
n : ℕ
⊢ map (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) n = map φ f n ≫ map ψ g n

Tactic:
by

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

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
⊢ A.indToCoind ∘ₗ A.coindToInd = LinearMap.id

Tactic:
by

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
⊢ Coinvariants.ker ρ = (ρ g - LinearMap.id).range

Tactic:
by

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

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 ∈ Finset.univ, y.coeff (g⁻¹ * i) = y.coeff (g⁻¹ * i)

Tactic:
by

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
⊢ x = x.coeff.sum fun g r ↦ MonoidAlgebra.single g r - MonoidAlgebra.single 1 r

Tactic:
by

Goal state after:
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 ∈
    Function.support
      ↑(A.indToCoind
          ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
            ((MonoidAlgebra.lsingle g) 1 ⊗ₜ[k] a)))
⊢ x ∈ MulAction.orbit (↥S) g

Tactic:
contrapose hx

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
⊢ x ∉
    Function.support
      ↑(A.indToCoind
          ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
            ((MonoidAlgebra.lsingle g) 1 ⊗ₜ[k] a)))
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

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
⊢ A.coindToInd ∘ₗ A.indToCoind = LinearMap.id

Tactic:
by

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
⊢ Coinvariants.ker (leftRegular k G) = ((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker

Tactic:
by

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
x✝¹ : ↑(leftRegular k G)
x✝ : x✝¹ ∈ (Hom.hom (leftRegular k G).norm).range
w✝ : ↑(leftRegular k G)
h : (Hom.hom (leftRegular k G).norm).toLinearMap w✝ = x✝¹
⊢ x✝¹ ∈ (Hom.hom ((leftRegular k G).applyAsHom g - 𝟙 (leftRegular k G))).ker

Tactic:
by

Goal state after: