mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : 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
N : ℕ
⊢ ∑ i ∈ range N, ENNReal.ofReal (Var[S (u i); ℙ] / (↑(u i) * ε) ^ 2) =
    ENNReal.ofReal (∑ i ∈ range N, Var[S (u i); ℙ] / (↑(u i) * ε) ^ 2)

Tactic:
by

Goal state after:
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
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f₁ f₂ : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
⊢ (f₁ + f₂).tensor g = f₁.tensor g + f₂.tensor g

Tactic:
by

Goal state after:
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
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g₁ g₂ : τ.IntertwiningMap π
⊢ f.tensor (g₁ + g₂) = f.tensor g₁ + f.tensor g₂

Tactic:
by

Goal state after:
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
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
a : A
f : ρ.IntertwiningMap σ
g : τ.IntertwiningMap π
⊢ (a • f).tensor g = a • f.tensor g

Tactic:
by

Goal state after:
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
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
a : A
g : τ.IntertwiningMap π
⊢ f.tensor (a • g) = a • f.tensor g

Tactic:
by

Goal state after:
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
⊢ lTensor ρ (id σ) = id (ρ.tprod σ)

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst✝ : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
h_subG : ∀ i < n - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
⊢ HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G✝ : Type v
inst✝³ : CommRing R
inst✝² : Field k
inst✝¹ : Monoid G✝
G : Type u
inst✝ : Monoid G
⊢ LargeCategory (FDRep R G)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ ConcreteCategory (FDRep R G) (Action.HomSubtype (FGModuleCat R) G)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ Preadditive (FDRep R G)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ HasFiniteLimits (FDRep k G)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ Linear R (FDRep R G)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
V : FDRep R G
⊢ Module.Finite R ↑V.V

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R : Type u
G : Type v
inst✝¹ : CommRing R
inst✝ : Monoid G
V W : FDRep R G
i : V ≅ W
g : G
⊢ W.ρ g = (isoToLinearEquiv i).conj (V.ρ g)

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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
⊢ (comm σ ρ).symm = comm ρ σ

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

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

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ MonoidalCategory (FDRep R G)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ MonoidalPreadditive (FDRep R G)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ MonoidalLinear R (FDRep R G)

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ HasKernels (FDRep k G)

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : 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
N : ℕ
⊢ ENNReal.ofReal (∑ i ∈ range N, Var[S (u i); ℙ] / (↑(u i) * ε) ^ 2) ≤ ENNReal.ofReal (ε⁻¹ ^ 2 * C)

Tactic:
by

Goal state after:
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
⊢ ↑(dualTensorHomEquiv k V W) ∘ₗ (ρ.dual.tprod σ) g = (ρ.linHom σ) g ∘ₗ ↑(dualTensorHomEquiv k V W)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
X Y : FDRep R G
f : (forget₂ (FDRep R G) (Rep R G)).obj X ⟶ (forget₂ (FDRep R G) (Rep R G)).obj Y
g : G
⊢ X.ρ g ≫ InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap) =
    InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap) ≫ Y.ρ g

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : 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
⊢ ∀ (N : ℕ), ∑ i ∈ range N, ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} ≤ ENNReal.ofReal (ε⁻¹ ^ 2 * C)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
X Y : FDRep R G
f : X ⟶ Y
g : G
⊢ ModuleCat.Hom.hom ((forget₂ (FGModuleCat R) (ModuleCat R)).map f.hom) ∘ₗ
      ((((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj X).V.endRingEquiv.toMonoidHom.comp
          (((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj X).ρ)
        g =
    ((((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj Y).V.endRingEquiv.toMonoidHom.comp
          (((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj Y).ρ)
        g ∘ₗ
      ModuleCat.Hom.hom ((forget₂ (FGModuleCat R) (ModuleCat R)).map f.hom)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ (forget₂ (FDRep R G) (Rep R G)).Full

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
⊢ (forget₂ (FDRep R G) (Rep R G)).Faithful

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: k : Type u
G : Type v
V : Type u
inst✝⁴ : Field k
inst✝³ : Group G
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : FiniteDimensional k V
ρV : Representation k G V
W : FDRep k G
⊢ of ρV.dual ⊗ W ≅ of (ρV.linHom W.ρ)

Tactic:
by

Goal state after:
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
X Y : Rep k G
f : H →* G
p : X ⟶ Y
h : H
⊢ ↑(Hom.hom p) ∘ₗ (MonoidHom.comp X.ρ f) h = (MonoidHom.comp Y.ρ f) h ∘ₗ ↑(Hom.hom p)

Tactic:
by

Goal state after:
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
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (resFunctor f).map a₁✝ = (resFunctor f).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
by

Goal state after:
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
g : G
⊢ (Hom.hom f').toLinearMap ∘ₗ X.ρ g = Y.ρ g ∘ₗ (Hom.hom f').toLinearMap

Tactic:
by

Goal state after:
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:
by

Goal state after:
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✝²
⊢ (resFunctor f).map (x✝¹ + x✝) = (resFunctor f).map x✝¹ + (resFunctor f).map x✝

Tactic:
by

Goal state after:
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
⊢ (resFunctor f).map (x✝ • x✝¹) = x✝ • (resFunctor f).map x✝¹

Tactic:
by

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

Goal state before:
pp: G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
f : H →* G
k : Type u
inst✝ : Ring k
M : Rep k G
⊢ IsZero (res f M) ↔ IsZero M

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 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
⊢ f ((((lift k (V →ₗ[k] V) G) ρ) r) x) = (((lift k (W →ₗ[k] W) G) σ) r) (f x)

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
M : ModuleCat k[G]
⊢ ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M) ≃+ ↑M

Tactic:
by

Goal state after:
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)
exact✝ : S.Exact
mono_f : Mono S.f
epi_g : Epi S.g
⊢ (S.map (resFunctor φ)).Exact

Tactic:
by

Goal state after:
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
⊢ ↑V ≃+ ↑((toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).obj V)

Tactic:
by

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
M : ModuleCat k[G]
r : k[G]
x : (ofModuleMonoidAlgebra.obj M).ρ.asModule
⊢ counitIsoAddEquiv.toFun (r • x) = (RingHom.id k[G]) r • counitIsoAddEquiv.toFun x

Tactic:
by

Goal state after:
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)
exact✝ : S.Exact
mono_f : Mono S.f
epi_g : Epi S.g
⊢ Mono (S.map (resFunctor φ)).f

Tactic:
by

Goal state after:
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
⊢ unitIsoAddEquiv ((V.ρ g).toFun x) =
    ((ofModuleMonoidAlgebra.obj (toModuleMonoidAlgebra.obj V)).ρ g).toFun (unitIsoAddEquiv x)

Tactic:
by

Goal state after:
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)
exact✝ : S.Exact
mono_f : Mono S.f
epi_g : Epi S.g
⊢ Epi (S.map (resFunctor φ)).g

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ ∀ {X Y : Rep k G} (f : X ⟶ Y),
    (𝟭 (Rep k G)).map f ≫ Y.unitIso.hom = X.unitIso.hom ≫ (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).map f

Tactic:
by

Goal state after: