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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
nk : ℕ → ℕ
hnk : ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
n : ℕ
ω : Ω
⊢ (Monotone fun x ↦ σ n x ω) →
    {ω | σ n (mkStrictMonoAux nk n) ω < min (τ n ω) ↑(T n)} ω ≤ {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ω

Tactic:
hω

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
nk : ℕ → ℕ
hnk : ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
n : ℕ
ω : Ω
hω : Monotone fun x ↦ σ n x ω
⊢ {ω | σ n (mkStrictMonoAux nk n) ω < min (τ n ω) ↑(T n)} ω ≤ {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ω
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : ConditionallyCompleteLinearOrderBot ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝² : SecondCountableTopology ι
inst✝¹ : IsFiniteMeasure P
inst✝ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
this : ∑' (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} < ∞
ω : Ω
⊢ (∀ᶠ (n : ℕ) in atTop, ¬σ n (nk n) ω < min (τ n ω) ↑(T n)) →
    Tendsto (fun x ↦ τ x ω) atTop (𝓝 ⊤) → Tendsto (fun x ↦ min (τ x ω) (σ x (nk x) ω)) atTop (𝓝 ⊤)

Tactic:
hω

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : ConditionallyCompleteLinearOrderBot ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝² : SecondCountableTopology ι
inst✝¹ : IsFiniteMeasure P
inst✝ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
this : ∑' (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} < ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, ¬σ n (nk n) ω < min (τ n ω) ↑(T n)
⊢ Tendsto (fun x ↦ τ x ω) atTop (𝓝 ⊤) → Tendsto (fun x ↦ min (τ x ω) (σ x (nk x) ω)) atTop (𝓝 ⊤)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
ω : Ω
⊢ ω ∈ {ω | X ω ∈ Set.Ioi ↑i} → ω ∈ ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}

Tactic:
hω

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
ω : Ω
hω : ω ∈ {ω | X ω ∈ Set.Ioi ↑i}
⊢ ω ∈ ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e_f.e_a
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
j k : ℕ
⊢ k < j → IntervalIntegrable (fun x ↦ x ^ 2) ρ ↑k ↑(k + 1)

Tactic:
_

Goal state after:
case e_f.e_a
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
j k : ℕ
a✝ : k < j
⊢ IntervalIntegrable (fun x ↦ x ^ 2) ρ ↑k ↑(k + 1)
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
k : Type u
inst✝ : CommSemiring k
α : Type w'
g : G
i : α
r s : k
⊢ (leftRegularTensorTrivialIsoFree α) (MonoidAlgebra.single g r ⊗ₜ[k] MonoidAlgebra.single i s) =
    single i (MonoidAlgebra.single g (r * s))

Tactic:
simp [leftRegularTensorTrivialIsoFree]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e_f.e_a.hs
Ω : 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)
N i j : ℕ
⊢ j ∈ range (u i) → MemLp (Y j) 2 ℙ

Tactic:
_

Goal state after:
case e_f.e_a.hs
Ω : 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)
N i j : ℕ
a✝ : j ∈ range (u i)
⊢ MemLp (Y j) 2 ℙ
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e_f.e_a.h
Ω : 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)
N i k : ℕ
⊢ k ∈ ↑(range (u i)) → ∀ ⦃y : ℕ⦄, y ∈ ↑(range (u i)) → k ≠ y → (fun i j ↦ Y i ⟂ᵢ Y j) k y

Tactic:
_

Goal state after:
case e_f.e_a.h
Ω : 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)
N i k : ℕ
a✝ : k ∈ ↑(range (u i))
⊢ ∀ ⦃y : ℕ⦄, y ∈ ↑(range (u i)) → k ≠ y → (fun i j ↦ Y i ⟂ᵢ Y j) k y
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e_f.e_a.h
Ω : 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)
N i k : ℕ
a✝ : k ∈ ↑(range (u i))
l : ℕ
⊢ l ∈ ↑(range (u i)) → k ≠ l → (fun i j ↦ Y i ⟂ᵢ Y j) k l

Tactic:
_

Goal state after:
case e_f.e_a.h
Ω : 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)
N i k : ℕ
a✝¹ : k ∈ ↑(range (u i))
l : ℕ
a✝ : l ∈ ↑(range (u i))
⊢ k ≠ l → (fun i j ↦ Y i ⟂ᵢ Y j) k l
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✝⁵ : 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
e : V ≃ₗ[A] W
he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e
g : G
⊢ (↑e ∘ₗ ↑e.symm) ∘ₗ σ g = (σ g ∘ₗ ↑e) ∘ₗ ↑e.symm

Tactic:
e.comp_symm,

Goal state after:
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
e : V ≃ₗ[A] W
he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e
g : G
⊢ LinearMap.id ∘ₗ σ g = (σ g ∘ₗ ↑e) ∘ₗ ↑e.symm
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✝⁵ : 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
e : V ≃ₗ[A] W
he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e
g : G
⊢ σ g = σ g ∘ₗ ↑e ∘ₗ ↑e.symm

Tactic:
e.comp_symm,

Goal state after:
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
e : V ≃ₗ[A] W
he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e
g : G
⊢ σ g = σ g ∘ₗ LinearMap.id
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
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|} < ∞
ω : Ω
⊢ (∀ᶠ (n : ℕ) in atTop, ¬↑(u n) * ε ≤ |S (u n) ω - ∫ (a : Ω), S (u n) a|) →
    ∀ᶠ (n : ℕ) in atTop,
      |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (range ⌊c ^ n⌋₊).sum Y a| < ε * ↑⌊c ^ n⌋₊

Tactic:
hω

Goal state after:
Ω : 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, ¬↑(u n) * ε ≤ |S (u n) ω - ∫ (a : Ω), S (u n) a|
⊢ ∀ᶠ (n : ℕ) in atTop,
    |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (range ⌊c ^ n⌋₊).sum Y a| < ε * ↑⌊c ^ n⌋₊
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
v : ℕ → ℝ
v_pos : ∀ (n : ℕ), 0 < v n
v_lim : Tendsto v atTop (𝓝 0)
this :
  ∀ (i : ℕ),
    ∀ᵐ (ω : Ω),
      ∀ᶠ (n : ℕ) in atTop,
        |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| <
          v i * ↑⌊c ^ n⌋₊
ω : Ω
⊢ (∀ (i : ℕ),
      ∀ᶠ (n : ℕ) in atTop,
        |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| <
          v i * ↑⌊c ^ n⌋₊) →
    (fun n ↦
        ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω -
          ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a) =o[atTop]
      fun n ↦ ↑⌊c ^ n⌋₊

Tactic:
hω

Goal state after:
Ω : 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
v : ℕ → ℝ
v_pos : ∀ (n : ℕ), 0 < v n
v_lim : Tendsto v atTop (𝓝 0)
this :
  ∀ (i : ℕ),
    ∀ᵐ (ω : Ω),
      ∀ᶠ (n : ℕ) in atTop,
        |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| <
          v i * ↑⌊c ^ n⌋₊
ω : Ω
hω :
  ∀ (i : ℕ),
    ∀ᶠ (n : ℕ) in atTop,
      |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a| <
        v i * ↑⌊c ^ n⌋₊
⊢ (fun n ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω -
        ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a) =o[atTop]
    fun n ↦ ↑⌊c ^ n⌋₊
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
ω : Ω
⊢ ((fun n ↦
        ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω -
          ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a) =o[atTop]
      fun n ↦ ↑⌊c ^ n⌋₊) →
    (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊

Tactic:
hω

Goal state after:
Ω : 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ω :
  (fun n ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω -
        ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a) =o[atTop]
    fun n ↦ ↑⌊c ^ n⌋₊
⊢ (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
j : ℕ
⊢ ℙ {ω | X j ω ∈ Set.Ioi ↑j} = ℙ {ω | X 0 ω ∈ Set.Ioi ↑j}

Tactic:
exact (hident j).measure_mem_eq measurableSet_Ioi

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ∞
ω : Ω
⊢ (∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi ↑n) → Tendsto (fun n ↦ truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)

Tactic:
hω

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, X n ω ∉ Set.Ioi ↑n
⊢ Tendsto (fun n ↦ truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ∞
B : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)
ω : Ω
⊢ Tendsto (fun n ↦ truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0) →
    (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n

Tactic:
hω

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ∞
B : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)
ω : Ω
hω : Tendsto (fun n ↦ truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)
⊢ (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
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
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
⊢ ((fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊) →
    ((fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n) →
      Tendsto (fun n ↦ (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) / ↑⌊c ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))

Tactic:
hω

Goal state after:
Ω : 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⌋₊
⊢ ((fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n) →
    Tendsto (fun n ↦ (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) / ↑⌊c ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
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)
⊢ (Hom.hom f).toLinearMap c✝ ∈ Y.ρ.invariants

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: Ω : 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 : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
this :
  ∀ (k : ℕ), ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ↑⌊c k ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
ω : Ω
⊢ (∀ (i : ℕ), Tendsto (fun n ↦ (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) / ↑⌊c i ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))) →
    Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (a : Ω), X 0 a))

Tactic:
hω

Goal state after:
Ω : 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 : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
this :
  ∀ (k : ℕ), ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ↑⌊c k ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
ω : Ω
hω : ∀ (i : ℕ), Tendsto (fun n ↦ (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) / ↑⌊c i ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
⊢ Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (a : Ω), X 0 a))
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Monoid G
V W : FDRep k G
i : V ≅ W
g : G
⊢ V.character g = W.character g

Tactic:
simp only [character, FDRep.Iso.conj_ρ i]

Goal state after:
k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Monoid G
V W : FDRep k G
i : V ≅ W
g : G
⊢ (trace k ↑V.V) (V.ρ g) = (trace k ↑W.V) ((isoToLinearEquiv i).conj (V.ρ g))
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ∀ᵐ (ω : Ω), X 0 ω = 0
I : ∀ᵐ (ω : Ω), ∀ (i : ℕ), X i ω = 0
ω : Ω
⊢ (∀ (i : ℕ), X i ω = 0) → Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
hω

Goal state after:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ∀ᵐ (ω : Ω), X 0 ω = 0
I : ∀ᵐ (ω : Ω), ∀ (i : ℕ), X i ω = 0
ω : Ω
hω : ∀ (i : ℕ), X i ω = 0
⊢ Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))