mathlib-initiative/mathlib-tactics huggingface dataset:
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
π₂ : ContRepresentation R G W
f : π₁ →ⁱL π₂
x✝¹ x✝ : C(G, V)
a✝ : G
⊢ ((↑f).comp (x✝¹ + x✝)) a✝ = ((↑f).comp x✝¹ + (↑f).comp x✝) a✝

Tactic:
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
π₂ : ContRepresentation R G W
f : π₁ →ⁱL π₂
x✝¹ : R
x✝ : C(G, V)
a✝ : G
⊢ ((↑f).comp (x✝¹ • x✝)) a✝ = ((RingHom.id R) x✝¹ • (↑f).comp x✝) a✝

Tactic:
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:
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 Y Z : Rep k G
x✝² : ↑X
x✝¹ : ↑Y
x✝ : ↑Z
⊢ ((TensorProduct.AlgebraTensorModule.curry
          ((TensorProduct.AlgebraTensorModule.curry
              ↑((TensorProduct.assoc k ↑X ↑Y ↑Z).symm ≪≫ₗ
                  (TensorProduct.comm k (TensorProduct k ↑X ↑Y) ↑Z ≪≫ₗ (TensorProduct.assoc k ↑Z ↑X ↑Y).symm)))
            x✝²))
        x✝¹)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
          ((TensorProduct.AlgebraTensorModule.curry
              ((LinearMap.rTensor ↑Y ↑(TensorProduct.comm k ↑X ↑Z) ∘ₗ ↑(TensorProduct.assoc k ↑X ↑Z ↑Y).symm) ∘ₗ
                LinearMap.lTensor ↑X ↑(TensorProduct.comm k ↑Y ↑Z)))
            x✝²))
        x✝¹)
      x✝

Tactic:
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✝
k : Type u
inst✝² : Semiring k
G : Type v
inst✝¹ : Group G
inst✝ : Fintype G
A : Rep k G
g : G
x✝ : ↑A
⊢ (A.ρ.norm ∘ₗ A.ρ g) x✝ = (A.ρ g ∘ₗ A.ρ.norm) x✝

Tactic:
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:
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
x✝³ : ↥S
x✝² : G
x✝¹ : ↑A
x✝ : G
⊢ ↑(((AlgebraTensorModule.curry
                (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✝³) ∘ₗ
              MonoidAlgebra.lsingle x✝²)
            1)
          x✝¹)
      x✝ =
    ↑(((AlgebraTensorModule.curry
                (TensorProduct.lift
                  ((linearCombination k fun g ↦ LinearMap.codRestrict (coindV S.subtype A.ρ) (A.indToCoindAux g) ⋯) ∘ₗ
                    ↑(MonoidAlgebra.coeffLinearEquiv k))) ∘ₗ
              MonoidAlgebra.lsingle x✝²)
            1)
          x✝¹)
      x✝

Tactic:
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:
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:
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
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
⊢ ⟦g⟧.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = (IndV.mk S.subtype A.ρ g) (↑f g)

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case h₁
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
⊢ ⟦g⟧ ∉ Finset.univ → ⟦g⟧.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = 0

Tactic:
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
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
⊢ ↑(A.indToCoind (⟦a⟧.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = ↑g a

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case h₁
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 : ↑(coind.{u, v, v, w} S.subtype A)
a : G
⊢ ⟦a⟧ ∉ Finset.univ → ↑(A.indToCoind (⟦a⟧.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = 0

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

Tactic:
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:
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
A : Rep.{max w u, u, v} k ↥S
g x✝² : G
x✝¹ : ↑A
x✝ : G
⊢ ↑(((AlgebraTensorModule.curry
                ((↑(LinearEquiv.ofLinearMap A.indToCoind A.coindToInd ⋯ ⋯) ∘ₗ (Representation.ind S.subtype A.ρ) g) ∘ₗ
                  Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ)) ∘ₗ
              MonoidAlgebra.lsingle x✝²)
            1)
          x✝¹)
      x✝ =
    ↑(((AlgebraTensorModule.curry
                (((Representation.coind S.subtype A.ρ) g ∘ₗ ↑(LinearEquiv.ofLinearMap A.indToCoind A.coindToInd ⋯ ⋯)) ∘ₗ
                  Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ)) ∘ₗ
              MonoidAlgebra.lsingle x✝²)
            1)
          x✝¹)
      x✝

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

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : CommRing k
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommGroup A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommGroup B
inst✝ : Module k B
τ : Representation k G B
x✝¹ : H
x✝ : A
⊢ ((TensorProduct.AlgebraTensorModule.curry
            (Coinvariants.map (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)
                { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * 1⁻¹),
                  isIntertwining' := ⋯ } ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (1 ∘ₗ Coinvariants.mk (tprod (MonoidHom.comp (leftRegular k H) φ) ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : CommRing k
inst✝³ : Group G
inst✝² : Group H
φ : G →* H
A : Type u_4
inst✝¹ : AddCommGroup A
inst✝ : Module k A
ρ : Representation k G A
h₁ h₂ : H
a : A
⊢ ((ind φ ρ) h₁) ((IndV.mk φ ρ h₂) a) = (IndV.mk φ ρ (h₂ * h₁⁻¹)) a

Tactic:
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
A B : Rep k G
f : A ⟶ B
g x✝¹ : H
x✝ : ↑A
⊢ ((TensorProduct.AlgebraTensorModule.curry
            ((Representation.Coinvariants.map
                  (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                  (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) B.ρ)
                  { toLinearMap := LinearMap.lTensor k[H] (Hom.hom f).toLinearMap, isIntertwining' := ⋯ } ∘ₗ
                (Representation.ind φ A.ρ) g) ∘ₗ
              Representation.Coinvariants.mk
                (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            (((Representation.ind φ B.ρ) g ∘ₗ
                Representation.Coinvariants.map
                  (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                  (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) B.ρ)
                  { toLinearMap := LinearMap.lTensor k[H] (Hom.hom f).toLinearMap, isIntertwining' := ⋯ }) ∘ₗ
              Representation.Coinvariants.mk
                (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝

Tactic:
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 : ℕ
⊢ (freeLiftLEquiv k G (Fin n → G) A).toModuleIso.inv ≫
      0 ≫ (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A).toModuleIso.hom =
    0

Tactic:
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 : ℕ
⊢ (inhomogeneousCochains A).d n (n + 1) = d A n

Tactic:
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:
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:
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
B✝ : Rep k H
A : Rep k G
B : Rep k H
f : A ⟶ res φ B
g x✝¹ : H
x✝ : ↑A
⊢ ((TensorProduct.AlgebraTensorModule.curry
            ((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)))
                  ⋯ ∘ₗ
                (Representation.ind φ A.ρ) g) ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
            ((B.ρ g ∘ₗ
                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)))
                  ⋯) ∘ₗ
              Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
          MonoidAlgebra.lsingle x✝¹)
        1)
      x✝

Tactic:
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
B✝ : Rep k H
A : Rep k G
B : Rep k H
x✝¹ : A ⟶ res φ B
x✝ : ↑(of A.ρ)
⊢ (Hom.hom
          ((fun f ↦ ofHom { toLinearMap := (Hom.hom f).toLinearMap ∘ₗ IndV.mk φ A.ρ 1, isIntertwining' := ⋯ })
            ((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' := ⋯ })
              x✝¹))).toLinearMap
      x✝ =
    (Hom.hom x✝¹).toLinearMap x✝

Tactic:
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
x✝³ x✝² : H
x✝¹ : ↑A
x✝ : ↑B
⊢ (((TensorProduct.AlgebraTensorModule.curry
              (TensorProduct.AlgebraTensorModule.curry
                  (TensorProduct.lift
                      (Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                        (TensorProduct.lift
                          (((lift (↑A →ₗ[k] ↑B →ₗ[k] (A.ρ.tprod (MonoidHom.comp B.ρ φ)).Coinvariants) k H) fun g ↦
                              (A.coinvariantsTensorMk (res φ B)).compl₂ (B.ρ g)) ∘ₗ
                            ↑(MonoidAlgebra.coeffLinearEquiv k)))
                        ⋯) ∘ₗ
                    TensorProduct.map
                      (Coinvariants.map (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                        (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                        {
                          toLinearMap :=
                            LinearMap.rTensor (↑A) (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * x✝³⁻¹),
                          isIntertwining' := ⋯ })
                      (B.ρ x✝³)) ∘ₗ
                Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
            MonoidAlgebra.lsingle x✝²)
          1)
        x✝¹)
      x✝ =
    (((TensorProduct.AlgebraTensorModule.curry
              (TensorProduct.AlgebraTensorModule.curry
                  (TensorProduct.lift
                    (Coinvariants.lift (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)
                      (TensorProduct.lift
                        (((lift (↑A →ₗ[k] ↑B →ₗ[k] (A.ρ.tprod (MonoidHom.comp B.ρ φ)).Coinvariants) k H) fun g ↦
                            (A.coinvariantsTensorMk (res φ B)).compl₂ (B.ρ g)) ∘ₗ
                          ↑(MonoidAlgebra.coeffLinearEquiv k)))
                      ⋯)) ∘ₗ
                Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ)) ∘ₗ
            MonoidAlgebra.lsingle x✝²)
          1)
        x✝¹)
      x✝

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

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
n : ℕ
a✝ : ∀ [h₀ : NeZero n], Even n → (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev n) n
h₀ : NeZero (n + 1)
hi : Even (n + 1)
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev (n + 1)) (n + 1)

Tactic:
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:
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:
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
j : ℕ
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev (2 * j + 1)) (2 * j + 1)

Tactic:
simp

Goal state after: