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₃✝
x✝² : ↑X₁✝
x✝¹ : ↑X₂✝
x✝ : ↑X₃✝
⊢ (((TensorProduct.AlgebraTensorModule.curry
            (TensorProduct.AlgebraTensorModule.curry
              (Hom.hom
                  (ofHom ((Hom.hom (ofHom ((Hom.hom x✝⁵).tensor (Hom.hom x✝⁴)))).tensor (Hom.hom x✝³)) ≫
                    (mkIso (assoc Y₁✝.ρ Y₂✝.ρ Y₃✝.ρ)).hom)).toLinearMap))
          x✝²)
        x✝¹)
      x✝ =
    (((TensorProduct.AlgebraTensorModule.curry
            (TensorProduct.AlgebraTensorModule.curry
              (Hom.hom
                  ((mkIso (assoc X₁✝.ρ X₂✝.ρ X₃✝.ρ)).hom ≫
                    ofHom ((Hom.hom x✝⁵).tensor (Hom.hom (ofHom ((Hom.hom x✝⁴).tensor (Hom.hom x✝³))))))).toLinearMap))
          x✝²)
        x✝¹)
      x✝

Tactic:
;

Goal state after:
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₃✝
x✝² : ↑X₁✝
x✝¹ : ↑X₂✝
x✝ : ↑X₃✝
⊢ (((TensorProduct.AlgebraTensorModule.curry
            (TensorProduct.AlgebraTensorModule.curry
              (Hom.hom
                  (ofHom ((Hom.hom (ofHom ((Hom.hom x✝⁵).tensor (Hom.hom x✝⁴)))).tensor (Hom.hom x✝³)) ≫
                    (mkIso (assoc Y₁✝.ρ Y₂✝.ρ Y₃✝.ρ)).hom)).toLinearMap))
          x✝²)
        x✝¹)
      x✝ =
    (((TensorProduct.AlgebraTensorModule.curry
            (TensorProduct.AlgebraTensorModule.curry
              (Hom.hom
                  ((mkIso (assoc X₁✝.ρ X₂✝.ρ X₃✝.ρ)).hom ≫
                    ofHom ((Hom.hom x✝⁵).tensor (Hom.hom (ofHom ((Hom.hom x✝⁴).tensor (Hom.hom x✝³))))))).toLinearMap))
          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
x✝ : ↥(coindV φ π)
a✝ : H
⊢ ↑({
            toFun := fun x ↦
              match x with
              | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight 1), ⋯⟩,
            map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
          x✝)
      a✝ =
    ↑(1 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
x✝ : ↥(coindV φ π)
a✝ : H
⊢ ↑({
            toFun := fun x ↦
              match x with
              | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight 1), ⋯⟩,
            map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
          x✝)
      a✝ =
    ↑(1 x✝) a✝
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: case mp
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
this : Invertible ↑(Nat.card G)
h : Simple V
⊢ ↑(Nat.card G) = ∑ g, V.character g * V.character g⁻¹

Tactic:
;

Goal state after:
case mp
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
this : Invertible ↑(Nat.card G)
h : Simple V
⊢ ↑(Nat.card G) = ∑ g, V.character g * V.character g⁻¹
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✝ : ↑X✝
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (Hom.hom (ofHom (lTensor (trivial k G k).ρ (Hom.hom x✝¹)) ≫ (mkIso (lid k Y✝.ρ)).hom)).toLinearMap)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (Hom.hom ((mkIso (lid k X✝.ρ)).hom ≫ x✝¹)).toLinearMap) 1) 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✝ : ↑X✝
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (Hom.hom (ofHom (lTensor (trivial k G k).ρ (Hom.hom x✝¹)) ≫ (mkIso (lid k Y✝.ρ)).hom)).toLinearMap)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (Hom.hom ((mkIso (lid k X✝.ρ)).hom ≫ x✝¹)).toLinearMap) 1) 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
h1 h2 : H
x✝ : ↥(coindV φ π)
a✝ : H
⊢ ↑({
            toFun := fun x ↦
              match x with
              | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight (h1 * h2)), ⋯⟩,
            map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
          x✝)
      a✝ =
    ↑(({
              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 := ⋯ })
          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
h1 h2 : H
x✝ : ↥(coindV φ π)
a✝ : H
⊢ ↑({
            toFun := fun x ↦
              match x with
              | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight (h1 * h2)), ⋯⟩,
            map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
          x✝)
      a✝ =
    ↑(({
              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 := ⋯ })
          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✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : ↑X✝
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (Hom.hom (ofHom (rTensor (trivial k G k).ρ (Hom.hom x✝¹)) ≫ (mkIso (rid k Y✝.ρ)).hom)).toLinearMap)
        x✝)
      1 =
    ((TensorProduct.AlgebraTensorModule.curry (Hom.hom ((mkIso (rid k X✝.ρ)).hom ≫ x✝¹)).toLinearMap) x✝) 1

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✝ : ↑X✝
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (Hom.hom (ofHom (rTensor (trivial k G k).ρ (Hom.hom x✝¹)) ≫ (mkIso (rid k Y✝.ρ)).hom)).toLinearMap)
        x✝)
      1 =
    ((TensorProduct.AlgebraTensorModule.curry (Hom.hom ((mkIso (rid k X✝.ρ)).hom ≫ x✝¹)).toLinearMap) x✝) 1
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)
a✝ : G
⊢ ((↑(π g)).comp ((x✝¹ + x✝).comp (ContinuousMap.mulLeft g⁻¹))) a✝ =
    ((↑(π g)).comp (x✝¹.comp (ContinuousMap.mulLeft g⁻¹)) + (↑(π g)).comp (x✝.comp (ContinuousMap.mulLeft g⁻¹))) 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
g : G
x✝¹ x✝ : C(G, V)
a✝ : G
⊢ ((↑(π g)).comp ((x✝¹ + x✝).comp (ContinuousMap.mulLeft g⁻¹))) a✝ =
    ((↑(π g)).comp (x✝¹.comp (ContinuousMap.mulLeft g⁻¹)) + (↑(π g)).comp (x✝.comp (ContinuousMap.mulLeft g⁻¹))) 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✝⁵ x✝⁴ : Rep k G
x✝³ : ↑x✝⁷
x✝² : ↑x✝⁶
x✝¹ : ↑x✝⁵
x✝ : ↑x✝⁴
⊢ ((((TensorProduct.AlgebraTensorModule.curry
              (TensorProduct.AlgebraTensorModule.curry
                (TensorProduct.AlgebraTensorModule.curry
                  (Hom.hom
                      (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)))).toLinearMap)))
            x✝³)
          x✝²)
        x✝¹)
      x✝ =
    ((((TensorProduct.AlgebraTensorModule.curry
              (TensorProduct.AlgebraTensorModule.curry
                (TensorProduct.AlgebraTensorModule.curry
                  (Hom.hom
                      ((mkIso (assoc (of (x✝⁷.ρ.tprod x✝⁶.ρ)).ρ x✝⁵.ρ x✝⁴.ρ)).hom ≫
                        (mkIso (assoc x✝⁷.ρ x✝⁶.ρ (of (x✝⁵.ρ.tprod x✝⁴.ρ)).ρ)).hom)).toLinearMap)))
            x✝³)
          x✝²)
        x✝¹)
      x✝

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝⁷ x✝⁶ x✝⁵ x✝⁴ : Rep k G
x✝³ : ↑x✝⁷
x✝² : ↑x✝⁶
x✝¹ : ↑x✝⁵
x✝ : ↑x✝⁴
⊢ ((((TensorProduct.AlgebraTensorModule.curry
              (TensorProduct.AlgebraTensorModule.curry
                (TensorProduct.AlgebraTensorModule.curry
                  (Hom.hom
                      (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)))).toLinearMap)))
            x✝³)
          x✝²)
        x✝¹)
      x✝ =
    ((((TensorProduct.AlgebraTensorModule.curry
              (TensorProduct.AlgebraTensorModule.curry
                (TensorProduct.AlgebraTensorModule.curry
                  (Hom.hom
                      ((mkIso (assoc (of (x✝⁷.ρ.tprod x✝⁶.ρ)).ρ x✝⁵.ρ x✝⁴.ρ)).hom ≫
                        (mkIso (assoc x✝⁷.ρ x✝⁶.ρ (of (x✝⁵.ρ.tprod x✝⁴.ρ)).ρ)).hom)).toLinearMap)))
            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
g : G
x✝¹ : R
x✝ : C(G, V)
a✝ : G
⊢ ((↑(π g)).comp ((x✝¹ • x✝).comp (ContinuousMap.mulLeft g⁻¹))) a✝ =
    ((RingHom.id R) x✝¹ • (↑(π g)).comp (x✝.comp (ContinuousMap.mulLeft g⁻¹))) 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
g : G
x✝¹ : R
x✝ : C(G, V)
a✝ : G
⊢ ((↑(π g)).comp ((x✝¹ • x✝).comp (ContinuousMap.mulLeft g⁻¹))) a✝ =
    ((RingHom.id R) x✝¹ • (↑(π g)).comp (x✝.comp (ContinuousMap.mulLeft g⁻¹))) a✝
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✝ : C(G, V)
a✝ : G
⊢ ({ toFun := fun f ↦ (↑(π 1)).comp (f.comp (ContinuousMap.mulLeft 1⁻¹)), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x✝)
      a✝ =
    (1 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
x✝ : C(G, V)
a✝ : G
⊢ ({ toFun := fun f ↦ (↑(π 1)).comp (f.comp (ContinuousMap.mulLeft 1⁻¹)), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x✝)
      a✝ =
    (1 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 : Rep k G
x✝¹ : ↑X
x✝ : ↑Y
⊢ (((TensorProduct.AlgebraTensorModule.curry
            (TensorProduct.AlgebraTensorModule.curry
              (Hom.hom
                  ((mkIso (assoc X.ρ (trivial k G k).ρ Y.ρ)).hom ≫
                    ofHom (lTensor X.ρ (Hom.hom (mkIso (lid k Y.ρ)).hom)))).toLinearMap))
          x✝¹)
        1)
      x✝ =
    (((TensorProduct.AlgebraTensorModule.curry
            (TensorProduct.AlgebraTensorModule.curry
              (Hom.hom (ofHom (rTensor Y.ρ (Hom.hom (mkIso (rid k X.ρ)).hom)))).toLinearMap))
          x✝¹)
        1)
      x✝

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Rep k G
x✝¹ : ↑X
x✝ : ↑Y
⊢ (((TensorProduct.AlgebraTensorModule.curry
            (TensorProduct.AlgebraTensorModule.curry
              (Hom.hom
                  ((mkIso (assoc X.ρ (trivial k G k).ρ Y.ρ)).hom ≫
                    ofHom (lTensor X.ρ (Hom.hom (mkIso (lid k Y.ρ)).hom)))).toLinearMap))
          x✝¹)
        1)
      x✝ =
    (((TensorProduct.AlgebraTensorModule.curry
            (TensorProduct.AlgebraTensorModule.curry
              (Hom.hom (ofHom (rTensor Y.ρ (Hom.hom (mkIso (rid k X.ρ)).hom)))).toLinearMap))
          x✝¹)
        1)
      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
x✝² x✝¹ : G
x✝ : C(G, V)
a✝ : G
⊢ ({ toFun := fun f ↦ (↑(π (x✝² * x✝¹))).comp (f.comp (ContinuousMap.mulLeft (x✝² * x✝¹)⁻¹)), map_add' := ⋯,
          map_smul' := ⋯, cont := ⋯ }
        x✝)
      a✝ =
    (({ 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 := ⋯ })
        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
x✝² x✝¹ : G
x✝ : C(G, V)
a✝ : G
⊢ ({ toFun := fun f ↦ (↑(π (x✝² * x✝¹))).comp (f.comp (ContinuousMap.mulLeft (x✝² * x✝¹)⁻¹)), map_add' := ⋯,
          map_smul' := ⋯, cont := ⋯ }
        x✝)
      a✝ =
    (({ 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 := ⋯ })
        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
⊢ Hom.hom (x✝² ◁ 0) = Hom.hom 0

Tactic:
;

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝² x✝¹ x✝ : Rep k G
⊢ Hom.hom (x✝² ◁ 0) = Hom.hom 0
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
⊢ Hom.hom (0 ▷ x✝²) = Hom.hom 0

Tactic:
;

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