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
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✝² x✝¹ : S
x✝ : π₁ →ⁱL π₂
⊢ (x✝² + x✝¹) • x✝ = x✝² • x✝ + x✝¹ • x✝

Tactic:
ext

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
π₁ : 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✝³ x✝² : S
x✝¹ : π₁ →ⁱL π₂
x✝ : V
⊢ ((x✝³ + x✝²) • x✝¹).toContinuousLinearMap x✝ = (x✝³ • x✝¹ + x✝² • x✝¹).toContinuousLinearMap 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
π₁ : 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 π₂
⊢ 0 • x✝ = 0

Tactic:
ext

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
π₁ : 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✝
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
⊢ A.ρ (g1 * g2) = A.ρ g1 ∘ₗ A.ρ g2

Tactic:
ext

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

Goal state before:
pp: k : Type u
inst✝¹ : Semiring k
G : Type v
inst✝ : CommMonoid G
A B : Rep k G
f : A ⟶ B
g : G
⊢ A.applyAsHom g ≫ f = f ≫ B.applyAsHom g

Tactic:
ext

Goal state after:
k : Type u
inst✝¹ : Semiring k
G : Type v
inst✝ : CommMonoid G
A B : Rep k G
f : A ⟶ B
g : G
x✝ : ↑A
⊢ (Hom.hom (A.applyAsHom g ≫ f)).toLinearMap x✝ = (Hom.hom (f ≫ B.applyAsHom g)).toLinearMap x✝
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 : G
⊢ (((Finsupp.lift (↑A) k G) fun g ↦ (A.ρ g) x) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
      (Representation.ofMulAction k G G) g =
    A.ρ g ∘ₗ ((Finsupp.lift (↑A) k G) fun g ↦ (A.ρ g) x) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)

Tactic:
ext

Goal state after:
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
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 σ
⊢ φ.trans φ.symm = refl ρ

Tactic:
ext

Goal state after:
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✝
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 σ
⊢ φ.symm.trans φ = refl σ

Tactic:
ext

Goal state after:
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✝
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 G W
φ : H →* G
f : π →ⁱL π'
h : H
⊢ f.toContinuousLinearMap ∘SL (π.restrict φ) h = (π'.restrict φ) h ∘SL f.toContinuousLinearMap

Tactic:
ext

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 G W
φ : H →* G
f : π →ⁱL π'
h : H
x✝ : V
⊢ (f.toContinuousLinearMap ∘SL (π.restrict φ) h) x✝ = ((π'.restrict φ) h ∘SL f.toContinuousLinearMap) x✝
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 : X ⟶ trivial k G PUnit.{w + 1}
⊢ f = default

Tactic:
ext

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommSemiring k
inst✝ : Monoid G
M N O : Rep k G
f : M ⟶ N
r : k
g : N ⟶ O
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
ext

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommSemiring k
inst✝ : Monoid G
M N O : Rep k G
f : M ⟶ N
r : k
g : N ⟶ O
x✝ : ↑M
⊢ (Hom.hom (f ≫ (r • g))).toLinearMap x✝ = (Hom.hom (r • f ≫ g)).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 : Rep k G
f : X ⟶ Y
r : k
⊢ (forget₂ (Rep k G) (ModuleCat k)).map (r • f) = r • (forget₂ (Rep k G) (ModuleCat k)).map f

Tactic:
ext

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Rep k G
f : X ⟶ Y
r : k
x✝ : ↑((forget₂ (Rep k G) (ModuleCat k)).obj X)
⊢ (ModuleCat.Hom.hom ((forget₂ (Rep k G) (ModuleCat k)).map (r • f))) x✝ =
    (ModuleCat.Hom.hom (r • (forget₂ (Rep k G) (ModuleCat k)).map f)) x✝
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
this : Invertible ↑(Nat.card G)
⊢ Simple V ↔ ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)

Tactic:
constructor

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)
⊢ Simple V → ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)

case mpr
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)
⊢ ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G) → Simple V
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:
ext

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

Tactic:
ext

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.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:
ext

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
⊢ {
      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:
ext

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

Tactic:
ext

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)
⊢ (↑(π g)).comp ((x✝¹ + x✝).comp (ContinuousMap.mulLeft g⁻¹)) =
    (↑(π g)).comp (x✝¹.comp (ContinuousMap.mulLeft g⁻¹)) + (↑(π g)).comp (x✝.comp (ContinuousMap.mulLeft g⁻¹))

Tactic:
ext

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
⊢ 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:
ext

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✝