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

Goal state after:
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✝
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✝ : Y✝ ⟶ Z✝
⊢ Hom.hom ((x✝¹ + x✝) ▷ X✝) = Hom.hom (x✝¹ ▷ X✝ + x✝ ▷ X✝)

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ Z✝ : Rep k G
x✝¹ x✝ : Y✝ ⟶ Z✝
⊢ Hom.hom ((x✝¹ + x✝) ▷ X✝) = Hom.hom (x✝¹ ▷ X✝ + x✝ ▷ X✝)
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:
;

Goal state after:
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✝
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✝¹ : k
x✝ : x✝³ ⟶ x✝²
⊢ Hom.hom (x✝⁴ ◁ (x✝¹ • x✝)) = Hom.hom (x✝¹ • x✝⁴ ◁ x✝)

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝⁴ x✝³ x✝² : Rep k G
x✝¹ : k
x✝ : x✝³ ⟶ x✝²
⊢ Hom.hom (x✝⁴ ◁ (x✝¹ • x✝)) = Hom.hom (x✝¹ • x✝⁴ ◁ x✝)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝⁴ : k
x✝³ x✝² : Rep k G
x✝¹ : x✝³ ⟶ x✝²
x✝ : Rep k G
⊢ Hom.hom ((x✝⁴ • x✝¹) ▷ x✝) = Hom.hom (x✝⁴ • x✝¹ ▷ x✝)

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝⁴ : k
x✝³ x✝² : Rep k G
x✝¹ : x✝³ ⟶ x✝²
x✝ : Rep k G
⊢ Hom.hom ((x✝⁴ • x✝¹) ▷ x✝) = Hom.hom (x✝⁴ • x✝¹ ▷ x✝)
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 π₂
g : G
x✝ : C(G, V)
a✝ : G
⊢ (({ toFun := (↑f).comp, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } ∘SL π₁.coind₁ g) x✝) a✝ =
    ((π₂.coind₁ g ∘SL { toFun := (↑f).comp, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }) x✝) a✝

Tactic:
;

Goal state after:
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 π₂
g : G
x✝ : C(G, V)
a✝ : G
⊢ (({ toFun := (↑f).comp, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } ∘SL π₁.coind₁ g) x✝) a✝ =
    ((π₂.coind₁ g ∘SL { toFun := (↑f).comp, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }) x✝) a✝
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✝¹
⊢ Hom.hom (x✝³ ◁ x✝ ≫ (mkIso (Representation.TensorProduct.comm x✝³.ρ x✝¹.ρ)).hom) =
    Hom.hom ((mkIso (Representation.TensorProduct.comm x✝³.ρ x✝².ρ)).hom ≫ x✝ ▷ x✝³)

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝³ x✝² x✝¹ : Rep k G
x✝ : x✝² ⟶ x✝¹
⊢ Hom.hom (x✝³ ◁ x✝ ≫ (mkIso (Representation.TensorProduct.comm x✝³.ρ x✝¹.ρ)).hom) =
    Hom.hom ((mkIso (Representation.TensorProduct.comm x✝³.ρ x✝².ρ)).hom ≫ x✝ ▷ x✝³)
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : Rep k G
⊢ Hom.hom (x✝¹ ▷ x✝ ≫ (mkIso (Representation.TensorProduct.comm Y✝.ρ x✝.ρ)).hom) =
    Hom.hom ((mkIso (Representation.TensorProduct.comm X✝.ρ x✝.ρ)).hom ≫ x✝ ◁ x✝¹)

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : Rep k G
⊢ Hom.hom (x✝¹ ▷ x✝ ≫ (mkIso (Representation.TensorProduct.comm Y✝.ρ x✝.ρ)).hom) =
    Hom.hom ((mkIso (Representation.TensorProduct.comm X✝.ρ x✝.ρ)).hom ≫ x✝ ◁ x✝¹)
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:
;

Goal state after:
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✝
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Rep k G
⊢ Hom.hom ((β_ X Y).hom ≫ (β_ Y X).hom) = Hom.hom (𝟙 (X ⊗ Y))

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Rep k G
⊢ Hom.hom ((β_ X Y).hom ≫ (β_ Y X).hom) = Hom.hom (𝟙 (X ⊗ Y))
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type v
inst✝ : Group G
A B C : Rep k G
X Y : Rep k G
f : X ⟶ Y
g : G
x✝¹ : ↑A →ₗ[k] ↑X
x✝ : ↑A
⊢ (((LinearMap.llcomp k ↑A ↑X ↑Y) (Hom.hom f).toLinearMap ∘ₗ (A.ρ.linHom X.ρ) g) x✝¹) x✝ =
    (((A.ρ.linHom Y.ρ) g ∘ₗ (LinearMap.llcomp k ↑A ↑X ↑Y) (Hom.hom f).toLinearMap) x✝¹) x✝

Tactic:
;

Goal state after:
k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type v
inst✝ : Group G
A B C : Rep k G
X Y : Rep k G
f : X ⟶ Y
g : G
x✝¹ : ↑A →ₗ[k] ↑X
x✝ : ↑A
⊢ (((LinearMap.llcomp k ↑A ↑X ↑Y) (Hom.hom f).toLinearMap ∘ₗ (A.ρ.linHom X.ρ) g) x✝¹) x✝ =
    (((A.ρ.linHom Y.ρ) g ∘ₗ (LinearMap.llcomp k ↑A ↑X ↑Y) (Hom.hom f).toLinearMap) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type v
inst✝ : Group G
A B C : Rep k G
X Y : Rep k G
f : X ⟶ Y
g : G
⊢ (LinearMap.llcomp k ↑A ↑X ↑Y) (Hom.hom f).toLinearMap ∘ₗ (A.ρ.linHom X.ρ) g =
    (A.ρ.linHom Y.ρ) g ∘ₗ (LinearMap.llcomp k ↑A ↑X ↑Y) (Hom.hom f).toLinearMap

Tactic:
ext; simp [Representation.IntertwiningMap.toLinearMap_apply, ← hom_comm_apply]

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

Goal state before:
pp: k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type v
inst✝ : Group G
A B C : Rep k G
x✝² : Rep k G
x✝¹ : ↑(of (A.ρ.linHom x✝².ρ))
x✝ : ↑A
⊢ ((Hom.hom
            (ofHom
              { toLinearMap := (LinearMap.llcomp k ↑A ↑x✝² ↑x✝²) (Hom.hom (𝟙 x✝²)).toLinearMap,
                isIntertwining' := ⋯ })).toLinearMap
        x✝¹)
      x✝ =
    ((Hom.hom (𝟙 (of (A.ρ.linHom x✝².ρ)))).toLinearMap x✝¹) x✝

Tactic:
;

Goal state after:
k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type v
inst✝ : Group G
A B C : Rep k G
x✝² : Rep k G
x✝¹ : ↑(of (A.ρ.linHom x✝².ρ))
x✝ : ↑A
⊢ ((Hom.hom
            (ofHom
              { toLinearMap := (LinearMap.llcomp k ↑A ↑x✝² ↑x✝²) (Hom.hom (𝟙 x✝²)).toLinearMap,
                isIntertwining' := ⋯ })).toLinearMap
        x✝¹)
      x✝ =
    ((Hom.hom (𝟙 (of (A.ρ.linHom x✝².ρ)))).toLinearMap x✝¹) x✝
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type v
inst✝ : Group G
A B C : Rep k G
X✝ Y✝ Z✝ : Rep k G
x✝³ : X✝ ⟶ Y✝
x✝² : Y✝ ⟶ Z✝
x✝¹ : ↑(of (A.ρ.linHom X✝.ρ))
x✝ : ↑A
⊢ ((Hom.hom
            (ofHom
              { toLinearMap := (LinearMap.llcomp k ↑A ↑X✝ ↑Z✝) (Hom.hom (x✝³ ≫ x✝²)).toLinearMap,
                isIntertwining' := ⋯ })).toLinearMap
        x✝¹)
      x✝ =
    ((Hom.hom
            (ofHom { toLinearMap := (LinearMap.llcomp k ↑A ↑X✝ ↑Y✝) (Hom.hom x✝³).toLinearMap, isIntertwining' := ⋯ } ≫
              ofHom
                { toLinearMap := (LinearMap.llcomp k ↑A ↑Y✝ ↑Z✝) (Hom.hom x✝²).toLinearMap,
                  isIntertwining' := ⋯ })).toLinearMap
        x✝¹)
      x✝

Tactic:
;

Goal state after:
k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type v
inst✝ : Group G
A B C : Rep k G
X✝ Y✝ Z✝ : Rep k G
x✝³ : X✝ ⟶ Y✝
x✝² : Y✝ ⟶ Z✝
x✝¹ : ↑(of (A.ρ.linHom X✝.ρ))
x✝ : ↑A
⊢ ((Hom.hom
            (ofHom
              { toLinearMap := (LinearMap.llcomp k ↑A ↑X✝ ↑Z✝) (Hom.hom (x✝³ ≫ x✝²)).toLinearMap,
                isIntertwining' := ⋯ })).toLinearMap
        x✝¹)
      x✝ =
    ((Hom.hom
            (ofHom { toLinearMap := (LinearMap.llcomp k ↑A ↑X✝ ↑Y✝) (Hom.hom x✝³).toLinearMap, isIntertwining' := ⋯ } ≫
              ofHom
                { toLinearMap := (LinearMap.llcomp k ↑A ↑Y✝ ↑Z✝) (Hom.hom x✝²).toLinearMap,
                  isIntertwining' := ⋯ })).toLinearMap
        x✝¹)
      x✝
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
A B : Rep k G
x✝ : ↑((ihom A ⋙ tensorLeft A).obj B)
⊢ (Hom.hom ((ihom.ev A).app B)).toLinearMap x✝ =
    ((TensorProduct.uncurry (RingHom.id k) (↑A) (↑A →ₗ[k] ↑B) ↑B) LinearMap.id.flip) x✝

Tactic:
;

Goal state after:
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
A B : Rep k G
x✝ : ↑((ihom A ⋙ tensorLeft A).obj B)
⊢ (Hom.hom ((ihom.ev A).app B)).toLinearMap x✝ =
    ((TensorProduct.uncurry (RingHom.id k) (↑A) (↑A →ₗ[k] ↑B) ↑B) LinearMap.id.flip) x✝
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:
;

Goal state after:
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✝
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
x✝ : ↑A
⊢ (Hom.hom (f ≫ B.norm)).toLinearMap x✝ = (Hom.hom (A.norm ≫ f)).toLinearMap x✝

Tactic:
;

Goal state after:
k : Type u
inst✝² : Semiring k
G : Type v
inst✝¹ : Group G
inst✝ : Fintype G
A B : Rep k G
f : A ⟶ B
x✝ : ↑A
⊢ (Hom.hom (f ≫ B.norm)).toLinearMap x✝ = (Hom.hom (A.norm ≫ f)).toLinearMap x✝
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✝
⊢ Hom.hom ((linearization k G).obj Z ◁ (linearization k G).map f ≫ ofHom (μ Z Y✝)) =
    Hom.hom (ofHom (μ Z X✝) ≫ (linearization k G).map (Z ◁ f))

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ Z : Action (Type u) G
f : X✝ ⟶ Y✝
⊢ Hom.hom ((linearization k G).obj Z ◁ (linearization k G).map f ≫ ofHom (μ Z Y✝)) =
    Hom.hom (ofHom (μ Z X✝) ≫ (linearization k G).map (Z ◁ f))
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) ▷ (linearization k G).obj Z ≫ ofHom (μ (X ⊗ Y) Z) ≫ (linearization k G).map (α_ X Y Z).hom) =
    Hom.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:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y Z : Action (Type u) G
⊢ Hom.hom (ofHom (μ X Y) ▷ (linearization k G).obj Z ≫ ofHom (μ (X ⊗ Y) Z) ≫ (linearization k G).map (α_ X Y Z).hom) =
    Hom.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)))
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
s : ↥S
⊢ (fun m ↦ m • g) s * g⁻¹ ∈ S

Tactic:
;

Goal state after:
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
s : ↥S
⊢ (fun m ↦ m • g) s * g⁻¹ ∈ S
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:
simp [S.1.smul_def, smul_eq_mul, mul_assoc]

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

Goal state after:
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✝
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₁
this : ↑f (S.subtype s * g₂) = (A.ρ s) (↑f 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:
;

Goal state after:
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₁
this : ↑f (S.subtype s * g₂) = (A.ρ s) (↑f 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₂)
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:
;

Goal state after:
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✝