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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
h'f : 0 ≤ f
⊢ ∫ (x : α), truncation f A x ∂μ = ∫ (y : ℝ) in 0..A, y ∂Measure.map f μ

Tactic:
simpa using

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
h'f : 0 ≤ f
⊢ ∫ (x : α), truncation f A x ∂μ = ∫ (y : ℝ) in 0..A, y ∂Measure.map f μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case pos.integrable_exp_mul
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
⊢ ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * Y ω)) (⇑(prodMkLeft Ω' η) ∘ₘ ν ⊗ₘ κ)

Tactic:
simpa using

Goal state after:
case pos.integrable_exp_mul
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
⊢ ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * Y ω)) (⇑η ∘ₘ ⇑κ ∘ₘ ν)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ (∫ (a : Ω), truncation X (↑N) a) + ∫ (x : ℝ) in 0..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + ∫ (x : ℝ) in 0..↑N, 1 ∂ρ

Tactic:
integral_truncation_le_integral_of_nonneg hint hnonneg

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ (∫ (x : Ω), X x) + ∫ (x : ℝ) in 0..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + ∫ (x : ℝ) in 0..↑N, 1 ∂ρ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
x✝ : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
h1 : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑(Kernel.const Unit μ) ∘ₘ Measure.dirac ())
h2 : ∀ᵐ (ω' : Unit) ∂Measure.dirac (), ∀ (t : ℝ), mgf X ((Kernel.const Unit μ) ω') t ≤ rexp (↑c * t ^ 2 / 2)
⊢ ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) μ

Tactic:
simpa using

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
x✝ : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
h1 : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑(Kernel.const Unit μ) ∘ₘ Measure.dirac ())
h2 : ∀ᵐ (ω' : Unit) ∂Measure.dirac (), ∀ (t : ℝ), mgf X ((Kernel.const Unit μ) ω') t ≤ rexp (↑c * t ^ 2 / 2)
⊢ ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
x✝ : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
h1 : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑(Kernel.const Unit μ) ∘ₘ Measure.dirac ())
h2 : ∀ᵐ (ω' : Unit) ∂Measure.dirac (), ∀ (t : ℝ), mgf X ((Kernel.const Unit μ) ω') t ≤ rexp (↑c * t ^ 2 / 2)
⊢ ∀ (t : ℝ), mgf X μ t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
simpa using

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
x✝ : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
h1 : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑(Kernel.const Unit μ) ∘ₘ Measure.dirac ())
h2 : ∀ᵐ (ω' : Unit) ∂Measure.dirac (), ∀ (t : ℝ), mgf X ((Kernel.const Unit μ) ω') t ≤ rexp (↑c * t ^ 2 / 2)
⊢ ∀ (t : ℝ), mgf X μ t ≤ rexp (↑c * t ^ 2 / 2)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
x✝ : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
h1 : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑(Kernel.const Unit μ) ∘ₘ Measure.dirac ())
h2 : ∀ᵐ (ω' : Unit) ∂Measure.dirac (), ∀ (t : ℝ), mgf X ((Kernel.const Unit μ) ω') t ≤ rexp (↑c * t ^ 2 / 2)
⊢ ∀ (t : ℝ), mgf X μ t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
simpa using h2

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
h_int : Integrable (fun ω ↦ rexp (1 * X ω)) μ
⊢ AEStronglyMeasurable X μ

Tactic:
simpa using

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
h_int : Integrable (fun ω ↦ rexp (1 * X ω)) μ
⊢ AEStronglyMeasurable X μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
t : ℝ
p : ℝ≥0
⊢ MemLp (fun ω ↦ rexp (t * X ω)) (↑p) μ

Tactic:
simpa using

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
t : ℝ
p : ℝ≥0
⊢ MemLp (fun ω ↦ rexp (t * X ω)) (↑p) μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
t : ℝ
⊢ cgf X μ t ≤ ↑c * t ^ 2 / 2

Tactic:
simpa using

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
t : ℝ
⊢ cgf X μ t ≤ ↑c * t ^ 2 / 2
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
⊢ HasSubgaussianMGF (-X) c μ

Tactic:
simpa using

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
⊢ Kernel.HasSubgaussianMGF (-X) c (Kernel.const Unit μ) (Measure.dirac ())
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: k✝ : Type u
inst✝¹¹ : Semiring k✝
G : Type v
inst✝¹⁰ : Monoid G
V : Type v'
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module k✝ V
W : Type w'
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module k✝ W
H : Type w
inst✝⁵ : Subsingleton H
inst✝⁴ : MulOneClass H
inst✝³ : MulAction G H
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
x : (leftRegular k G).IntertwiningMap σ
x✝ : G
⊢ (((fun v ↦
              { toLinearMap := ((Finsupp.llift V k k G) fun g ↦ (σ g) v) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k),
                isIntertwining' := ⋯ })
            ((fun f ↦ (Finsupp.llift V k k G).symm (f.toLinearMap ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k).symm) 1)
              x)).toLinearMap ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    (x.toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1

Tactic:
simp [← x.isIntertwining]

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

Goal state before:
pp: case refine_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ mgf id (Measure.map X μ) t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
mgf_id_map hX

Goal state after:
case refine_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ mgf X μ t ≤ rexp (↑c * t ^ 2 / 2)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
ε : ℝ
hε : 0 ≤ ε
⊢ μ.real {ω | ε ≤ X ω} ≤ rexp (-ε ^ 2 / (2 * ↑c))

Tactic:
simpa using

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
ε : ℝ
hε : 0 ≤ ε
⊢ μ.real {ω | ε ≤ X ω} ≤ rexp (-ε ^ 2 / (2 * ↑c))
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 μ
⊢ X =ᵐ[μ] 0

Tactic:
simpa using

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 μ
⊢ X =ᵐ[μ] 0
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
this :
  Kernel.HasSubgaussianMGF (fun ω ↦ X ω + Y ω) ((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) (Kernel.const Unit μ)
    (Measure.dirac ())
⊢ HasSubgaussianMGF (fun ω ↦ X ω + Y ω) ((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) μ

Tactic:
simpa using

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
this :
  Kernel.HasSubgaussianMGF (fun ω ↦ X ω + Y ω) ((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) (Kernel.const Unit μ)
    (Measure.dirac ())
⊢ Kernel.HasSubgaussianMGF (fun ω ↦ X ω + Y ω) ((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) (Kernel.const Unit μ)
    (Measure.dirac ())
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case mk.mk
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring 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
toLinearMap✝¹ : V →ₗ[A] W
isIntertwining'✝¹ : ∀ (g : G), toLinearMap✝¹ ∘ₗ ρ g = σ g ∘ₗ toLinearMap✝¹
toLinearMap✝ : V →ₗ[A] W
isIntertwining'✝ : ∀ (g : G), toLinearMap✝ ∘ₗ ρ g = σ g ∘ₗ toLinearMap✝
h :
  { toLinearMap := toLinearMap✝¹, isIntertwining' := isIntertwining'✝¹ }.toLinearMap =
    { toLinearMap := toLinearMap✝, isIntertwining' := isIntertwining'✝ }.toLinearMap
⊢ { toLinearMap := toLinearMap✝¹, isIntertwining' := isIntertwining'✝¹ } =
    { toLinearMap := toLinearMap✝, isIntertwining' := isIntertwining'✝ }

Tactic:
simpa using

Goal state after:
case mk.mk
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring 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
toLinearMap✝¹ : V →ₗ[A] W
isIntertwining'✝¹ : ∀ (g : G), toLinearMap✝¹ ∘ₗ ρ g = σ g ∘ₗ toLinearMap✝¹
toLinearMap✝ : V →ₗ[A] W
isIntertwining'✝ : ∀ (g : G), toLinearMap✝ ∘ₗ ρ g = σ g ∘ₗ toLinearMap✝
h :
  { toLinearMap := toLinearMap✝¹, isIntertwining' := isIntertwining'✝¹ }.toLinearMap =
    { toLinearMap := toLinearMap✝, isIntertwining' := isIntertwining'✝ }.toLinearMap
⊢ toLinearMap✝¹ = toLinearMap✝
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
h_indep : iIndepFun X μ
c : ℝ≥0
n : ℕ
h_subG : ∀ i < n, HasSubgaussianMGF (X i) c μ
ε : ℝ
hε : 0 ≤ ε
h : μ.real {ω | ε ≤ ∑ i ∈ Finset.range n, X i ω} ≤ rexp (-ε ^ 2 / (2 * ↑(∑ i ∈ Finset.range n, c)))
⊢ μ.real {ω | ε ≤ ∑ i ∈ Finset.range n, X i ω} ≤ rexp (-ε ^ 2 / (2 * ↑n * ↑c))

Tactic:
simpa using

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
h_indep : iIndepFun X μ
c : ℝ≥0
n : ℕ
h_subG : ∀ i < n, HasSubgaussianMGF (X i) c μ
ε : ℝ
hε : 0 ≤ ε
h : μ.real {ω | ε ≤ ∑ i ∈ Finset.range n, X i ω} ≤ rexp (-ε ^ 2 / (2 * ↑(∑ i ∈ Finset.range n, c)))
⊢ μ.real {ω | ε ≤ ∑ i ∈ Finset.range n, X i ω} ≤ rexp (-ε ^ 2 / (2 * ↑n * ↑c))
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case mk'.mk'
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring 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
toIntertwiningMap✝¹ : σ.IntertwiningMap ρ
invFun✝¹ : V → W
left_inv✝¹ : Function.LeftInverse invFun✝¹ toIntertwiningMap✝¹.toFun
right_inv✝¹ : Function.RightInverse invFun✝¹ toIntertwiningMap✝¹.toFun
toIntertwiningMap✝ : σ.IntertwiningMap ρ
invFun✝ : V → W
left_inv✝ : Function.LeftInverse invFun✝ toIntertwiningMap✝.toFun
right_inv✝ : Function.RightInverse invFun✝ toIntertwiningMap✝.toFun
h :
  { toIntertwiningMap := toIntertwiningMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹,
        right_inv := right_inv✝¹ }.toLinearEquiv =
    { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝,
        right_inv := right_inv✝ }.toLinearEquiv
⊢ { toIntertwiningMap := toIntertwiningMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Tactic:
simpa using

Goal state after:
case mk'.mk'
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring 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
toIntertwiningMap✝¹ : σ.IntertwiningMap ρ
invFun✝¹ : V → W
left_inv✝¹ : Function.LeftInverse invFun✝¹ toIntertwiningMap✝¹.toFun
right_inv✝¹ : Function.RightInverse invFun✝¹ toIntertwiningMap✝¹.toFun
toIntertwiningMap✝ : σ.IntertwiningMap ρ
invFun✝ : V → W
left_inv✝ : Function.LeftInverse invFun✝ toIntertwiningMap✝.toFun
right_inv✝ : Function.RightInverse invFun✝ toIntertwiningMap✝.toFun
h :
  { toIntertwiningMap := toIntertwiningMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹,
        right_inv := right_inv✝¹ }.toLinearEquiv =
    { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝,
        right_inv := right_inv✝ }.toLinearEquiv
⊢ toIntertwiningMap✝¹.toLinearMap = toIntertwiningMap✝.toLinearMap ∧ invFun✝¹ = invFun✝
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case mk'.mk'
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring 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
toIntertwiningMap✝¹ : ρ.IntertwiningMap σ
invFun✝¹ : W → V
left_inv✝¹ : Function.LeftInverse invFun✝¹ toIntertwiningMap✝¹.toFun
right_inv✝¹ : Function.RightInverse invFun✝¹ toIntertwiningMap✝¹.toFun
toIntertwiningMap✝ : ρ.IntertwiningMap σ
invFun✝ : W → V
left_inv✝ : Function.LeftInverse invFun✝ toIntertwiningMap✝.toFun
right_inv✝ : Function.RightInverse invFun✝ toIntertwiningMap✝.toFun
h :
  ⇑{ toIntertwiningMap := toIntertwiningMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    ⇑{ toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
⊢ { toIntertwiningMap := toIntertwiningMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Tactic:
simpa using

Goal state after:
case mk'.mk'
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring 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
toIntertwiningMap✝¹ : ρ.IntertwiningMap σ
invFun✝¹ : W → V
left_inv✝¹ : Function.LeftInverse invFun✝¹ toIntertwiningMap✝¹.toFun
right_inv✝¹ : Function.RightInverse invFun✝¹ toIntertwiningMap✝¹.toFun
toIntertwiningMap✝ : ρ.IntertwiningMap σ
invFun✝ : W → V
left_inv✝ : Function.LeftInverse invFun✝ toIntertwiningMap✝.toFun
right_inv✝ : Function.RightInverse invFun✝ toIntertwiningMap✝.toFun
h :
  ⇑{ toIntertwiningMap := toIntertwiningMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    ⇑{ toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
⊢ toIntertwiningMap✝¹ = toIntertwiningMap✝ ∧ invFun✝¹ = invFun✝
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
ω : Ω
hab : X ω ∈ Set.Icc a b
⊢ X ω - ∫ (x : Ω), X x ∂μ ∈ Set.Icc (a - ∫ (x : Ω), X x ∂μ) (b - ∫ (x : Ω), X x ∂μ)

Tactic:
simpa using

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
ω : Ω
hab : X ω ∈ Set.Icc a b
⊢ a ≤ X ω ∧ X ω ≤ b
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case hbc
Ω : 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 : ℕ → Ω → ℝ := ⋯
S : ℕ → Ω → ℝ := ⋯
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := ⋯
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := ⋯
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N : ℕ
⊢ ∑ i ∈ range N, (↑(u i))⁻¹ ^ 2 * Var[S (u i); ℙ] ≤ C

Tactic:
simpa using

Goal state after:
case hbc
Ω : 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 : ℕ
⊢ ∑ x ∈ range N, (↑(u x) ^ 2)⁻¹ * Var[S (u x); ℙ] ≤ C
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:
simpa using

Goal state after:
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).toLinearMap ∘ₗ X.ρ (f h) = Y.ρ (f h) ∘ₗ (Hom.hom p).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
X✝ Y✝ : Rep k G
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (resFunctor f).map a₁✝ = (resFunctor f).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
simpa using

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
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (resFunctor f).map a₁✝ = (resFunctor f).map a₂✝
⊢ (Hom.hom a₁✝).toLinearMap = (Hom.hom a₂✝).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
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:
simpa using

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

Goal state before:
pp: case pred
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
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x : V
hx : (ρ g) x = x
i : ℕ
h : (ρ ((fun x ↦ g ^ x) (-↑i))) x = x
⊢ (ρ ((fun x ↦ g ^ x) (-↑i - 1))) x = x

Tactic:
simpa using

Goal state after:
case pred
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
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x : V
hx : (ρ g) x = x
i : ℕ
h : (ρ ((fun x ↦ g ^ x) (-↑i))) x = x
⊢ (ρ g⁻¹) ((ρ (g ^ i)⁻¹) x) = x
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁴ : CommRing k
inst✝³ : Group G
V : Type u_5
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
S : Subgroup G
inst✝ : S.Normal
g : G
x : V
hx : x ∈ invariants (MonoidHom.comp ρ S.subtype)
x✝ : ↥S
s : G
hs : s ∈ S
⊢ ((MonoidHom.comp ρ S.subtype) ⟨s, hs⟩) ((ρ g) x) = (ρ g) x

Tactic:
simpa using

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁴ : CommRing k
inst✝³ : Group G
V : Type u_5
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
S : Subgroup G
inst✝ : S.Normal
g : G
x : V
hx : x ∈ invariants (MonoidHom.comp ρ S.subtype)
x✝ : ↥S
s : G
hs : s ∈ S
⊢ (ρ s) ((ρ g) x) = (ρ g) x
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V✝ : Type u_3
W : Type u_4
inst✝⁸ : CommRing k
inst✝⁷ : Group G
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module k V✝
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
ρ✝ : Representation k G V✝
σ : Representation k G W
V : Type u_5
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
S : Subgroup G
inst✝ : S.Normal
g : ↥S
x✝ : ↥(invariants (MonoidHom.comp ρ S.subtype))
x : V
hx : x ∈ invariants (MonoidHom.comp ρ S.subtype)
⊢ ↑(((MonoidHom.comp (ρ.toInvariants S) S.subtype) g) ⟨x, hx⟩) = ↑(LinearMap.id ⟨x, hx⟩)

Tactic:
simpa using

Goal state after:
k : Type u_1
G : Type u_2
V✝ : Type u_3
W : Type u_4
inst✝⁸ : CommRing k
inst✝⁷ : Group G
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module k V✝
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
ρ✝ : Representation k G V✝
σ : Representation k G W
V : Type u_5
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
S : Subgroup G
inst✝ : S.Normal
g : ↥S
x✝ : ↥(invariants (MonoidHom.comp ρ S.subtype))
x : V
hx : x ∈ invariants (MonoidHom.comp ρ S.subtype)
⊢ (ρ ↑g) x = x
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝⁹ : Group G
inst✝⁸ : Field k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : FiniteDimensional k V
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
⊢ (↑(Nat.card G))⁻¹ * ∑ g, σ.character g * ρ.character g⁻¹ = ↑(finrank k (ρ.IntertwiningMap σ))

Tactic:
by
  simp_rw [mul_comm, ← char_linHom, card_inv_mul_sum_char_eq_finrank,
    (invariantsEquivIntertwiningMap ρ σ).finrank_eq]

Goal state after:
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
h : H
x : H → B
hx : x ∈ coindV φ ρ
g : G
h₁ : H
⊢ (LinearMap.funLeft k B fun x ↦ x * h) x (φ g * h₁) = (ρ g) ((LinearMap.funLeft k B fun x ↦ x * h) x h₁)

Tactic:
simpa using

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
h : H
x : H → B
hx : x ∈ coindV φ ρ
g : G
h₁ : H
⊢ x (φ g * (h₁ * h)) = (ρ g) (x (h₁ * h))