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
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✝

Tactic:
;

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 τ
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✝

Tactic:
;

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 τ
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✝

Tactic:
;

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.FDRep

Goal state before:
pp: R : Type u
G : Type v
inst✝¹ : CommRing R
inst✝ : Monoid G
V : FDRep R G
g : G
v : ↑((forget₂ (FDRep R G) (Rep R G)).obj V)
⊢ (((forget₂ (FDRep R G) (Rep R G)).obj V).ρ g) v = (V.ρ g) v

Tactic:
;

Goal state after:
R : Type u
G : Type v
inst✝¹ : CommRing R
inst✝ : Monoid G
V : FDRep R G
g : G
v : ↑((forget₂ (FDRep R G) (Rep R G)).obj V)
⊢ (((forget₂ (FDRep R G) (Rep R G)).obj V).ρ g) v = (V.ρ g) v
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
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✝

Tactic:
;

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
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

Tactic:
;

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
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✝

Tactic:
;

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.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 : Type u_6
k : Type u_7
V : Type u_8
W : Type u_9
inst✝⁷ : Group G
inst✝⁶ : Field k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : FiniteDimensional k V
inst✝ : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
g : G
v' : Module.Dual k V
w : W
v : V
⊢ (((TensorProduct.AlgebraTensorModule.curry (↑(dualTensorHomEquiv k V W) ∘ₗ (ρ.dual.tprod σ) g)) v') w) v =
    (((TensorProduct.AlgebraTensorModule.curry ((ρ.linHom σ) g ∘ₗ ↑(dualTensorHomEquiv k V W))) v') w) v

Tactic:
;

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 : Type u_6
k : Type u_7
V : Type u_8
W : Type u_9
inst✝⁷ : Group G
inst✝⁶ : Field k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : FiniteDimensional k V
inst✝ : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
g : G
v' : Module.Dual k V
w : W
v : V
⊢ (((TensorProduct.AlgebraTensorModule.curry (↑(dualTensorHomEquiv k V W) ∘ₗ (ρ.dual.tprod σ) g)) v') w) v =
    (((TensorProduct.AlgebraTensorModule.curry ((ρ.linHom σ) g ∘ₗ ↑(dualTensorHomEquiv k V W))) v') w) v
Module: Mathlib.RepresentationTheory.Rep.Iso

Goal state before:
pp: case add
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : k[G]
x : V
g h : k[G]
gw : f ((((lift k (V →ₗ[k] V) G) ρ) g) x) = (((lift k (W →ₗ[k] W) G) σ) g) (f x)
hw : f ((((lift k (V →ₗ[k] V) G) ρ) h) x) = (((lift k (W →ₗ[k] W) G) σ) h) (f x)
⊢ f ((((lift k (V →ₗ[k] V) G) ρ) (g + h)) x) = (((lift k (W →ₗ[k] W) G) σ) (g + h)) (f x)

Tactic:
;

Goal state after:
case add
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : k[G]
x : V
g h : k[G]
gw : f ((((lift k (V →ₗ[k] V) G) ρ) g) x) = (((lift k (W →ₗ[k] W) G) σ) g) (f x)
hw : f ((((lift k (V →ₗ[k] V) G) ρ) h) x) = (((lift k (W →ₗ[k] W) G) σ) h) (f x)
⊢ f ((((lift k (V →ₗ[k] V) G) ρ) (g + h)) x) = (((lift k (W →ₗ[k] W) G) σ) (g + h)) (f 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
M : Rep k G
X Y : Rep k G
hf : Function.Surjective ⇑f
f' : res f X ⟶ res f Y
h : H
⊢ (Hom.hom f').toLinearMap ∘ₗ X.ρ (f h) = Y.ρ (f h) ∘ₗ (Hom.hom f').toLinearMap

Tactic:
;

Goal state after:
k : Type u
inst✝² : Semiring k
G : Type v1
H : Type v2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : H →* G
M : Rep k G
X Y : Rep k G
hf : Function.Surjective ⇑f
f' : res f X ⟶ res f Y
h : H
⊢ (Hom.hom f').toLinearMap ∘ₗ X.ρ (f h) = Y.ρ (f h) ∘ₗ (Hom.hom f').toLinearMap
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
x✝ : ↑((resFunctor f).obj X)
⊢ (Hom.hom ((resFunctor f).map (liftHomOfSurj f hf f'))).toLinearMap x✝ = (Hom.hom f').toLinearMap x✝

Tactic:
;

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: k : Type u
inst✝² : Semiring k
G : Type v1
H : Type v2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : H →* G
M : Rep k G
x✝³ x✝² : Rep k G
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ (Hom.hom ((resFunctor f).map (x✝¹ + x✝))).toLinearMap =
    (Hom.hom ((resFunctor f).map x✝¹ + (resFunctor f).map x✝)).toLinearMap

Tactic:
;

Goal state after:
k : Type u
inst✝² : Semiring k
G : Type v1
H : Type v2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : H →* G
M : Rep k G
x✝³ x✝² : Rep k G
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ (Hom.hom ((resFunctor f).map (x✝¹ + x✝))).toLinearMap =
    (Hom.hom ((resFunctor f).map x✝¹ + (resFunctor f).map x✝)).toLinearMap
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
M : Rep k✝ G
k : Type u
inst✝ : CommSemiring k
x✝³ x✝² : Rep k G
x✝¹ : x✝³ ⟶ x✝²
x✝ : k
⊢ (Hom.hom ((resFunctor f).map (x✝ • x✝¹))).toLinearMap = (Hom.hom (x✝ • (resFunctor f).map x✝¹)).toLinearMap

Tactic:
;

Goal state after:
k✝ : Type u
inst✝³ : Semiring k✝
G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
f : H →* G
M : Rep k✝ G
k : Type u
inst✝ : CommSemiring k
x✝³ x✝² : Rep k G
x✝¹ : x✝³ ⟶ x✝²
x✝ : k
⊢ (Hom.hom ((resFunctor f).map (x✝ • x✝¹))).toLinearMap = (Hom.hom (x✝ • (resFunctor f).map x✝¹)).toLinearMap
Module: Mathlib.RepresentationTheory.Rep.Iso

Goal state before:
pp: case smul
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : k[G]
x : V
⊢ ∀ (r : k) (x_1 : k[G]),
    f ((((lift k (V →ₗ[k] V) G) ρ) x_1) x) = (((lift k (W →ₗ[k] W) G) σ) x_1) (f x) →
      f ((((lift k (V →ₗ[k] V) G) ρ) (r • x_1)) x) = (((lift k (W →ₗ[k] W) G) σ) (r • x_1)) (f x)

Tactic:
intro r

Goal state after:
case smul
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r✝ : k[G]
x : V
r : k
⊢ ∀ (x_1 : k[G]),
    f ((((lift k (V →ₗ[k] V) G) ρ) x_1) x) = (((lift k (W →ₗ[k] W) G) σ) x_1) (f x) →
      f ((((lift k (V →ₗ[k] V) G) ρ) (r • x_1)) x) = (((lift k (W →ₗ[k] W) G) σ) (r • x_1)) (f x)
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
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✝

Tactic:
;

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
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✝

Tactic:
;

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.Probability.StrongLaw

Goal state before:
pp: case e'_3
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
I3 : ∀ (N : ℕ), ∑ i ∈ range N, ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} ≤ ENNReal.ofReal (ε⁻¹ ^ 2 * C)
I4 : ∑' (i : ℕ), ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} < ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, |∑ c ∈ range (u n), Y c ω - ∫ (a : Ω), ∑ c ∈ range (u n), Y c a| < ε * ↑(u n)
x✝¹ : ℕ
x✝ : Ω
⊢ (range ⌊c ^ x✝¹⌋₊).sum Y x✝ = ∑ c ∈ range (u x✝¹), Y c x✝

Tactic:
;

Goal state after:
case e'_3
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
I3 : ∀ (N : ℕ), ∑ i ∈ range N, ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} ≤ ENNReal.ofReal (ε⁻¹ ^ 2 * C)
I4 : ∑' (i : ℕ), ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} < ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, |∑ c ∈ range (u n), Y c ω - ∫ (a : Ω), ∑ c ∈ range (u n), Y c a| < ε * ↑(u n)
x✝¹ : ℕ
x✝ : Ω
⊢ (range ⌊c ^ x✝¹⌋₊).sum Y x✝ = ∑ c ∈ range (u x✝¹), Y c 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
x✝ : V
⊢ x✝ ∈ ρ.invariants.carrier ↔ x✝ ∈ ⋂ g, Function.fixedPoints ⇑(ρ g)

Tactic:
;

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
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✝)

Tactic:
;

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.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
X : Rep k G
g : G
x : ↑((invariantsFunctor k G).obj X)
⊢ (X.ρ.invariants.subtype ∘ₗ (Representation.trivial k G ↑((invariantsFunctor k G).obj X)) g) x =
    (X.ρ g ∘ₗ X.ρ.invariants.subtype) x

Tactic:
;

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
X : Rep k G
g : G
x : ↑((invariantsFunctor k G).obj X)
⊢ (X.ρ.invariants.subtype ∘ₗ (Representation.trivial k G ↑((invariantsFunctor k G).obj X)) g) x =
    (X.ρ g ∘ₗ X.ρ.invariants.subtype) x
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
X : ModuleCat k
Y : Rep k G
f : (trivialFunctor k G).obj X ⟶ Y
c✝ : ↑((trivialFunctor k G).obj X)
g✝ : G
⊢ (Y.ρ g✝) ((Hom.hom f).toLinearMap c✝) = (Hom.hom f).toLinearMap c✝

Tactic:
;

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
X : ModuleCat k
Y : Rep k G
f : (trivialFunctor k G).obj X ⟶ Y
c✝ : ↑((trivialFunctor k G).obj X)
g✝ : G
⊢ (Y.ρ g✝) ((Hom.hom f).toLinearMap c✝) = (Hom.hom f).toLinearMap c✝
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e'_7
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
L : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
n : ℕ
⊢ (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) / ↑⌊c ^ n⌋₊ - ∫ (a : Ω), X 0 a =
    (∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) * (↑⌊c ^ n⌋₊)⁻¹

Tactic:
;

Goal state after:
case e'_7
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
L : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
n : ℕ
⊢ (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) / ↑⌊c ^ n⌋₊ - ∫ (a : Ω), X 0 a =
    (∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) * (↑⌊c ^ n⌋₊)⁻¹