mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X : Rep k G
Y : ModuleCat k
f : X ⟶ (trivialFunctor k G).obj Y
⊢ ((coinvariantsAdjunction k G).homEquiv X Y).symm f = desc f

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

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

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep.{?u.16, u, v} k G
⊢ ∀ {X' X : Rep.{max w t, u, w} k H} {Y : Rep.{max w t, u, v} k G} (f : X' ⟶ X) (g : X ⟶ (coindFunctor k φ).obj Y),
    (resCoindHomEquiv.{?u.42, u, v, w} φ X' Y).toEquiv.symm (f ≫ g) =
      (resFunctor φ).map f ≫ (resCoindHomEquiv.{?u.42, u, v, w} φ X Y).toEquiv.symm g

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u
G✝ : Type v
inst✝⁴ : CommRing k✝
inst✝³ : Monoid G✝
A B : Rep k✝ G✝
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : S.Normal
X : Rep k G
⊢ ofHom
      { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map (𝟙 X))),
        isIntertwining' := ⋯ } =
    𝟙 (X.quotientToCoinvariants S)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝ : Type u
G✝ : Type v
inst✝⁴ : CommRing k✝
inst✝³ : Monoid G✝
A B : Rep k✝ G✝
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
inst✝ : S.Normal
X✝ Y✝ Z✝ : Rep k G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ofHom
      { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map (f ≫ g))),
        isIntertwining' := ⋯ } =
    ofHom
        { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map f)),
          isIntertwining' := ⋯ } ≫
      ofHom
        { toLinearMap := ModuleCat.Hom.hom ((coinvariantsFunctor k ↥S).map ((resFunctor S.subtype).map g)),
          isIntertwining' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
α : Type u
inst✝ : DecidableEq α
x : ↑A
i : α
g : G
r : k
⊢ (A.coinvariantsTensorFreeToFinsupp α)
      ((Coinvariants.mk (A.ρ.tprod (Representation.free k G α))) (x ⊗ₜ[k] single i (MonoidAlgebra.single g r))) =
    single i (r • (A.ρ g⁻¹) x)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
α : Type u
inst✝ : DecidableEq α
i : α
x : ↑A
⊢ (A.finsuppToCoinvariantsTensorFree α) (single i x) =
    (Coinvariants.mk (A.ρ.tprod (Representation.free k G α))) (x ⊗ₜ[k] single i (MonoidAlgebra.single 1 1))

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝¹ : Type u
G✝¹ : Type v
inst✝⁶ : CommRing k✝¹
inst✝⁵ : Monoid G✝¹
A✝ B : Rep k✝¹ G✝¹
k✝ : Type u
G✝ : Type v
inst✝⁴ : CommRing k✝
inst✝³ : Group G✝
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
α : Type u
inst✝ : DecidableEq α
i : α
x : ↑A
⊢ (A.coinvariantsTensorFreeToFinsupp α ∘ₗ A.finsuppToCoinvariantsTensorFree α) (single i x) = LinearMap.id (single i x)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep.{?u.16, u, v} k G
⊢ ∀ {X : Rep.{max w t, u, w} k H} {Y Y' : Rep.{max w t, u, v} k G} (f : (resFunctor φ).obj X ⟶ Y) (g : Y ⟶ Y'),
    (resCoindHomEquiv.{t, u, v, w} φ X Y').toEquiv (f ≫ g) =
      (resCoindHomEquiv.{t, u, v, w} φ X Y).toEquiv f ≫ (coindFunctor k φ).map g

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k✝¹ : Type u
G✝¹ : Type v
inst✝⁶ : CommRing k✝¹
inst✝⁵ : Monoid G✝¹
A✝ B : Rep k✝¹ G✝¹
k✝ : Type u
G✝ : Type v
inst✝⁴ : CommRing k✝
inst✝³ : Group G✝
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
α : Type u
inst✝ : DecidableEq α
a : ↑A
i : α
g : G
r : k
⊢ ((((TensorProduct.mk k ↑A ↑(free k G α)).compr₂ₛₗ
              ((A.finsuppToCoinvariantsTensorFree α ∘ₗ A.coinvariantsTensorFreeToFinsupp α) ∘ₗ
                Coinvariants.mk (A ⊗ free k G α).ρ))
            a ∘ₗ
          lsingle i) ∘ₗ
        MonoidAlgebra.lsingle g)
      r =
    ((((TensorProduct.mk k ↑A ↑(free k G α)).compr₂ₛₗ (LinearMap.id ∘ₗ Coinvariants.mk (A ⊗ free k G α).ρ)) a ∘ₗ
          lsingle i) ∘ₗ
        MonoidAlgebra.lsingle g)
      r

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
α : Type u
inst✝ : DecidableEq α
x : (A ⊗ free k G α).ρ.Coinvariants
⊢ (A.coinvariantsTensorFreeToFinsupp α) x = (A.coinvariantsTensorFreeToFinsupp α) x

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
A : ∀ (i : ℕ), Integrable (X i) μ
Y : ℕ → Ω → E := fun i ↦ AEStronglyMeasurable.mk (X i) ⋯
B : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), X n ω = Y n ω
Yint : Integrable (Y 0) μ
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))

Tactic:
by

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

Goal state before:
pp: k : Type u
G : Type v
X : Type w
inst✝⁷ : TopologicalSpace k
inst✝⁶ : Ring k
inst✝⁵ : Monoid G
inst✝⁴ : AddCommGroup X
inst✝³ : Module k X
inst✝² : TopologicalSpace X
inst✝¹ : IsTopologicalAddGroup X
inst✝ : ContinuousSMul k X
ρ : ContRepresentation k G X
⊢ ↑(of ρ) = X

Tactic:
by

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

Goal state before:
pp: k : Type u
G : Type v
X : Type w
inst✝⁷ : TopologicalSpace k
inst✝⁶ : Ring k
inst✝⁵ : Monoid G
inst✝⁴ : AddCommGroup X
inst✝³ : Module k X
inst✝² : TopologicalSpace X
inst✝¹ : IsTopologicalAddGroup X
inst✝ : ContinuousSMul k X
ρ : ContRepresentation k G X
⊢ (of ρ).ρ = ρ

Tactic:
by

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

Goal state before:
pp: k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : Ring k
inst✝ : Monoid G
A B : TopRep k G
f : A ⟶ B
g : G
a : ↑A
⊢ (Hom.hom f) ((A.ρ g) a) = (B.ρ g) ((Hom.hom f) a)

Tactic:
by

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

Goal state before:
pp: k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : Ring k
inst✝ : Monoid G
A B C : TopRep k G
f : A ⟶ B
g h : B ⟶ C
⊢ f ≫ (g + h) = f ≫ g + f ≫ h

Tactic:
by

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

Goal state before:
pp: k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : Ring k
inst✝ : Monoid G
A B C : TopRep k G
f g : A ⟶ B
h : B ⟶ C
⊢ (f + g) ≫ h = f ≫ h + g ≫ h

Tactic:
by

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

Goal state before:
pp: k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : CommRing k
inst✝ : Monoid G
A B C : TopRep k G
r : k
f : A ⟶ B
g : B ⟶ C
⊢ (r • f) ≫ g = r • f ≫ g

Tactic:
by

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

Goal state before:
pp: k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : CommRing k
inst✝ : Monoid G
A B C : TopRep k G
f : A ⟶ B
r : k
g : B ⟶ C
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
by

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

Goal state before:
pp: k : Type u
G : Type v
X Y : Type w
inst✝¹² : TopologicalSpace k
inst✝¹¹ : Ring k
inst✝¹⁰ : Monoid G
inst✝⁹ : AddCommGroup X
inst✝⁸ : Module k X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : IsTopologicalAddGroup X
inst✝⁵ : ContinuousSMul k X
inst✝⁴ : AddCommGroup Y
inst✝³ : Module k Y
inst✝² : TopologicalSpace Y
inst✝¹ : IsTopologicalAddGroup Y
inst✝ : ContinuousSMul k Y
ρ : ContRepresentation k G X
σ : ContRepresentation k G Y
A B C : TopRep k G
X✝ Y✝ : TopRep k G
f : X✝ ⟶ Y✝
g : G
⊢ { V := TopModuleCat.of k ↑X✝, ρ := (TopModuleCat.of k ↑X✝).endRingEquiv.symm.toMonoidHom.comp ↑X✝.ρ }.ρ g ≫
      Hom.toTopModuleCatHom f =
    Hom.toTopModuleCatHom f ≫
      { V := TopModuleCat.of k ↑Y✝, ρ := (TopModuleCat.of k ↑Y✝).endRingEquiv.symm.toMonoidHom.comp ↑Y✝.ρ }.ρ g

Tactic:
by

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

Goal state before:
pp: k : Type u
G : Type v
X✝ Y✝ : Type w
inst✝¹² : TopologicalSpace k
inst✝¹¹ : Ring k
inst✝¹⁰ : Monoid G
inst✝⁹ : AddCommGroup X✝
inst✝⁸ : Module k X✝
inst✝⁷ : TopologicalSpace X✝
inst✝⁶ : IsTopologicalAddGroup X✝
inst✝⁵ : ContinuousSMul k X✝
inst✝⁴ : AddCommGroup Y✝
inst✝³ : Module k Y✝
inst✝² : TopologicalSpace Y✝
inst✝¹ : IsTopologicalAddGroup Y✝
inst✝ : ContinuousSMul k Y✝
ρ : ContRepresentation k G X✝
σ : ContRepresentation k G Y✝
A B C : TopRep k G
X Y : Action (TopModuleCat k) G
f : X ⟶ Y
g : G
⊢ TopModuleCat.Hom.hom f.hom ∘SL { toMonoidHom := X.V.endRingEquiv.toMonoidHom.comp X.ρ } g =
    { toMonoidHom := Y.V.endRingEquiv.toMonoidHom.comp Y.ρ } g ∘SL TopModuleCat.Hom.hom f.hom

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Semisimple

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : Monoid G
inst✝² : Field k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ ρ.IsSemisimpleRepresentation ↔ IsSemisimpleModule k[G] ρ.asModule

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Semisimple

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Monoid G
inst✝² : Field k
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module k[G] M
⊢ IsSemisimpleModule k[G] M ↔ (ofModule M).IsSemisimpleRepresentation

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝⁹ : CommRing k
G : Type u_2
inst✝⁸ : Group G
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module k[G] V
inst✝⁴ : IsScalarTower k k[G] V
W : Type u_4
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module k[G] W
inst✝ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
h : ∀ (v : V), π (i v) = v
g : G
v : V
⊢ (π.conjugate g) (i v) = v

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
inst✝ : Fintype G
g : G
v : W
⊢ (sumOfConjugates G π) (MonoidAlgebra.single g 1 • v) = MonoidAlgebra.single g 1 • (sumOfConjugates G π) v

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
inst✝ : Fintype G
v : W
⊢ (equivariantProjection G π) v = (↑(Nat.card G))⁻¹ʳ • ∑ g, (π.conjugate g) v

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
n : ℕ
⊢ eLpNorm (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω - ∫ (x : Ω), X 0 x ∂μ) p μ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
⊢ Tendsto (fun n ↦ eLpNorm (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω - ∫ (x : Ω), X 0 x ∂μ) p μ) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
inst✝ : Fintype G
hcard : IsUnit ↑(Nat.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ (equivariantProjection G π) (i v) = v

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝⁷ : Field k
G : Type u_2
inst✝⁶ : Finite G
inst✝⁵ : NeZero ↑(Nat.card G)
inst✝⁴ : Group G
V : Type u_3
inst✝³ : AddCommGroup V
inst✝² : Module k[G] V
W : Type u_4
inst✝¹ : AddCommGroup W
inst✝ : Module k[G] W
f : V →ₗ[k[G]] W
hf : f.ker = ⊥
A : Type (max u_1 u_2) := k[G]
this✝¹ : Module k W := Module.compHom W (algebraMap k A)
this✝ : Module k V := Module.compHom V (algebraMap k A)
this : IsScalarTower k A W
⊢ ∃ g, g ∘ₗ f = LinearMap.id

Tactic:
have := IsScalarTower.of_compHom k A V

Goal state after:
k : Type u_1
inst✝⁷ : Field k
G : Type u_2
inst✝⁶ : Finite G
inst✝⁵ : NeZero ↑(Nat.card G)
inst✝⁴ : Group G
V : Type u_3
inst✝³ : AddCommGroup V
inst✝² : Module k[G] V
W : Type u_4
inst✝¹ : AddCommGroup W
inst✝ : Module k[G] W
f : V →ₗ[k[G]] W
hf : f.ker = ⊥
A : Type (max u_1 u_2) := k[G]
this✝² : Module k W := Module.compHom W (algebraMap k A)
this✝¹ : Module k V := Module.compHom V (algebraMap k A)
this✝ : IsScalarTower k A W
this : IsScalarTower k A V
⊢ ∃ g, g ∘ₗ f = LinearMap.id
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝⁷ : Field k
G : Type u_2
inst✝⁶ : Finite G
inst✝⁵ : NeZero ↑(Nat.card G)
inst✝⁴ : Group G
V : Type u_3
inst✝³ : AddCommGroup V
inst✝² : Module k[G] V
W : Type u_4
inst✝¹ : AddCommGroup W
inst✝ : Module k[G] W
f : V →ₗ[k[G]] W
hf : f.ker = ⊥
A : Type (max u_1 u_2) := k[G]
this✝² : Module k W := Module.compHom W (algebraMap k A)
this✝¹ : Module k V := Module.compHom V (algebraMap k A)
this✝ : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V := (↑k f).leftInverse
⊢ ∀ (x : V), φ (f x) = x

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝⁷ : Field k
G : Type u_2
inst✝⁶ : Finite G
inst✝⁵ : NeZero ↑(Nat.card G)
inst✝⁴ : Group G
V : Type u_3
inst✝³ : AddCommGroup V
inst✝² : Module k[G] V
W : Type u_4
inst✝¹ : AddCommGroup W
inst✝ : Module k[G] W
f : V →ₗ[k[G]] W
hf : f.ker = ⊥
⊢ ∃ g, g ∘ₗ f = LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝⁵ : Field k
G : Type u_2
inst✝⁴ : Finite G
inst✝³ : NeZero ↑(Nat.card G)
inst✝² : Group G
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Module k[G] V
p : Submodule k[G] V
⊢ ∃ q, IsCompl p q

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝⁸ : Field k
G : Type u_2
inst✝⁷ : Finite G
inst✝⁶ : NeZero ↑(Nat.card G)
inst✝⁵ : Group G
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module k[G] V
W : Type u_4
inst✝² : AddCommGroup W
inst✝¹ : Module k[G] W
inst✝ : AddGroup G
⊢ NeZero ↑(Nat.card (Multiplicative G))

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k✝ : Type u_1
inst✝¹³ : Field k✝
G✝ : Type u_2
inst✝¹² : Finite G✝
inst✝¹¹ : NeZero ↑(Nat.card G✝)
inst✝¹⁰ : Group G✝
V✝ : Type u_3
inst✝⁹ : AddCommGroup V✝
inst✝⁸ : Module k✝[G✝] V✝
W : Type u_4
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k✝[G✝] W
G : Type u_5
k : Type u_6
V : Type u_7
inst✝⁵ : Group G
inst✝⁴ : Field k
inst✝³ : Finite G
inst✝² : NeZero ↑(Nat.card G)
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ ρ.IsSemisimpleRepresentation

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.InjectiveProjective

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : IsSemisimpleRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X Y : Type u_2
x✝⁴ : AddCommGroup X
x✝³ : AddCommGroup Y
x✝² : Module R X
x✝¹ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
h : Y →ₗ[R] M
comp : h ∘ₗ f = g
x✝ : X
⊢ h (f x✝) = g x✝

Tactic:
by

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹³ : Monoid G
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : IsTopologicalAddGroup W
inst✝⁴ : Module R W
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
π₁ π₂ : ContRepresentation R G V
x✝ : (fun π ↦ ⇑π.toMonoidHom) π₁ = (fun π ↦ ⇑π.toMonoidHom) π₂
⊢ π₁ = π₂

Tactic:
by

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹³ : Monoid G
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : IsTopologicalAddGroup W
inst✝⁴ : Module R W
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
g : G
⊢ ContinuousLinearMap.id R V ∘SL π₁ g = π₁ g ∘SL ContinuousLinearMap.id R V

Tactic:
by

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁹ : Monoid G
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : Module R V
inst✝³ : AddCommGroup W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup W
inst✝ : Module R W
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
f g : π₁ →ⁱL π₂
h : f.toContinuousLinearMap = g.toContinuousLinearMap
⊢ f = g

Tactic:
by

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁹ : Monoid G
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : Module R V
inst✝³ : AddCommGroup W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup W
inst✝ : Module R W
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
x✝² x✝¹ : π₁ →ⁱL π₂
x✝ : (fun f ↦ f.toIntertwiningMap) x✝² = (fun f ↦ f.toIntertwiningMap) x✝¹
⊢ x✝² = x✝¹

Tactic:
by

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁹ : Monoid G
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : Module R V
inst✝³ : AddCommGroup W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup W
inst✝ : Module R W
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
f g : π₁ →ⁱL π₂
h : (fun f ↦ (↑f.toContinuousLinearMap).toFun) f = (fun f ↦ (↑f.toContinuousLinearMap).toFun) g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝¹³ : Monoid G
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : TopologicalSpace V
inst✝⁹ : IsTopologicalAddGroup V
inst✝⁸ : Module R V
inst✝⁷ : AddCommGroup W
inst✝⁶ : TopologicalSpace W
inst✝⁵ : IsTopologicalAddGroup W
inst✝⁴ : Module R W
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
π₁✝ : ContRepresentation R G V
π₂✝ : ContRepresentation R G W
π₃✝ : ContRepresentation R G U
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
f : π₂ →ⁱL π₃
g : π₁ →ⁱL π₂
h : G
⊢ (f.toContinuousLinearMap ∘SL g.toContinuousLinearMap) ∘SL π₁ h =
    π₃ h ∘SL f.toContinuousLinearMap ∘SL g.toContinuousLinearMap

Tactic:
by

Goal state after: