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

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
⊢ lTensor ρ 0 = 0

Tactic:
ext

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
x✝¹ : V
x✝ : W
⊢ ((TensorProduct.AlgebraTensorModule.curry (lTensor ρ 0).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (toLinearMap 0)) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
⊢ rTensor ρ (id σ) = id (σ.tprod ρ)

Tactic:
ext

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
x✝¹ : W
x✝ : V
⊢ ((TensorProduct.AlgebraTensorModule.curry (rTensor ρ (id σ)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (id (σ.tprod ρ)).toLinearMap) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
⊢ rTensor ρ 0 = 0

Tactic:
ext

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
x✝¹ : W
x✝ : V
⊢ ((TensorProduct.AlgebraTensorModule.curry (rTensor ρ 0).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (toLinearMap 0)) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
Q : Type u_7
inst✝¹ : AddCommMonoid Q
inst✝ : Module A Q
υ : Representation A G Q
f : ρ.IntertwiningMap τ
g : σ.IntertwiningMap υ
⊢ (rTensor υ f).comp (lTensor ρ g) = f.tensor g

Tactic:
ext

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
Q : Type u_7
inst✝¹ : AddCommMonoid Q
inst✝ : Module A Q
υ : Representation A G Q
f : ρ.IntertwiningMap τ
g : σ.IntertwiningMap υ
x✝¹ : V
x✝ : W
⊢ ((TensorProduct.AlgebraTensorModule.curry ((rTensor υ f).comp (lTensor ρ g)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (f.tensor g).toLinearMap) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
Q : Type u_7
inst✝¹ : AddCommMonoid Q
inst✝ : Module A Q
υ : Representation A G Q
f : ρ.IntertwiningMap τ
g : σ.IntertwiningMap υ
⊢ (lTensor τ g).comp (rTensor σ f) = f.tensor g

Tactic:
ext

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
Q : Type u_7
inst✝¹ : AddCommMonoid Q
inst✝ : Module A Q
υ : Representation A G Q
f : ρ.IntertwiningMap τ
g : σ.IntertwiningMap υ
x✝¹ : V
x✝ : W
⊢ ((TensorProduct.AlgebraTensorModule.curry ((lTensor τ g).comp (rTensor σ f)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (f.tensor g).toLinearMap) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
⊢ ↑(_root_.TensorProduct.comm A V W) ∘ₗ (ρ.tprod σ) g = (σ.tprod ρ) g ∘ₗ ↑(_root_.TensorProduct.comm A V W)

Tactic:
ext

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
x✝¹ : V
x✝ : W
⊢ ((TensorProduct.AlgebraTensorModule.curry (↑(_root_.TensorProduct.comm A V W) ∘ₗ (ρ.tprod σ) g)) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry ((σ.tprod ρ) g ∘ₗ ↑(_root_.TensorProduct.comm A V W))) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : σ.IntertwiningMap τ
⊢ (↑(comm ρ τ)).comp (IntertwiningMap.lTensor ρ f) = (IntertwiningMap.rTensor ρ f).comp ↑(comm ρ σ)

Tactic:
ext

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : σ.IntertwiningMap τ
x✝¹ : V
x✝ : W
⊢ ((TensorProduct.AlgebraTensorModule.curry ((↑(comm ρ τ)).comp (IntertwiningMap.lTensor ρ f)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry ((IntertwiningMap.rTensor ρ f).comp ↑(comm ρ σ)).toLinearMap) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : σ.IntertwiningMap τ
⊢ (↑(comm τ ρ)).comp (IntertwiningMap.rTensor ρ f) = (IntertwiningMap.lTensor ρ f).comp ↑(comm σ ρ)

Tactic:
ext

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : σ.IntertwiningMap τ
x✝¹ : W
x✝ : V
⊢ ((TensorProduct.AlgebraTensorModule.curry ((↑(comm τ ρ)).comp (IntertwiningMap.rTensor ρ f)).toLinearMap) x✝¹) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry ((IntertwiningMap.lTensor ρ f).comp ↑(comm σ ρ)).toLinearMap) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
⊢ ↑(_root_.TensorProduct.assoc A V W U) ∘ₗ ((ρ.tprod σ).tprod τ) g =
    (ρ.tprod (σ.tprod τ)) g ∘ₗ ↑(_root_.TensorProduct.assoc A V W U)

Tactic:
ext

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
x✝² : V
x✝¹ : W
x✝ : U
⊢ (((TensorProduct.AlgebraTensorModule.curry
            (TensorProduct.AlgebraTensorModule.curry
              (↑(_root_.TensorProduct.assoc A V W U) ∘ₗ ((ρ.tprod σ).tprod τ) g)))
          x✝²)
        x✝¹)
      x✝ =
    (((TensorProduct.AlgebraTensorModule.curry
            (TensorProduct.AlgebraTensorModule.curry
              ((ρ.tprod (σ.tprod τ)) g ∘ₗ ↑(_root_.TensorProduct.assoc A V W U))))
          x✝²)
        x✝¹)
      x✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
⊢ ↑(_root_.TensorProduct.rid A W) ∘ₗ (σ.tprod (trivial A G A)) g = σ g ∘ₗ ↑(_root_.TensorProduct.rid A W)

Tactic:
ext

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
x✝ : W
⊢ ((TensorProduct.AlgebraTensorModule.curry (↑(_root_.TensorProduct.rid A W) ∘ₗ (σ.tprod (trivial A G A)) g)) x✝) 1 =
    ((TensorProduct.AlgebraTensorModule.curry (σ g ∘ₗ ↑(_root_.TensorProduct.rid A W))) x✝) 1
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
⊢ ↑(_root_.TensorProduct.lid A W) ∘ₗ ((trivial A G A).tprod σ) g = σ g ∘ₗ ↑(_root_.TensorProduct.lid A W)

Tactic:
ext

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
g : G
x✝ : W
⊢ ((TensorProduct.AlgebraTensorModule.curry (↑(_root_.TensorProduct.lid A W) ∘ₗ ((trivial A G A).tprod σ) g)) 1) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (σ g ∘ₗ ↑(_root_.TensorProduct.lid A W))) 1) x✝
Module: Mathlib.RepresentationTheory.Rep.Res

Goal state before:
pp: k : Type u
inst✝² : Semiring k
G : Type v1
H : Type v2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : H →* G
hf : Function.Surjective ⇑f
X Y : Rep k G
f' : (resFunctor f).obj X ⟶ (resFunctor f).obj Y
⊢ (resFunctor f).map (liftHomOfSurj f hf f') = f'

Tactic:
ext

Goal state after:
k : Type u
inst✝² : Semiring k
G : Type v1
H : Type v2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : H →* G
hf : Function.Surjective ⇑f
X Y : Rep k G
f' : (resFunctor f).obj X ⟶ (resFunctor f).obj Y
x✝ : ↑((resFunctor f).obj X)
⊢ (Hom.hom ((resFunctor f).map (liftHomOfSurj f hf f'))).toLinearMap x✝ = (Hom.hom f').toLinearMap x✝
Module: Mathlib.RepresentationTheory.Rep.Res

Goal state before:
pp: G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
k : Type u
inst✝ : CommRing k
φ : H →* G
S : ShortComplex (Rep k G)
⊢ (S.map (resFunctor φ)).ShortExact ↔ S.ShortExact

Tactic:
constructor

Goal state after:
case mp
G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
k : Type u
inst✝ : CommRing k
φ : H →* G
S : ShortComplex (Rep k G)
⊢ (S.map (resFunctor φ)).ShortExact → S.ShortExact

case mpr
G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
k : Type u
inst✝ : CommRing k
φ : H →* G
S : ShortComplex (Rep k G)
⊢ S.ShortExact → (S.map (resFunctor φ)).ShortExact
Module: Mathlib.RepresentationTheory.Rep.Iso

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : ModuleCat k[G]
f : X✝ ⟶ Y✝
g : G
⊢ { toAddHom := (ModuleCat.Hom.hom f).toAddHom, map_smul' := ⋯ } ∘ₗ (Representation.ofModule ↑X✝) g =
    (Representation.ofModule ↑Y✝) g ∘ₗ { toAddHom := (ModuleCat.Hom.hom f).toAddHom, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : ModuleCat k[G]
f : X✝ ⟶ Y✝
g : G
x✝ : RestrictScalars k k[G] ↑X✝
⊢ ({ toAddHom := (ModuleCat.Hom.hom f).toAddHom, map_smul' := ⋯ } ∘ₗ (Representation.ofModule ↑X✝) g) x✝ =
    ((Representation.ofModule ↑Y✝) g ∘ₗ { toAddHom := (ModuleCat.Hom.hom f).toAddHom, map_smul' := ⋯ }) x✝
Module: Mathlib.RepresentationTheory.Rep.Iso

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
g : G
⊢ ↑(let __src := unitIsoAddEquiv;
        { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯,
          right_inv := ⋯ }) ∘ₗ
      V.ρ g =
    (Representation.ofModule ↑(toModuleMonoidAlgebra.obj V)) g ∘ₗ
      ↑(let __src := unitIsoAddEquiv;
        { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ })

Tactic:
ext

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
g : G
x✝ : ↑V
⊢ (↑(let __src := unitIsoAddEquiv;
          { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯,
            right_inv := ⋯ }) ∘ₗ
        V.ρ g)
      x✝ =
    ((Representation.ofModule ↑(toModuleMonoidAlgebra.obj V)) g ∘ₗ
        ↑(let __src := unitIsoAddEquiv;
          { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯,
            right_inv := ⋯ }))
      x✝
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ ρ.invariants.carrier = ⋂ g, Function.fixedPoints ⇑(ρ g)

Tactic:
ext

Goal state after:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
x✝ : V
⊢ x✝ ∈ ρ.invariants.carrier ↔ x✝ ∈ ⋂ g, Function.fixedPoints ⇑(ρ g)
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
⊢ Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f ↔ f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f

Tactic:
constructor

Goal state after:
case mp
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
⊢ Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f → f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f

case mpr
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
⊢ f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f → Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S✝ : Subgroup G
inst✝¹ : S✝.Normal
S : Subgroup G
inst✝ : S.Normal
X Y : Rep k G
f : X ⟶ Y
g✝ : G ⧸ S
g : G
⊢ ModuleCat.Hom.hom ((invariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)) ∘ₗ (X.ρ.quotientToInvariants S) ↑g =
    (Y.ρ.quotientToInvariants S) ↑g ∘ₗ ModuleCat.Hom.hom ((invariantsFunctor k ↥S).map ((resFunctor S.subtype).map f))

Tactic:
ext

Goal state after:
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S✝ : Subgroup G
inst✝¹ : S✝.Normal
S : Subgroup G
inst✝ : S.Normal
X Y : Rep k G
f : X ⟶ Y
g✝ : G ⧸ S
g : G
x✝ : ↥(invariants (MonoidHom.comp X.ρ S.subtype))
⊢ ↑((ModuleCat.Hom.hom ((invariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)) ∘ₗ (X.ρ.quotientToInvariants S) ↑g)
        x✝) =
    ↑(((Y.ρ.quotientToInvariants S) ↑g ∘ₗ
          ModuleCat.Hom.hom ((invariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)))
        x✝)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun n ↦ F ∘ X n
this : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
⊢ s.indicator (Function.const E c) = fun x ↦ s.indicator 1 x • c

Tactic:
ext

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun n ↦ F ∘ X n
this : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
x✝ : E
⊢ s.indicator (Function.const E c) x✝ = s.indicator 1 x✝ • c
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun n ↦ F ∘ X n
this : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
x✝ : E
⊢ Function.const E c = fun x ↦ 1 x • c

Tactic:
ext

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun n ↦ F ∘ X n
this : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
x✝¹ x✝ : E
⊢ Function.const E c x✝ = 1 x✝ • c
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
σ : Representation k G A
ρ : Representation k G B
⊢ (LinearMap.funLeft k B fun x ↦ x * 1).restrict ⋯ = 1

Tactic:
ext

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
σ : Representation k G A
ρ : Representation k G B
x✝¹ : ↥(coindV φ ρ)
x✝ : H
⊢ ↑(((LinearMap.funLeft k B fun x ↦ x * 1).restrict ⋯) x✝¹) x✝ = ↑(1 x✝¹) x✝
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
σ : Representation k G A
ρ : Representation k G B
x✝¹ x✝ : H
⊢ (LinearMap.funLeft k B fun x ↦ x * (x✝¹ * x✝)).restrict ⋯ =
    (LinearMap.funLeft k B fun x ↦ x * x✝¹).restrict ⋯ * (LinearMap.funLeft k B fun x ↦ x * x✝).restrict ⋯

Tactic:
ext

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
σ : Representation k G A
ρ : Representation k G B
x✝³ x✝² : H
x✝¹ : ↥(coindV φ ρ)
x✝ : H
⊢ ↑(((LinearMap.funLeft k B fun x ↦ x * (x✝³ * x✝²)).restrict ⋯) x✝¹) x✝ =
    ↑(((LinearMap.funLeft k B fun x ↦ x * x✝³).restrict ⋯ * (LinearMap.funLeft k B fun x ↦ x * x✝²).restrict ⋯) x✝¹) x✝
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
σ : Representation k G A
ρ : Representation k G B
f : σ.IntertwiningMap ρ
h : H
⊢ (f.compLeft H).restrict ⋯ ∘ₗ (coind φ σ) h = (coind φ ρ) h ∘ₗ (f.compLeft H).restrict ⋯

Tactic:
ext

Goal state after:
k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
σ : Representation k G A
ρ : Representation k G B
f : σ.IntertwiningMap ρ
h : H
x✝¹ : ↥(coindV φ σ)
x✝ : H
⊢ ↑(((f.compLeft H).restrict ⋯ ∘ₗ (coind φ σ) h) x✝¹) x✝ = ↑(((coind φ ρ) h ∘ₗ (f.compLeft H).restrict ⋯) x✝¹) x✝