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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : Rep k G
x✝² : X₁✝ ⟶ Y₁✝
x✝¹ : X₂✝ ⟶ Y₂✝
x✝ : X₃✝ ⟶ Y₃✝
⊢ ofHom ((Hom.hom (ofHom ((Hom.hom x✝²).tensor (Hom.hom x✝¹)))).tensor (Hom.hom x✝)) ≫
      (mkIso (assoc Y₁✝.ρ Y₂✝.ρ Y₃✝.ρ)).hom =
    (mkIso (assoc X₁✝.ρ X₂✝.ρ X₃✝.ρ)).hom ≫
      ofHom ((Hom.hom x✝²).tensor (Hom.hom (ofHom ((Hom.hom x✝¹).tensor (Hom.hom x✝)))))

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✝ : Rep k G
x✝ : X✝ ⟶ Y✝
⊢ ofHom (lTensor (trivial k G k).ρ (Hom.hom x✝)) ≫ (mkIso (lid k Y✝.ρ)).hom = (mkIso (lid k X✝.ρ)).hom ≫ x✝

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Group G
inst✝² : IsAlgClosed k
inst✝¹ : CharZero k
inst✝ : Fintype G
V : FDRep k G
⊢ Simple V ↔ ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)

Tactic:
by

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
h1 h2 : H
⊢ {
      toFun := fun x ↦
        match x with
        | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight (h1 * h2)), ⋯⟩,
      map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } =
    {
        toFun := fun x ↦
          match x with
          | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight h1), ⋯⟩,
        map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } *
      {
        toFun := fun x ↦
          match x with
          | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight h2), ⋯⟩,
        map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

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✝ : Rep k G
x✝ : X✝ ⟶ Y✝
⊢ ofHom (rTensor (trivial k G k).ρ (Hom.hom x✝)) ≫ (mkIso (rid k Y✝.ρ)).hom = (mkIso (rid k X✝.ρ)).hom ≫ x✝

Tactic:
by

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
g : G
x✝¹ x✝ : C(G, V)
⊢ (↑(π g)).comp ((x✝¹ + x✝).comp (ContinuousMap.mulLeft g⁻¹)) =
    (↑(π g)).comp (x✝¹.comp (ContinuousMap.mulLeft g⁻¹)) + (↑(π g)).comp (x✝.comp (ContinuousMap.mulLeft 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✝³ x✝² x✝¹ x✝ : Rep k G
⊢ ofHom (rTensor x✝.ρ (Hom.hom (mkIso (assoc x✝³.ρ x✝².ρ x✝¹.ρ)).hom)) ≫
      (mkIso (assoc x✝³.ρ (of (x✝².ρ.tprod x✝¹.ρ)).ρ x✝.ρ)).hom ≫
        ofHom (lTensor x✝³.ρ (Hom.hom (mkIso (assoc x✝².ρ x✝¹.ρ x✝.ρ)).hom)) =
    (mkIso (assoc (of (x✝³.ρ.tprod x✝².ρ)).ρ x✝¹.ρ x✝.ρ)).hom ≫
      (mkIso (assoc x✝³.ρ x✝².ρ (of (x✝¹.ρ.tprod x✝.ρ)).ρ)).hom

Tactic:
by

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
g : G
x✝¹ : R
x✝ : C(G, V)
⊢ (↑(π g)).comp ((x✝¹ • x✝).comp (ContinuousMap.mulLeft g⁻¹)) =
    (RingHom.id R) x✝¹ • (↑(π g)).comp (x✝.comp (ContinuousMap.mulLeft g⁻¹))

Tactic:
by

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
⊢ { toFun := fun f ↦ (↑(π 1)).comp (f.comp (ContinuousMap.mulLeft 1⁻¹)), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } = 1

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 : Rep k G
⊢ (mkIso (assoc X.ρ (trivial k G k).ρ Y.ρ)).hom ≫ ofHom (lTensor X.ρ (Hom.hom (mkIso (lid k Y.ρ)).hom)) =
    ofHom (rTensor Y.ρ (Hom.hom (mkIso (rid k X.ρ)).hom))

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 : Rep k G
x : ↑X
y : ↑Y
z : ↑Z
⊢ (Hom.hom (α_ X Y Z).hom).toLinearMap (x ⊗ₜ[k] y ⊗ₜ[k] z) = (↑(assoc X.ρ Y.ρ Z.ρ)).toLinearMap (x ⊗ₜ[k] y ⊗ₜ[k] 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 : Rep k G
⊢ Hom.hom (α_ X Y Z).hom = ↑(assoc X.ρ Y.ρ Z.ρ)

Tactic:
by

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
x✝¹ x✝ : G
⊢ { toFun := fun f ↦ (↑(π (x✝¹ * x✝))).comp (f.comp (ContinuousMap.mulLeft (x✝¹ * x✝)⁻¹)), map_add' := ⋯,
      map_smul' := ⋯, cont := ⋯ } =
    { toFun := fun f ↦ (↑(π x✝¹)).comp (f.comp (ContinuousMap.mulLeft x✝¹⁻¹)), map_add' := ⋯, map_smul' := ⋯,
        cont := ⋯ } *
      { toFun := fun f ↦ (↑(π x✝)).comp (f.comp (ContinuousMap.mulLeft x✝⁻¹)), map_add' := ⋯, map_smul' := ⋯,
        cont := ⋯ }

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✝² x✝¹ x✝ : Rep k G
⊢ x✝² ◁ 0 = 0

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✝² x✝¹ x✝ : Rep k G
⊢ 0 ▷ x✝² = 0

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✝ : Rep k G
x✝¹ x✝ : Y✝ ⟶ Z✝
⊢ X✝ ◁ (x✝¹ + x✝) = X✝ ◁ x✝¹ + X✝ ◁ x✝

Tactic:
by

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✝¹ x✝ : C(G, V)
⊢ (↑f).comp (x✝¹ + x✝) = (↑f).comp x✝¹ + (↑f).comp x✝

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✝ : Rep k G
x✝¹ x✝ : Y✝ ⟶ Z✝
⊢ (x✝¹ + x✝) ▷ X✝ = x✝¹ ▷ X✝ + x✝ ▷ X✝

Tactic:
by

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)
⊢ (↑f).comp (x✝¹ • x✝) = (RingHom.id R) x✝¹ • (↑f).comp x✝

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✝⁴ x✝³ x✝² : Rep k G
x✝¹ : k
x✝ : x✝³ ⟶ x✝²
⊢ x✝⁴ ◁ (x✝¹ • x✝) = x✝¹ • x✝⁴ ◁ x✝

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✝⁴ : k
x✝³ x✝² : Rep k G
x✝¹ : x✝³ ⟶ x✝²
x✝ : Rep k G
⊢ (x✝⁴ • x✝¹) ▷ x✝ = x✝⁴ • x✝¹ ▷ x✝

Tactic:
by

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 π₂
g : G
⊢ { toFun := (↑f).comp, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } ∘SL π₁.coind₁ g =
    π₂.coind₁ g ∘SL { toFun := (↑f).comp, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

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✝³ x✝² x✝¹ : Rep k G
x✝ : x✝² ⟶ x✝¹
⊢ x✝³ ◁ x✝ ≫ (mkIso (Representation.TensorProduct.comm x✝³.ρ x✝¹.ρ)).hom =
    (mkIso (Representation.TensorProduct.comm x✝³.ρ x✝².ρ)).hom ≫ x✝ ▷ x✝³

Tactic:
by

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
⊢ ∀ (g : G),
    { toFun := const G, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } ∘SL π g =
      π.coind₁ g ∘SL { toFun := const G, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

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✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : Rep k G
⊢ x✝¹ ▷ x✝ ≫ (mkIso (Representation.TensorProduct.comm Y✝.ρ x✝.ρ)).hom =
    (mkIso (Representation.TensorProduct.comm X✝.ρ x✝.ρ)).hom ≫ x✝ ◁ x✝¹

Tactic:
by

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
⊢ ⊤ = coindV 1 (trivial R G V)

Tactic:
by

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
g : ↥⊥
⊢ ↑(Submodule.topContEquiv.symm.trans (ContinuousLinearEquiv.ofEq ⊤ (coindV 1 (trivial R G V)) ⋯)) ∘SL
      (trivial R (↥⊥) V).coind₁ g =
    (coind 1 (trivial R G V)) g ∘SL
      ↑(Submodule.topContEquiv.symm.trans (ContinuousLinearEquiv.ofEq ⊤ (coindV 1 (trivial R G V)) ⋯))

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✝⁵ x✝⁴ x✝³ : Rep k G
x✝² : ↑x✝⁵
x✝¹ : ↑x✝⁴
x✝ : ↑x✝³
⊢ (Hom.hom
          ((α_ x✝⁵ x✝⁴ x✝³).hom ≫
            (mkIso (Representation.TensorProduct.comm x✝⁵.ρ (x✝⁴ ⊗ x✝³).ρ)).hom ≫ (α_ x✝⁴ x✝³ x✝⁵).hom)).toLinearMap
      (x✝² ⊗ₜ[k] x✝¹ ⊗ₜ[k] x✝) =
    (Hom.hom
          ((mkIso (Representation.TensorProduct.comm x✝⁵.ρ x✝⁴.ρ)).hom ▷ x✝³ ≫
            (α_ x✝⁴ x✝⁵ x✝³).hom ≫ x✝⁴ ◁ (mkIso (Representation.TensorProduct.comm x✝⁵.ρ x✝³.ρ)).hom)).toLinearMap
      (x✝² ⊗ₜ[k] x✝¹ ⊗ₜ[k] x✝)

Tactic:
by

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✝).hom ≫ (mkIso (Representation.TensorProduct.comm x✝².ρ (x✝¹ ⊗ x✝).ρ)).hom ≫ (α_ x✝¹ x✝ x✝²).hom =
    (mkIso (Representation.TensorProduct.comm x✝².ρ x✝¹.ρ)).hom ▷ x✝ ≫
      (α_ x✝¹ x✝² x✝).hom ≫ x✝¹ ◁ (mkIso (Representation.TensorProduct.comm x✝².ρ x✝.ρ)).hom

Tactic:
by

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
inst✝ : ContinuousSMul R U
π' : ContRepresentation R H W
φ : H →ₜ* G
π : ContRepresentation R G V
h : H
⊢ compCLM R V φ.toContinuousMap ∘SL (π.coind₁.restrict ↑φ) h =
    (π.restrict ↑φ).coind₁ h ∘SL compCLM R V φ.toContinuousMap

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 : Rep k G
⊢ (α_ X Y Z).inv ≫ (mkIso (Representation.TensorProduct.comm (X ⊗ Y).ρ Z.ρ)).hom ≫ (α_ Z X Y).inv =
    X ◁ (mkIso (Representation.TensorProduct.comm Y.ρ Z.ρ)).hom ≫
      (α_ X Z Y).inv ≫ (mkIso (Representation.TensorProduct.comm X.ρ Z.ρ)).hom ▷ Y

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 : Rep k G
⊢ (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)

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✝
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:
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✝
G : Type v
inst✝ : Group G
A B C : Rep k G
x✝ : Rep k G
⊢ ofHom { toLinearMap := (LinearMap.llcomp k ↑A ↑x✝ ↑x✝) (Hom.hom (𝟙 x✝)).toLinearMap, isIntertwining' := ⋯ } =
    𝟙 (of (A.ρ.linHom x✝.ρ))

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✝
G : Type v
inst✝ : Group G
A B C : Rep k G
X✝ Y✝ Z✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ofHom { toLinearMap := (LinearMap.llcomp k ↑A ↑X✝ ↑Z✝) (Hom.hom (x✝¹ ≫ x✝)).toLinearMap, isIntertwining' := ⋯ } =
    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' := ⋯ }

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✝
G : Type v
inst✝ : Group G
A✝ B✝ C✝ : Rep k G
A B C : Rep k G
f : A ⊗ B ⟶ C
g : G
x : ↑B
y : ↑A
⊢ ?m.292

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✝
G : Type v
inst✝ : Group G
A✝ B✝ C✝ : Rep k G
A B C : Rep k G
f : A ⊗ B ⟶ C
g : G
⊢ (TensorProduct.curry (Hom.hom f).toLinearMap).flip ∘ₗ B.ρ g =
    (A.ρ.linHom C.ρ) g ∘ₗ (TensorProduct.curry (Hom.hom f).toLinearMap).flip

Tactic:
ext x y
    simp only [tensor_V, tensor_ρ, LinearMap.coe_comp, Function.comp_apply, LinearMap.flip_apply,
      TensorProduct.curry_apply, Representation.IntertwiningMap.toLinearMap_apply,
      Representation.linHom_apply]
    have := by simpa using (hom_comm_apply f g (A.ρ g⁻¹ y ⊗ₜ[k] x)).symm
    simp [this]

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
A B C : Rep k G
f : A ⊗ B ⟶ C
g : G
⊢ (TensorProduct.curry (Hom.hom f).toLinearMap).flip ∘ₗ B.ρ g =
    (A.ρ.linHom C.ρ) g ∘ₗ (TensorProduct.curry (Hom.hom f).toLinearMap).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✝
G : Type v
inst✝ : Group G
A✝ B✝ C✝ : Rep k G
A B C : Rep k G
f : B ⟶ A.ihom.obj C
g : G
x : ↑A
y : ↑B
⊢ ((TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Hom.hom f).flip ∘ₗ (A.ρ.tprod B.ρ) g) (x ⊗ₜ[k] y) =
    (C.ρ g ∘ₗ (TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Hom.hom f).flip) (x ⊗ₜ[k] y)

Tactic:
by

Goal state after:
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
⊢ (Hom.hom ((ihom.ev A).app B)).toLinearMap =
    (TensorProduct.uncurry (RingHom.id k) (↑A) (↑A →ₗ[k] ↑B) ↑B) LinearMap.id.flip

Tactic:
by

Goal state after: