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
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
f : π₂ →ⁱL π₃
g h : π₁ →ⁱL π₂
x✝ : V
⊢ (f.comp (g - h)).toContinuousLinearMap x✝ = (f.comp g - f.comp h).toContinuousLinearMap x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹⁸ : Monoid G
inst✝¹⁷ : Ring R
inst✝¹⁶ : AddCommGroup V
inst✝¹⁵ : TopologicalSpace V
inst✝¹⁴ : IsTopologicalAddGroup V
inst✝¹³ : Module R V
inst✝¹² : AddCommGroup W
inst✝¹¹ : TopologicalSpace W
inst✝¹⁰ : IsTopologicalAddGroup W
inst✝⁹ : Module R W
inst✝⁸ : AddCommGroup U
inst✝⁷ : Module R U
inst✝⁶ : TopologicalSpace U
inst✝⁵ : IsTopologicalAddGroup U
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
S : Type u_7
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S U
inst✝² : SMulCommClass R S U
inst✝¹ : ContinuousConstSMul S U
inst✝ : LinearMap.CompatibleSMul U U S R
s : S
f : π₂ →ⁱL π₃
g : π₁ →ⁱL π₂
x✝ : V
⊢ ((s • f).comp g).toContinuousLinearMap x✝ = (s • f.comp g).toContinuousLinearMap x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝²³ : Monoid G
inst✝²² : Ring R
inst✝²¹ : AddCommGroup V
inst✝²⁰ : TopologicalSpace V
inst✝¹⁹ : IsTopologicalAddGroup V
inst✝¹⁸ : Module R V
inst✝¹⁷ : AddCommGroup W
inst✝¹⁶ : TopologicalSpace W
inst✝¹⁵ : IsTopologicalAddGroup W
inst✝¹⁴ : Module R W
inst✝¹³ : AddCommGroup U
inst✝¹² : Module R U
inst✝¹¹ : TopologicalSpace U
inst✝¹⁰ : IsTopologicalAddGroup U
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
S : Type u_7
inst✝⁹ : Monoid S
inst✝⁸ : DistribMulAction S U
inst✝⁷ : SMulCommClass R S U
inst✝⁶ : ContinuousConstSMul S U
inst✝⁵ : LinearMap.CompatibleSMul U U S R
inst✝⁴ : DistribMulAction S W
inst✝³ : SMulCommClass R S W
inst✝² : ContinuousConstSMul S W
inst✝¹ : LinearMap.CompatibleSMul W W S R
inst✝ : LinearMap.CompatibleSMul W U S R
s : S
f : π₂ →ⁱL π₃
g : π₁ →ⁱL π₂
x✝ : V
⊢ (f.comp (s • g)).toContinuousLinearMap x✝ = (s • f.comp g).toContinuousLinearMap x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹⁸ : Monoid G
inst✝¹⁷ : Ring R
inst✝¹⁶ : AddCommGroup V
inst✝¹⁵ : TopologicalSpace V
inst✝¹⁴ : IsTopologicalAddGroup V
inst✝¹³ : Module R V
inst✝¹² : AddCommGroup W
inst✝¹¹ : TopologicalSpace W
inst✝¹⁰ : IsTopologicalAddGroup W
inst✝⁹ : Module R W
inst✝⁸ : AddCommGroup U
inst✝⁷ : Module R U
inst✝⁶ : TopologicalSpace U
inst✝⁵ : IsTopologicalAddGroup U
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
S : Type u_6
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
x✝¹ : π₁ →ⁱL π₂
x✝ : V
⊢ (1 • x✝¹).toContinuousLinearMap x✝ = x✝¹.toContinuousLinearMap x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹⁸ : Monoid G
inst✝¹⁷ : Ring R
inst✝¹⁶ : AddCommGroup V
inst✝¹⁵ : TopologicalSpace V
inst✝¹⁴ : IsTopologicalAddGroup V
inst✝¹³ : Module R V
inst✝¹² : AddCommGroup W
inst✝¹¹ : TopologicalSpace W
inst✝¹⁰ : IsTopologicalAddGroup W
inst✝⁹ : Module R W
inst✝⁸ : AddCommGroup U
inst✝⁷ : Module R U
inst✝⁶ : TopologicalSpace U
inst✝⁵ : IsTopologicalAddGroup U
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
S : Type u_6
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
x✝¹ : S
x✝ : V
⊢ (x✝¹ • 0).toContinuousLinearMap x✝ = (toContinuousLinearMap 0) x✝

Tactic:
simp

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Semiring k
inst✝ : Monoid G
A B C : Rep k G
f : A ⟶ B
g : B ⟶ C
a : ↑A
⊢ (ConcreteCategory.hom (f ≫ g)) a = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) a)

Tactic:
simp

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Semiring k
inst✝ : Monoid G
A B : Rep k G
e : A ≅ B
x : ↑A
⊢ (Hom.hom e.inv) ((Hom.hom e.hom) x) = x

Tactic:
simp

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Semiring k
inst✝ : Monoid G
A B : Rep k G
e : A ≅ B
x : ↑B
⊢ (Hom.hom e.hom) ((Hom.hom e.inv) x) = x

Tactic:
simp

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

Goal state before:
pp: k : Type u
G : Type v
inst✝⁷ : Semiring k
inst✝⁶ : Monoid G
X Y : Type w
inst✝⁵ : AddCommGroup X
inst✝⁴ : AddCommGroup Y
inst✝³ : Module k X
inst✝² : Module k Y
ρ : Representation k G X
σ : Representation k G Y
A B C : Rep k G
Z : Type w
inst✝¹ : AddCommGroup Z
inst✝ : Module k Z
τ : Representation k G Z
i : A ≅ B
x : ↑A
⊢ (ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) x) = x

Tactic:
simp

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

Goal state before:
pp: k : Type u
G : Type v
inst✝⁷ : Semiring k
inst✝⁶ : Monoid G
X Y : Type w
inst✝⁵ : AddCommGroup X
inst✝⁴ : AddCommGroup Y
inst✝³ : Module k X
inst✝² : Module k Y
ρ : Representation k G X
σ : Representation k G Y
A B C : Rep k G
Z : Type w
inst✝¹ : AddCommGroup Z
inst✝ : Module k Z
τ : Representation k G Z
i : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom i.hom) ((ConcreteCategory.hom i.inv) x) = x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝²³ : Monoid G
inst✝²² : Ring R
inst✝²¹ : AddCommGroup V
inst✝²⁰ : TopologicalSpace V
inst✝¹⁹ : IsTopologicalAddGroup V
inst✝¹⁸ : Module R V
inst✝¹⁷ : AddCommGroup W
inst✝¹⁶ : TopologicalSpace W
inst✝¹⁵ : IsTopologicalAddGroup W
inst✝¹⁴ : Module R W
inst✝¹³ : AddCommGroup U
inst✝¹² : Module R U
inst✝¹¹ : TopologicalSpace U
inst✝¹⁰ : IsTopologicalAddGroup U
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
S✝ : Type u_6
inst✝⁹ : Monoid S✝
inst✝⁸ : DistribMulAction S✝ W
inst✝⁷ : SMulCommClass R S✝ W
inst✝⁶ : ContinuousConstSMul S✝ W
inst✝⁵ : LinearMap.CompatibleSMul W W S✝ R
S : Type u_7
inst✝⁴ : Ring S
inst✝³ : Module S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
x✝¹ : π₁ →ⁱL π₂
x✝ : V
⊢ (0 • x✝¹).toContinuousLinearMap x✝ = (toContinuousLinearMap 0) x✝

Tactic:
simp

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Semiring k
inst✝ : Monoid G
A B C : Rep k G
f : A ⟶ B
g₁ g₂ : B ⟶ C
⊢ f ≫ (g₁ + g₂) = f ≫ g₁ + f ≫ g₂

Tactic:
ext1
  simp [add_hom, Representation.IntertwiningMap.comp_add]

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

Goal state before:
pp: case empty
k : Type u
G : Type v
inst✝¹ : Semiring k
inst✝ : Monoid G
A B : Rep k G
ι : Type u'
f : ι → (A ⟶ B)
⊢ Hom.hom (∑ i ∈ ∅, f i) = ∑ i ∈ ∅, Hom.hom (f i)

Tactic:
simp

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

Goal state before:
pp: case empty
k : Type u
G : Type v
inst✝⁵ : Semiring k
inst✝⁴ : Monoid G
ι : Type u'
M N : Type v'
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module k M
inst✝ : Module k N
σ : Representation k G M
ρ : Representation k G N
f : ι → σ.IntertwiningMap ρ
⊢ ofHom (∑ i ∈ ∅, f i) = ∑ i ∈ ∅, ofHom (f i)

Tactic:
simp

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Semiring k
inst✝ : Monoid G
A : Rep k G
g1 g2 : G
x✝ : ↑A
⊢ (A.ρ (g1 * g2)) x✝ = (A.ρ g1 ∘ₗ A.ρ g2) x✝

Tactic:
simp

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A : Rep k G
x : ↑A
g x✝ : G
⊢ (((((Finsupp.lift (↑A) k G) fun g ↦ (A.ρ g) x) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
          (Representation.ofMulAction k G G) g) ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((A.ρ g ∘ₗ ((Finsupp.lift (↑A) k G) fun g ↦ (A.ρ g) x) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹³ : Monoid G
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : IsTopologicalAddGroup W
inst✝⁴ : Module R W
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
τ : ContRepresentation R G U
φ : ρ.Equiv σ
⊢ ∀ (g : G), ↑(ContinuousLinearEquiv.refl R V) ∘SL ρ g = ρ g ∘SL ↑(ContinuousLinearEquiv.refl R V)

Tactic:
simp

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C X : Rep k G
g : G
⊢ LinearMap.id ∘ₗ X.ρ g = X.ρ g ∘ₗ LinearMap.id

Tactic:
simp

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ Hom.hom
      (ofHom (Representation.IntertwiningMap.inl k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.fst k A.ρ B.ρ)) =
    Hom.hom (𝟙 A)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ : ρ.Equiv σ
x✝ : V
⊢ (φ.trans φ.symm) x✝ = (refl ρ) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ : ρ.Equiv σ
x✝ : W
⊢ (φ.symm.trans φ) x✝ = (refl σ) x✝

Tactic:
simp

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A✝ B✝ C A B : Rep k G
⊢ Hom.hom
      (ofHom (Representation.IntertwiningMap.inr k A.ρ B.ρ) ≫ ofHom (Representation.IntertwiningMap.snd k A.ρ B.ρ)) =
    Hom.hom (𝟙 B)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹³ : Monoid G
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : IsTopologicalAddGroup W
inst✝⁴ : Module R W
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
π : ContRepresentation R G V
⊢ 0 ∈ {v | ∀ (g : G), (π g) v = v}

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
G✝ : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝²¹ : Monoid G✝
inst✝²⁰ : Ring R
inst✝¹⁹ : AddCommGroup V
inst✝¹⁸ : TopologicalSpace V
inst✝¹⁷ : IsTopologicalAddGroup V
inst✝¹⁶ : Module R V
inst✝¹⁵ : AddCommGroup W
inst✝¹⁴ : TopologicalSpace W
inst✝¹³ : IsTopologicalAddGroup W
inst✝¹² : Module R W
inst✝¹¹ : AddCommGroup U
inst✝¹⁰ : Module R U
inst✝⁹ : TopologicalSpace U
inst✝⁸ : IsTopologicalAddGroup U
H✝ : Type u_6
inst✝⁷ : Monoid H✝
π✝ : ContRepresentation R G✝ V
π' : ContRepresentation R H✝ W
G : Type u_7
H : Type u_8
inst✝⁶ : Group G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace R
inst✝³ : ContinuousSMul R V
inst✝² : ContinuousSMul R W
inst✝¹ : Group H
inst✝ : TopologicalSpace H
φ : G →ₜ* H
π : ContRepresentation R G V
⊢ 0 ∈ {f | ∀ (g : G) (h : H), f (φ g * h) = (π g) (f h)}

Tactic:
simp

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C X : Rep k G
f : trivial k G PUnit.{w + 1} ⟶ X
⊢ (Hom.hom f).toLinearMap 0 = (Hom.hom default).toLinearMap 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
G✝ : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝²³ : Monoid G✝
inst✝²² : Ring R
inst✝²¹ : AddCommGroup V
inst✝²⁰ : TopologicalSpace V
inst✝¹⁹ : IsTopologicalAddGroup V
inst✝¹⁸ : Module R V
inst✝¹⁷ : AddCommGroup W
inst✝¹⁶ : TopologicalSpace W
inst✝¹⁵ : IsTopologicalAddGroup W
inst✝¹⁴ : Module R W
inst✝¹³ : AddCommGroup U
inst✝¹² : Module R U
inst✝¹¹ : TopologicalSpace U
inst✝¹⁰ : IsTopologicalAddGroup U
H✝ : Type u_6
inst✝⁹ : Monoid H✝
π✝¹ : ContRepresentation R G✝ V
π' : ContRepresentation R H✝ W
G : Type u_7
H : Type u_8
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalSpace R
inst✝⁵ : ContinuousSMul R V
inst✝⁴ : ContinuousSMul R W
inst✝³ : Group H
inst✝² : TopologicalSpace H
φ : G →ₜ* H
π✝ : ContRepresentation R G V
inst✝¹ : IsTopologicalGroup G
inst✝ : IsTopologicalGroup H
π : ContRepresentation R G V
h : H
x✝¹ x✝ : ↥(coindV φ π)
⊢ (match x✝¹ + x✝ with
    | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight h), ⋯⟩) =
    (match x✝¹ with
      | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight h), ⋯⟩) +
      match x✝ with
      | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight h), ⋯⟩

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
G✝ : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝²³ : Monoid G✝
inst✝²² : Ring R
inst✝²¹ : AddCommGroup V
inst✝²⁰ : TopologicalSpace V
inst✝¹⁹ : IsTopologicalAddGroup V
inst✝¹⁸ : Module R V
inst✝¹⁷ : AddCommGroup W
inst✝¹⁶ : TopologicalSpace W
inst✝¹⁵ : IsTopologicalAddGroup W
inst✝¹⁴ : Module R W
inst✝¹³ : AddCommGroup U
inst✝¹² : Module R U
inst✝¹¹ : TopologicalSpace U
inst✝¹⁰ : IsTopologicalAddGroup U
H✝ : Type u_6
inst✝⁹ : Monoid H✝
π✝¹ : ContRepresentation R G✝ V
π' : ContRepresentation R H✝ W
G : Type u_7
H : Type u_8
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalSpace R
inst✝⁵ : ContinuousSMul R V
inst✝⁴ : ContinuousSMul R W
inst✝³ : Group H
inst✝² : TopologicalSpace H
φ : G →ₜ* H
π✝ : ContRepresentation R G V
inst✝¹ : IsTopologicalGroup G
inst✝ : IsTopologicalGroup H
π : ContRepresentation R G V
h : H
x✝¹ : R
x✝ : ↥(coindV φ π)
⊢ (match x✝¹ • x✝ with
    | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight h), ⋯⟩) =
    (RingHom.id R) x✝¹ •
      match x✝ with
      | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight h), ⋯⟩

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
G✝ : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝²³ : Monoid G✝
inst✝²² : Ring R
inst✝²¹ : AddCommGroup V
inst✝²⁰ : TopologicalSpace V
inst✝¹⁹ : IsTopologicalAddGroup V
inst✝¹⁸ : Module R V
inst✝¹⁷ : AddCommGroup W
inst✝¹⁶ : TopologicalSpace W
inst✝¹⁵ : IsTopologicalAddGroup W
inst✝¹⁴ : Module R W
inst✝¹³ : AddCommGroup U
inst✝¹² : Module R U
inst✝¹¹ : TopologicalSpace U
inst✝¹⁰ : IsTopologicalAddGroup U
H✝ : Type u_6
inst✝⁹ : Monoid H✝
π✝¹ : ContRepresentation R G✝ V
π' : ContRepresentation R H✝ W
G : Type u_7
H : Type u_8
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalSpace R
inst✝⁵ : ContinuousSMul R V
inst✝⁴ : ContinuousSMul R W
inst✝³ : Group H
inst✝² : TopologicalSpace H
φ : G →ₜ* H
π✝ : ContRepresentation R G V
inst✝¹ : IsTopologicalGroup G
inst✝ : IsTopologicalGroup H
π : ContRepresentation R G V
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:
simp

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X₁✝ X₂✝ X₃✝ 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:
simp

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

Goal state before:
pp: R : Type u_1
G✝ : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝²³ : Monoid G✝
inst✝²² : Ring R
inst✝²¹ : AddCommGroup V
inst✝²⁰ : TopologicalSpace V
inst✝¹⁹ : IsTopologicalAddGroup V
inst✝¹⁸ : Module R V
inst✝¹⁷ : AddCommGroup W
inst✝¹⁶ : TopologicalSpace W
inst✝¹⁵ : IsTopologicalAddGroup W
inst✝¹⁴ : Module R W
inst✝¹³ : AddCommGroup U
inst✝¹² : Module R U
inst✝¹¹ : TopologicalSpace U
inst✝¹⁰ : IsTopologicalAddGroup U
H✝ : Type u_6
inst✝⁹ : Monoid H✝
π✝¹ : ContRepresentation R G✝ V
π' : ContRepresentation R H✝ W
G : Type u_7
H : Type u_8
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalSpace R
inst✝⁵ : ContinuousSMul R V
inst✝⁴ : ContinuousSMul R W
inst✝³ : Group H
inst✝² : TopologicalSpace H
φ : G →ₜ* H
π✝ : ContRepresentation R G V
inst✝¹ : IsTopologicalGroup G
inst✝ : IsTopologicalGroup H
π : ContRepresentation R G V
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:
simp

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝⁷ x✝⁶ x✝⁵ 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:
simp

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

Goal state before:
pp: R : Type u_1
G✝ : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝²³ : Monoid G✝
inst✝²² : Ring R
inst✝²¹ : AddCommGroup V
inst✝²⁰ : TopologicalSpace V
inst✝¹⁹ : IsTopologicalAddGroup V
inst✝¹⁸ : Module R V
inst✝¹⁷ : AddCommGroup W
inst✝¹⁶ : TopologicalSpace W
inst✝¹⁵ : IsTopologicalAddGroup W
inst✝¹⁴ : Module R W
inst✝¹³ : AddCommGroup U
inst✝¹² : Module R U
inst✝¹¹ : TopologicalSpace U
inst✝¹⁰ : IsTopologicalAddGroup U
H✝ : Type u_6
inst✝⁹ : Monoid H✝
π✝¹ : ContRepresentation R G✝ V
π' : ContRepresentation R H✝ W
G : Type u_7
H : Type u_8
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalSpace R
inst✝⁵ : ContinuousSMul R V
inst✝⁴ : ContinuousSMul R W
inst✝³ : Group H
inst✝² : TopologicalSpace H
φ : G →ₜ* H
π✝ : ContRepresentation R G V
inst✝¹ : IsTopologicalGroup G
inst✝ : IsTopologicalGroup H
π : ContRepresentation R G V
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:
simp

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

Goal state before:
pp: R : Type u_1
G✝ : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝²³ : Monoid G✝
inst✝²² : Ring R
inst✝²¹ : AddCommGroup V
inst✝²⁰ : TopologicalSpace V
inst✝¹⁹ : IsTopologicalAddGroup V
inst✝¹⁸ : Module R V
inst✝¹⁷ : AddCommGroup W
inst✝¹⁶ : TopologicalSpace W
inst✝¹⁵ : IsTopologicalAddGroup W
inst✝¹⁴ : Module R W
inst✝¹³ : AddCommGroup U
inst✝¹² : Module R U
inst✝¹¹ : TopologicalSpace U
inst✝¹⁰ : IsTopologicalAddGroup U
H✝ : Type u_6
inst✝⁹ : Monoid H✝
π✝¹ : ContRepresentation R G✝ V
π' : ContRepresentation R H✝ W
G : Type u_7
H : Type u_8
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalSpace R
inst✝⁵ : ContinuousSMul R V
inst✝⁴ : ContinuousSMul R W
inst✝³ : Group H
inst✝² : TopologicalSpace H
φ : G →ₜ* H
π✝ : ContRepresentation R G V
inst✝¹ : IsTopologicalGroup G
inst✝ : IsTopologicalGroup H
π : ContRepresentation R G V
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:
simp

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : 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:
simp

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝² x✝¹ x✝ : Rep k G
⊢ Hom.hom (x✝² ◁ 0) = Hom.hom 0

Tactic:
simp

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

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

Tactic:
simp

Goal state after: