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

Goal state before:
pp: R : Type u_1
G✝ : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝²³ : Monoid G✝
inst✝²² : Ring R
inst✝²¹ : AddCommGroup V
inst✝²⁰ : TopologicalSpace V
inst✝¹⁹ : IsTopologicalAddGroup V
inst✝¹⁸ : Module R V
inst✝¹⁷ : AddCommGroup W
inst✝¹⁶ : TopologicalSpace W
inst✝¹⁵ : IsTopologicalAddGroup W
inst✝¹⁴ : Module R W
inst✝¹³ : AddCommGroup U
inst✝¹² : Module R U
inst✝¹¹ : TopologicalSpace U
inst✝¹⁰ : IsTopologicalAddGroup U
H✝ : Type u_6
inst✝⁹ : Monoid H✝
π✝¹ : ContRepresentation R G✝ V
π' : ContRepresentation R H✝ W
G : Type u_7
H : Type u_8
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalSpace R
inst✝⁵ : ContinuousSMul R V
inst✝⁴ : ContinuousSMul R W
inst✝³ : Group H
inst✝² : TopologicalSpace H
φ : G →ₜ* H
π✝ : ContRepresentation R G V
inst✝¹ : IsTopologicalGroup G
inst✝ : IsTopologicalGroup H
π : ContRepresentation R G V
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:
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✝¹ : 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
⊢ { toFun := fun f ↦ (↑(π 1)).comp (f.comp (ContinuousMap.mulLeft 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✝ : 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
⊢ (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:
ext

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
⊢ { 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:
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✝² 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.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:
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
π₂ : ContRepresentation R G W
f : π₁ →ⁱL π₂
x✝¹ x✝ : C(G, V)
a✝ : G
⊢ ((↑f).comp (x✝¹ + x✝)) a✝ = ((↑f).comp x✝¹ + (↑f).comp x✝) a✝
Module: Mathlib.RepresentationTheory.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:
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
π₂ : ContRepresentation R G W
f : π₁ →ⁱL π₂
x✝¹ : R
x✝ : C(G, V)
a✝ : G
⊢ ((↑f).comp (x✝¹ • x✝)) a✝ = ((RingHom.id R) x✝¹ • (↑f).comp x✝) a✝
Module: Mathlib.RepresentationTheory.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:
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
π₂ : ContRepresentation R G W
f : π₁ →ⁱL π₂
g : G
x✝ : C(G, V)
a✝ : G
⊢ (({ toFun := (↑f).comp, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } ∘SL π₁.coind₁ g) x✝) a✝ =
    ((π₂.coind₁ g ∘SL { toFun := (↑f).comp, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }) x✝) a✝
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y Z : Rep k G
⊢ ↑((TensorProduct.assoc k ↑X ↑Y ↑Z).symm ≪≫ₗ
        (TensorProduct.comm k (TensorProduct k ↑X ↑Y) ↑Z ≪≫ₗ (TensorProduct.assoc k ↑Z ↑X ↑Y).symm)) =
    (LinearMap.rTensor ↑Y ↑(TensorProduct.comm k ↑X ↑Z) ∘ₗ ↑(TensorProduct.assoc k ↑X ↑Z ↑Y).symm) ∘ₗ
      LinearMap.lTensor ↑X ↑(TensorProduct.comm k ↑Y ↑Z)

Tactic:
ext

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y Z : Rep k G
x✝² : ↑X
x✝¹ : ↑Y
x✝ : ↑Z
⊢ ((TensorProduct.AlgebraTensorModule.curry
          ((TensorProduct.AlgebraTensorModule.curry
              ↑((TensorProduct.assoc k ↑X ↑Y ↑Z).symm ≪≫ₗ
                  (TensorProduct.comm k (TensorProduct k ↑X ↑Y) ↑Z ≪≫ₗ (TensorProduct.assoc k ↑Z ↑X ↑Y).symm)))
            x✝²))
        x✝¹)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry
          ((TensorProduct.AlgebraTensorModule.curry
              ((LinearMap.rTensor ↑Y ↑(TensorProduct.comm k ↑X ↑Z) ∘ₗ ↑(TensorProduct.assoc k ↑X ↑Z ↑Y).symm) ∘ₗ
                LinearMap.lTensor ↑X ↑(TensorProduct.comm k ↑Y ↑Z)))
            x✝²))
        x✝¹)
      x✝
Module: Mathlib.RepresentationTheory.Rep.Basic

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

Tactic:
ext

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

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

Tactic:
ext

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

Goal state before:
pp: k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type v
inst✝ : Group G
A B C : Rep k G
X✝ Y✝ Z✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ 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:
ext

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

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

Tactic:
ext

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

Goal state before:
pp: k✝ : Type u
G✝ : Type v
inst✝⁴ : CommRing k✝
inst✝³ : Monoid G✝
k : Type u
inst✝² : Semiring k
G : Type v
inst✝¹ : Group G
inst✝ : Fintype G
A : Rep k G
g : G
⊢ A.ρ.norm ∘ₗ A.ρ g = A.ρ g ∘ₗ A.ρ.norm

Tactic:
ext

Goal state after:
k✝ : Type u
G✝ : Type v
inst✝⁴ : CommRing k✝
inst✝³ : Monoid G✝
k : Type u
inst✝² : Semiring k
G : Type v
inst✝¹ : Group G
inst✝ : Fintype G
A : Rep k G
g : G
x✝ : ↑A
⊢ (A.ρ.norm ∘ₗ A.ρ g) x✝ = (A.ρ g ∘ₗ A.ρ.norm) x✝
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
inst✝² : Semiring k
G : Type v
inst✝¹ : Group G
inst✝ : Fintype G
A B : Rep k G
f : A ⟶ B
⊢ f ≫ B.norm = A.norm ≫ f

Tactic:
ext

Goal state after:
k : Type u
inst✝² : Semiring k
G : Type v
inst✝¹ : Group G
inst✝ : Fintype G
A B : Rep k G
f : A ⟶ B
x✝ : ↑A
⊢ (Hom.hom (f ≫ B.norm)).toLinearMap x✝ = (Hom.hom (A.norm ≫ f)).toLinearMap x✝
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Basic

Goal state before:
pp: case zero
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
⊢ X.d 0 ≫ X.d (0 + 1) = 0

Tactic:
ext

Goal state after:
case zero
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
x✝ : ↑(X.resolutionX 0)
a✝¹ a✝ : G
⊢ (((Hom.hom (X.d 0 ≫ X.d (0 + 1))).toContinuousLinearMap x✝) a✝¹) a✝ = (((Hom.hom 0).toContinuousLinearMap x✝) a✝¹) a✝
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Basic

Goal state before:
pp: case succ
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι -
      (ofHom (X.resolutionX (n + 1)).ρ.coind₁ι ≫ (coind₁Functor k G).map (X.d (n + 1)) - (coind₁Functor k G).map 0) =
    0

Tactic:
Functor.map_zero,

Goal state after:
case succ
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι -
      (ofHom (X.resolutionX (n + 1)).ρ.coind₁ι ≫ (coind₁Functor k G).map (X.d (n + 1)) - 0) =
    0
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
x✝ : ↥S
⊢ TensorProduct.lift
        ((linearCombination k fun g ↦ LinearMap.codRestrict (coindV S.subtype A.ρ) (A.indToCoindAux g) ⋯) ∘ₗ
          ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
      (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ) x✝ =
    TensorProduct.lift
      ((linearCombination k fun g ↦ LinearMap.codRestrict (coindV S.subtype A.ρ) (A.indToCoindAux g) ⋯) ∘ₗ
        ↑(MonoidAlgebra.coeffLinearEquiv k))

Tactic:
ext

Goal state after:
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
x✝³ : ↥S
x✝² : G
x✝¹ : ↑A
x✝ : G
⊢ ↑(((AlgebraTensorModule.curry
                (TensorProduct.lift
                    ((linearCombination k fun g ↦ LinearMap.codRestrict (coindV S.subtype A.ρ) (A.indToCoindAux g) ⋯) ∘ₗ
                      ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
                  (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ) x✝³) ∘ₗ
              MonoidAlgebra.lsingle x✝²)
            1)
          x✝¹)
      x✝ =
    ↑(((AlgebraTensorModule.curry
                (TensorProduct.lift
                  ((linearCombination k fun g ↦ LinearMap.codRestrict (coindV S.subtype A.ρ) (A.indToCoindAux g) ⋯) ∘ₗ
                    ↑(MonoidAlgebra.coeffLinearEquiv k))) ∘ₗ
              MonoidAlgebra.lsingle x✝²)
            1)
          x✝¹)
      x✝