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 k G✝
G : Type v'
inst✝¹ : Group G
S : Subgroup G
X Y : Rep k ↥S
f : X ⟶ Y
inst✝ : Epi f
y : ↑((coindFunctor k S.subtype).obj Y)
this : Setoid G := QuotientGroup.rightRel S
s✝ : ↑Y → ↑X
hs : ∀ (b : ↑Y), (Hom.hom f) (s✝ b) = b
i : Quotient this → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : G → ↥S := fun g ↦ ⟨g * (i (Quotient.mk' g))⁻¹, ⋯⟩
hmk : ∀ (s : ↥S) (g : G), Quotient.mk' (↑s * g) = Quotient.mk' g
s : ↥S
g : G
⊢ γ (↑s * g) = s * γ g

Tactic:
ext

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 k G✝
G : Type v'
inst✝¹ : Group G
S : Subgroup G
X Y : Rep k ↥S
f : X ⟶ Y
inst✝ : Epi f
y : ↑((coindFunctor k S.subtype).obj Y)
this : Setoid G := ⋯
s✝ : ↑Y → ↑X
hs : ∀ (b : ↑Y), (Hom.hom f) (s✝ b) = b
i : Quotient this → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : G → ↥S := ⋯
hmk : ∀ (s : ↥S) (g : G), Quotient.mk' (↑s * g) = Quotient.mk' g
s : ↥S
g : G
⊢ ↑(γ (↑s * g)) = ↑(s * γ g)
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 k G
⊢ { toFun := fun f ↦ (resFunctor φ).map (↑(leftRegular k H).leftRegularHomEquiv.symm (MonoidAlgebra.single 1 1)) ≫ f,
      map_add' := ⋯, map_smul' := ⋯ } =
    1

Tactic:
ext

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 k G
x✝¹ : res φ (leftRegular k H) ⟶ A
x✝ : H
⊢ ((Hom.hom
            ({
                toFun := fun f ↦
                  (resFunctor φ).map (↑(leftRegular k H).leftRegularHomEquiv.symm (MonoidAlgebra.single 1 1)) ≫ f,
                map_add' := ⋯, map_smul' := ⋯ }
              x✝¹)).toLinearMap ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((Hom.hom (1 x✝¹)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1
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 k G
x✝¹ x✝ : H
⊢ {
      toFun := fun f ↦
        (resFunctor φ).map (↑(leftRegular k H).leftRegularHomEquiv.symm (MonoidAlgebra.single (x✝¹ * x✝) 1)) ≫ f,
      map_add' := ⋯, map_smul' := ⋯ } =
    {
        toFun := fun f ↦
          (resFunctor φ).map (↑(leftRegular k H).leftRegularHomEquiv.symm (MonoidAlgebra.single x✝¹ 1)) ≫ f,
        map_add' := ⋯, map_smul' := ⋯ } *
      {
        toFun := fun f ↦
          (resFunctor φ).map (↑(leftRegular k H).leftRegularHomEquiv.symm (MonoidAlgebra.single x✝ 1)) ≫ f,
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

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 k G
x✝³ x✝² : H
x✝¹ : res φ (leftRegular k H) ⟶ A
x✝ : H
⊢ ((Hom.hom
            ({
                toFun := fun f ↦
                  (resFunctor φ).map
                      (↑(leftRegular k H).leftRegularHomEquiv.symm (MonoidAlgebra.single (x✝³ * x✝²) 1)) ≫
                    f,
                map_add' := ⋯, map_smul' := ⋯ }
              x✝¹)).toLinearMap ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((Hom.hom
            (({
                  toFun := fun f ↦
                    (resFunctor φ).map (↑(leftRegular k H).leftRegularHomEquiv.symm (MonoidAlgebra.single x✝³ 1)) ≫ f,
                  map_add' := ⋯, map_smul' := ⋯ } *
                {
                  toFun := fun f ↦
                    (resFunctor φ).map (↑(leftRegular k H).leftRegularHomEquiv.symm (MonoidAlgebra.single x✝² 1)) ≫ f,
                  map_add' := ⋯, map_smul' := ⋯ })
              x✝¹)).toLinearMap ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1
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 k G
A B : Rep k G
f : A ⟶ B
h : H
⊢ Linear.rightComp k (res φ (leftRegular k H)) f ∘ₗ (Representation.coind' φ A) h =
    (Representation.coind' φ B) h ∘ₗ Linear.rightComp k (res φ (leftRegular k H)) f

Tactic:
ext

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 k G
A B : Rep k G
f : A ⟶ B
h : H
x✝ : res φ (leftRegular k H) ⟶ A
h✝ : H
⊢ (Hom.hom ((Linear.rightComp k (res φ (leftRegular k H)) f ∘ₗ (Representation.coind' φ A) h) x✝)).toLinearMap
      (MonoidAlgebra.single h✝ 1) =
    (Hom.hom (((Representation.coind' φ B) h ∘ₗ Linear.rightComp k (res φ (leftRegular k H)) f) x✝)).toLinearMap
      (MonoidAlgebra.single h✝ 1)
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 k G
f : ↥(Representation.coindV φ A.ρ)
g : G
⊢ (linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ (Representation.ofMulAction k H H) (φ g) =
    A.ρ g ∘ₗ linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)

Tactic:
ext

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 k G
f : ↥(Representation.coindV φ A.ρ)
g : G
x✝ : H
⊢ (((linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ (Representation.ofMulAction k H H) (φ g)) ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((A.ρ g ∘ₗ linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ MonoidAlgebra.lsingle x✝) 1
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommRing k
inst✝² : Monoid G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ map ρ ρ (IntertwiningMap.id ρ) = LinearMap.id

Tactic:
ext

Goal state after:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommRing k
inst✝² : Monoid G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
x✝ : V
⊢ (map ρ ρ (IntertwiningMap.id ρ) ∘ₗ mk ρ) x✝ = (LinearMap.id ∘ₗ mk ρ) x✝
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 k G
h : H
⊢ ↑(coindVEquiv φ A) ∘ₗ (Representation.coind φ A.ρ) h = (Representation.coind' φ A) h ∘ₗ ↑(coindVEquiv φ A)

Tactic:
ext

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 k G
h : H
x✝ : ↥(Representation.coindV φ A.ρ)
h✝ : H
⊢ (Hom.hom ((↑(coindVEquiv φ A) ∘ₗ (Representation.coind φ A.ρ) h) x✝)).toLinearMap (MonoidAlgebra.single h✝ 1) =
    (Hom.hom (((Representation.coind' φ A) h ∘ₗ ↑(coindVEquiv φ A)) x✝)).toLinearMap (MonoidAlgebra.single h✝ 1)
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W : Type u_4
X : Type u_5
inst✝¹¹ : CommRing k✝
inst✝¹⁰ : Monoid G✝
inst✝⁹ : AddCommGroup V✝
inst✝⁸ : Module k✝ V✝
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k✝ W
inst✝⁵ : AddCommGroup X
inst✝⁴ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ : Representation k✝ G✝ W
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
α : Type u_9
x✝ : G
⊢ mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ (ρ.finsupp α) x✝ = mapRange.linearMap (Coinvariants.mk ρ)

Tactic:
ext

Goal state after:
k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W : Type u_4
X : Type u_5
inst✝¹¹ : CommRing k✝
inst✝¹⁰ : Monoid G✝
inst✝⁹ : AddCommGroup V✝
inst✝⁸ : Module k✝ V✝
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k✝ W
inst✝⁵ : AddCommGroup X
inst✝⁴ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ : Representation k✝ G✝ W
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
α : Type u_9
x✝¹ : G
a✝¹ : α
x✝ : V
a✝ : α
⊢ (((mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ (ρ.finsupp α) x✝¹) ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((mapRange.linearMap (Coinvariants.mk ρ) ∘ₗ lsingle a✝¹) x✝) a✝
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 k G
X✝ Y✝ : Rep k G
x✝ : X✝ ⟶ Y✝
⊢ (coindFunctor k φ).map x✝ ≫ (coindIso φ Y✝).hom = (coindIso φ X✝).hom ≫ (coindFunctor' k φ).map x✝

Tactic:
ext

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 k G
X✝ Y✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : ↑((coindFunctor k φ).obj X✝)
⊢ (Hom.hom ((coindFunctor k φ).map x✝¹ ≫ (coindIso φ Y✝).hom)).toLinearMap x✝ =
    (Hom.hom ((coindIso φ X✝).hom ≫ (coindFunctor' k φ).map x✝¹)).toLinearMap x✝
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W : Type u_4
X : Type u_5
inst✝¹¹ : CommRing k✝
inst✝¹⁰ : Monoid G✝
inst✝⁹ : AddCommGroup V✝
inst✝⁸ : Module k✝ V✝
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k✝ W
inst✝⁵ : AddCommGroup X
inst✝⁴ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ : Representation k✝ G✝ W
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
α : Type u_9
⊢ ρ.coinvariantsToFinsupp α ∘ₗ ρ.finsuppToCoinvariants α = LinearMap.id

Tactic:
ext

Goal state after:
k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W : Type u_4
X : Type u_5
inst✝¹¹ : CommRing k✝
inst✝¹⁰ : Monoid G✝
inst✝⁹ : AddCommGroup V✝
inst✝⁸ : Module k✝ V✝
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k✝ W
inst✝⁵ : AddCommGroup X
inst✝⁴ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ : Representation k✝ G✝ W
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
α : Type u_9
a✝¹ : α
x✝ : V
a✝ : α
⊢ ((((ρ.coinvariantsToFinsupp α ∘ₗ ρ.finsuppToCoinvariants α) ∘ₗ lsingle a✝¹) ∘ₗ Coinvariants.mk ρ) x✝) a✝ =
    (((LinearMap.id ∘ₗ lsingle a✝¹) ∘ₗ Coinvariants.mk ρ) x✝) a✝
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W : Type u_4
X : Type u_5
inst✝¹¹ : CommRing k✝
inst✝¹⁰ : Monoid G✝
inst✝⁹ : AddCommGroup V✝
inst✝⁸ : Module k✝ V✝
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k✝ W
inst✝⁵ : AddCommGroup X
inst✝⁴ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ : Representation k✝ G✝ W
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
α : Type u_9
⊢ ρ.finsuppToCoinvariants α ∘ₗ ρ.coinvariantsToFinsupp α = LinearMap.id

Tactic:
ext

Goal state after:
k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W : Type u_4
X : Type u_5
inst✝¹¹ : CommRing k✝
inst✝¹⁰ : Monoid G✝
inst✝⁹ : AddCommGroup V✝
inst✝⁸ : Module k✝ V✝
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k✝ W
inst✝⁵ : AddCommGroup X
inst✝⁴ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ : Representation k✝ G✝ W
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
α : Type u_9
a✝ : α
x✝ : V
⊢ (((ρ.finsuppToCoinvariants α ∘ₗ ρ.coinvariantsToFinsupp α) ∘ₗ Coinvariants.mk (ρ.finsupp α)) ∘ₗ lsingle a✝) x✝ =
    ((LinearMap.id ∘ₗ Coinvariants.mk (ρ.finsupp α)) ∘ₗ lsingle a✝) x✝
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
X : Type u_5
inst✝¹³ : CommRing k✝
inst✝¹² : Monoid G✝
inst✝¹¹ : AddCommGroup V✝
inst✝¹⁰ : Module k✝ V✝
inst✝⁹ : AddCommGroup W✝
inst✝⁸ : Module k✝ W✝
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ✝ : Representation k✝ G✝ W✝
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
τ : Representation k G W
x✝ : G
⊢ (TensorProduct.lift ((linearCombination k fun g ↦ ρ g⁻¹) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
        ↑(_root_.TensorProduct.comm k V k[G])) ∘ₗ
      (ρ.tprod (leftRegular k G)) x✝ =
    TensorProduct.lift ((linearCombination k fun g ↦ ρ g⁻¹) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
      ↑(_root_.TensorProduct.comm k V k[G])

Tactic:
ext

Goal state after:
k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
X : Type u_5
inst✝¹³ : CommRing k✝
inst✝¹² : Monoid G✝
inst✝¹¹ : AddCommGroup V✝
inst✝¹⁰ : Module k✝ V✝
inst✝⁹ : AddCommGroup W✝
inst✝⁸ : Module k✝ W✝
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ✝ : Representation k✝ G✝ W✝
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
τ : Representation k G W
x✝² : G
x✝¹ : V
x✝ : G
⊢ ((TensorProduct.AlgebraTensorModule.curry
            ((TensorProduct.lift ((linearCombination k fun g ↦ ρ g⁻¹) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
                ↑(_root_.TensorProduct.comm k V k[G])) ∘ₗ
              (ρ.tprod (leftRegular k G)) x✝²))
          x✝¹ ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((TensorProduct.AlgebraTensorModule.curry
            (TensorProduct.lift ((linearCombination k fun g ↦ ρ g⁻¹) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
              ↑(_root_.TensorProduct.comm k V k[G])))
          x✝¹ ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
X : Type u_5
inst✝¹³ : CommRing k✝
inst✝¹² : Monoid G✝
inst✝¹¹ : AddCommGroup V✝
inst✝¹⁰ : Module k✝ V✝
inst✝⁹ : AddCommGroup W✝
inst✝⁸ : Module k✝ W✝
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ✝ : Representation k✝ G✝ W✝
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
τ : Representation k G W
⊢ ρ.ofCoinvariantsTprodLeftRegular ∘ₗ
      Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ (TensorProduct.mk k V k[G]).flip (MonoidAlgebra.single 1 1) =
    LinearMap.id

Tactic:
ext

Goal state after:
k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
X : Type u_5
inst✝¹³ : CommRing k✝
inst✝¹² : Monoid G✝
inst✝¹¹ : AddCommGroup V✝
inst✝¹⁰ : Module k✝ V✝
inst✝⁹ : AddCommGroup W✝
inst✝⁸ : Module k✝ W✝
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ✝ : Representation k✝ G✝ W✝
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
τ : Representation k G W
x✝ : V
⊢ (ρ.ofCoinvariantsTprodLeftRegular ∘ₗ
        Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ (TensorProduct.mk k V k[G]).flip (MonoidAlgebra.single 1 1))
      x✝ =
    LinearMap.id x✝
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
X : Type u_5
inst✝¹³ : CommRing k✝
inst✝¹² : Monoid G✝
inst✝¹¹ : AddCommGroup V✝
inst✝¹⁰ : Module k✝ V✝
inst✝⁹ : AddCommGroup W✝
inst✝⁸ : Module k✝ W✝
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ✝ : Representation k✝ G✝ W✝
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
τ : Representation k G W
⊢ (Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ (TensorProduct.mk k V k[G]).flip (MonoidAlgebra.single 1 1)) ∘ₗ
      ρ.ofCoinvariantsTprodLeftRegular =
    LinearMap.id

Tactic:
ext

Goal state after:
k✝ : Type u_1
G✝ : Type u_2
V✝ : Type u_3
W✝ : Type u_4
X : Type u_5
inst✝¹³ : CommRing k✝
inst✝¹² : Monoid G✝
inst✝¹¹ : AddCommGroup V✝
inst✝¹⁰ : Module k✝ V✝
inst✝⁹ : AddCommGroup W✝
inst✝⁸ : Module k✝ W✝
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module k✝ X
ρ✝ : Representation k✝ G✝ V✝
τ✝ : Representation k✝ G✝ W✝
υ : Representation k✝ G✝ X
k : Type u_6
G : Type u_7
V : Type u_8
W : Type u_9
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
τ : Representation k G W
x✝¹ : V
x✝ : G
⊢ ((TensorProduct.AlgebraTensorModule.curry
            (((Coinvariants.mk (ρ.tprod (leftRegular k G)) ∘ₗ
                  (TensorProduct.mk k V k[G]).flip (MonoidAlgebra.single 1 1)) ∘ₗ
                ρ.ofCoinvariantsTprodLeftRegular) ∘ₗ
              Coinvariants.mk (ρ.tprod (leftRegular k G))))
          x✝¹ ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((TensorProduct.AlgebraTensorModule.curry (LinearMap.id ∘ₗ Coinvariants.mk (ρ.tprod (leftRegular k G)))) x✝¹ ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1
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 k G
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
g : H
⊢ LinearMap.codRestrict (Representation.coindV φ A.ρ) ((LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) ∘ₗ B.ρ g)
      ⋯ =
    (Representation.coind φ A.ρ) g ∘ₗ
      LinearMap.codRestrict (Representation.coindV φ A.ρ) (LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) ⋯

Tactic:
ext

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 k G
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
g : H
x✝¹ : ↑B
x✝ : H
⊢ ↑((LinearMap.codRestrict (Representation.coindV φ A.ρ)
            ((LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) ∘ₗ B.ρ g) ⋯)
          x✝¹)
      x✝ =
    ↑(((Representation.coind φ A.ρ) g ∘ₗ
            LinearMap.codRestrict (Representation.coindV φ A.ρ) (LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h)
              ⋯)
          x✝¹)
      x✝
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
g : G
⊢ (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype ∘ₗ (A.ρ.toCoinvariantsKer S) g =
    A.ρ g ∘ₗ (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype

Tactic:
ext

Goal state after:
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
g : G
x✝ : ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype))
⊢ ((Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype ∘ₗ (A.ρ.toCoinvariantsKer S) g) x✝ =
    (A.ρ g ∘ₗ (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype) x✝
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
x : res φ B ⟶ A
⊢ (fun f ↦
        ofHom
          { toLinearMap := LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap,
            isIntertwining' := ⋯ })
      ((fun f ↦ resCoindToHom φ B A f) x) =
    x

Tactic:
ext

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
x : res φ B ⟶ A
x✝ : ↑(of (MonoidHom.comp B.ρ φ))
⊢ (Hom.hom
          ((fun f ↦
              ofHom
                { toLinearMap := LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap,
                  isIntertwining' := ⋯ })
            ((fun f ↦ resCoindToHom φ B A f) x))).toLinearMap
      x✝ =
    (Hom.hom x).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✝ Y✝ Z✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ModuleCat.ofHom (Coinvariants.map X✝.ρ Z✝.ρ (Hom.hom (x✝¹ ≫ x✝))) =
    ModuleCat.ofHom (Coinvariants.map X✝.ρ Y✝.ρ (Hom.hom x✝¹)) ≫
      ModuleCat.ofHom (Coinvariants.map Y✝.ρ Z✝.ρ (Hom.hom x✝))

Tactic:
ext

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
A B X✝ Y✝ Z✝ : Rep k G
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : ↑X✝
⊢ (ModuleCat.Hom.hom (ModuleCat.ofHom (Coinvariants.map X✝.ρ Z✝.ρ (Hom.hom (x✝² ≫ x✝¹)))) ∘ₗ Coinvariants.mk X✝.ρ) x✝ =
    (ModuleCat.Hom.hom
          (ModuleCat.ofHom (Coinvariants.map X✝.ρ Y✝.ρ (Hom.hom x✝²)) ≫
            ModuleCat.ofHom (Coinvariants.map Y✝.ρ Z✝.ρ (Hom.hom x✝¹))) ∘ₗ
        Coinvariants.mk X✝.ρ)
      x✝
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
z : B ⟶ coind.{u, v, w, max t w} φ A
⊢ (fun f ↦ resCoindToHom φ B A f)
      ((fun f ↦
          ofHom
            { toLinearMap := LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap,
              isIntertwining' := ⋯ })
        z) =
    z

Tactic:
ext

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
z : B ⟶ coind.{u, v, w, max t w} φ A
x✝¹ : ↑B
x✝ : H
⊢ ↑((Hom.hom
              ((fun f ↦ resCoindToHom φ B A f)
                ((fun f ↦
                    ofHom
                      {
                        toLinearMap :=
                          LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Hom.hom f).toLinearMap,
                        isIntertwining' := ⋯ })
                  z))).toLinearMap
          x✝¹)
      x✝ =
    ↑((Hom.hom z).toLinearMap x✝¹) 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
g : G
⊢ ModuleCat.Hom.hom ((coinvariantsMk k G).app X) ∘ₗ X.ρ g =
    (Representation.trivial k G ↑((coinvariantsFunctor k G).obj X)) g ∘ₗ ModuleCat.Hom.hom ((coinvariantsMk k G).app X)

Tactic:
ext

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
A B X : Rep k G
g : G
x✝ : ↑X
⊢ (ModuleCat.Hom.hom ((coinvariantsMk k G).app X) ∘ₗ X.ρ g) x✝ =
    ((Representation.trivial k G ↑((coinvariantsFunctor k G).obj X)) g ∘ₗ
        ModuleCat.Hom.hom ((coinvariantsMk k G).app X))
      x✝
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X : Rep k G
Y : ModuleCat k
f : X ⟶ (trivialFunctor k G).obj Y
⊢ ((coinvariantsAdjunction k G).homEquiv X Y).symm f = desc f

Tactic:
ext

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X : Rep k G
Y : ModuleCat k
f : X ⟶ (trivialFunctor k G).obj Y
x✝ : ↑((forget₂ (Rep k G) (ModuleCat k)).obj X)
⊢ (ModuleCat.Hom.hom ((coinvariantsMk k G).app X ≫ ((coinvariantsAdjunction k G).homEquiv X Y).symm f)) x✝ =
    (ModuleCat.Hom.hom ((coinvariantsMk k G).app X ≫ desc f)) x✝