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

Goal state before:
pp: case refine_2.hg
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f₁ f₂ : X → ℝ≥0∞
a✝¹ : Measurable f₁
a✝ : Measurable f₂
hf₁ : ∫⁻ (x : X), B.indicator 1 x * f₁ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂π x₀
hf₂ : ∫⁻ (x : X), B.indicator 1 x * f₂ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₂ x ∂π x₀
⊢ Measurable f₂

pp: case refine_2.hg
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f₁ f₂ : X → ℝ≥0∞
a✝¹ : Measurable f₁
a✝ : Measurable f₂
hf₁ : ∫⁻ (x : X), B.indicator 1 x * f₁ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂π x₀
hf₂ : ∫⁻ (x : X), B.indicator 1 x * f₂ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₂ x ∂π x₀
⊢ Measurable fun x ↦ B.indicator 1 x * f₂ x

Tactic:
<;>

Goal state after:
case refine_2.hg
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f₁ f₂ : X → ℝ≥0∞
a✝¹ : Measurable f₁
a✝ : Measurable f₂
hf₁ : ∫⁻ (x : X), B.indicator 1 x * f₁ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂π x₀
hf₂ : ∫⁻ (x : X), B.indicator 1 x * f₂ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₂ x ∂π x₀
⊢ Measurable f₂

case refine_2.hg
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f₁ f₂ : X → ℝ≥0∞
a✝¹ : Measurable f₁
a✝ : Measurable f₂
hf₁ : ∫⁻ (x : X), B.indicator 1 x * f₁ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂π x₀
hf₂ : ∫⁻ (x : X), B.indicator 1 x * f₂ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₂ x ∂π x₀
⊢ Measurable fun x ↦ B.indicator 1 x * f₂ x
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: case hs
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
f : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hA : MeasurableSet A
hB : MeasurableSet B
x₀ : X
⊢ MeasurableSet A

pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
f : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hA : MeasurableSet A
hB : MeasurableSet B
x₀ : X
⊢ Measurable (A.indicator f)

Tactic:
<;>

Goal state after:
case hs
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
f : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hA : MeasurableSet A
hB : MeasurableSet B
x₀ : X
⊢ MeasurableSet A

X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
f : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hA : MeasurableSet A
hB : MeasurableSet B
x₀ : X
⊢ Measurable (A.indicator f)
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case e'_4.f
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω ↦ 1 | m']
hg : ∀ i ∈ s, sets i = f i ⁻¹' g i
i : ι
hi : i ∈ s
⊢ sets i = f i ⁻¹' g i

pp: case e'_5.a
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω ↦ 1 | m']
hg : ∀ i ∈ s, sets i = f i ⁻¹' g i
i : ι
hi : i ∈ s
⊢ sets i = f i ⁻¹' g i

Tactic:
<;>

Goal state after:
case e'_4.f
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω ↦ 1 | m']
hg : ∀ i ∈ s, sets i = f i ⁻¹' g i
i : ι
hi : i ∈ s
⊢ sets i = f i ⁻¹' g i

case e'_5.a
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω ↦ 1 | m']
hg : ∀ i ∈ s, sets i = f i ⁻¹' g i
i : ι
hi : i ∈ s
⊢ sets i = f i ⁻¹' g i
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
ω : Ω
h : ω ∈ X ⁻¹' s
⊢ ‖1 ω‖ ≤ 1

pp: case neg
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
ω : Ω
h : ω ∉ X ⁻¹' s
⊢ ‖0‖ ≤ 1

Tactic:
<;>

Goal state after:
case pos
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
ω : Ω
h : ω ∈ X ⁻¹' s
⊢ ‖1 ω‖ ≤ 1

case neg
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
ω : Ω
h : ω ∉ X ⁻¹' s
⊢ ‖0‖ ≤ 1
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ Kernel.deterministic (fun x ↦ PUnit.unit) ⋯ ∥ₖ Kernel.deterministic id ⋯ ∘ₖ Kernel.deterministic Function.diag ⋯ =
    (Kernel.deterministic id ⋯).map fun x ↦ (PUnit.unit, x)

Tactic:
Kernel.deterministic_parallelComp_deterministic,

Goal state after:
X : SFinKer
⊢ Kernel.deterministic (Prod.map (fun x ↦ PUnit.unit) id) ⋯ ∘ₖ Kernel.deterministic Function.diag ⋯ =
    (Kernel.deterministic id ⋯).map fun x ↦ (PUnit.unit, x)
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ Kernel.deterministic id ⋯ ∥ₖ Kernel.deterministic (fun x ↦ PUnit.unit) ⋯ ∘ₖ Kernel.deterministic Function.diag ⋯ =
    (Kernel.deterministic id ⋯).map fun x ↦ (x, PUnit.unit)

Tactic:
Kernel.deterministic_parallelComp_deterministic,

Goal state after:
X : SFinKer
⊢ Kernel.deterministic (Prod.map id fun x ↦ PUnit.unit) ⋯ ∘ₖ Kernel.deterministic Function.diag ⋯ =
    (Kernel.deterministic id ⋯).map fun x ↦ (x, PUnit.unit)
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: case pos
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
ω : Ω
h✝ : ω ∈ A
⊢ f (1 ω) * ∏ s, (g s) (X s ω) =
    A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
      A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω

pp: case neg
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
ω : Ω
h✝ : ω ∉ A
⊢ f 0 * ∏ s, (g s) (X s ω) =
    A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
      A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω

Tactic:
<;>

Goal state after:
case pos
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
ω : Ω
h✝ : ω ∈ A
⊢ f (1 ω) * ∏ s, (g s) (X s ω) =
    A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
      A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω

case neg
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
ω : Ω
h✝ : ω ∉ A
⊢ f 0 * ∏ s, (g s) (X s ω) =
    A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
      A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ ↑i
⊢ MeasurableSet {ω | τ ω ≤ σ ω}

Tactic:
exact hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ)

Goal state after:
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
this :
  ∀ᵐ (x : Ω) ∂μ.restrict {x | τ x ≤ σ x},
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
⊢ MeasurableSet {x | τ x ≤ σ x}

Tactic:
exact hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ)

Goal state after:
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: case e'_2
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : IsProbabilityMeasure P
inst✝ : Finite S
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : ((s : S) → E s) →ᵇ ℝ), ∫ (ω : Ω) in A, f fun x ↦ X x ω ∂P = P.real A * ∫ (ω : Ω), f fun x ↦ X x ω ∂P
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
x✝ : Ω
⊢ ∏ s, (f s) (X s x✝) = (∏ s, (f s).compContinuous { toFun := Function.eval s, continuous_toFun := ⋯ }) fun x ↦ X x x✝

pp: case e'_3
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : IsProbabilityMeasure P
inst✝ : Finite S
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : ((s : S) → E s) →ᵇ ℝ), ∫ (ω : Ω) in A, f fun x ↦ X x ω ∂P = P.real A * ∫ (ω : Ω), f fun x ↦ X x ω ∂P
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
x✝ : Ω
⊢ ∏ s, (f s) (X s x✝) = (∏ s, (f s).compContinuous { toFun := Function.eval s, continuous_toFun := ⋯ }) fun x ↦ X x x✝

Tactic:
<;>

Goal state after:
case e'_2
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : IsProbabilityMeasure P
inst✝ : Finite S
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : ((s : S) → E s) →ᵇ ℝ), ∫ (ω : Ω) in A, f fun x ↦ X x ω ∂P = P.real A * ∫ (ω : Ω), f fun x ↦ X x ω ∂P
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
x✝ : Ω
⊢ ∏ s, (f s) (X s x✝) = (∏ s, (f s).compContinuous { toFun := Function.eval s, continuous_toFun := ⋯ }) fun x ↦ X x x✝

case e'_3
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : IsProbabilityMeasure P
inst✝ : Finite S
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : ((s : S) → E s) →ᵇ ℝ), ∫ (ω : Ω) in A, f fun x ↦ X x ω ∂P = P.real A * ∫ (ω : Ω), f fun x ↦ X x ω ∂P
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
x✝ : Ω
⊢ ∏ s, (f s) (X s x✝) = (∏ s, (f s).compContinuous { toFun := Function.eval s, continuous_toFun := ⋯ }) fun x ↦ X x x✝
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case neg.right
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : HasFiniteIntegral (fun ω ↦ rexp (↑p * t * X ω)) (⇑κ ∘ₘ ν)
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ ↑p ∂⇑κ ∘ₘ ν < ∞

Tactic:
rw [hasFiniteIntegral_def] at h'

Goal state after:
case neg.right
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : ∫⁻ (a : Ω), ‖rexp (↑p * t * X a)‖ₑ ∂⇑κ ∘ₘ ν < ∞
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ ↑p ∂⇑κ ∘ₘ ν < ∞
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: case e'_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : HasOuterApproxClosed G
Z : Ω → G
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P
f : Unit → G →ᵇ ℝ
x✝ : Ω
⊢ ∏ s, (f s) (Z x✝) = (f ()) (Z x✝)

pp: case e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : HasOuterApproxClosed G
Z : Ω → G
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P
f : Unit → G →ᵇ ℝ
x✝ : Ω
⊢ ∏ s, (f s) (Z x✝) = (f ()) (Z x✝)

Tactic:
<;>

Goal state after:
case e'_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : HasOuterApproxClosed G
Z : Ω → G
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P
f : Unit → G →ᵇ ℝ
x✝ : Ω
⊢ ∏ s, (f s) (Z x✝) = (f ()) (Z x✝)

case e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : HasOuterApproxClosed G
Z : Ω → G
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P
f : Unit → G →ᵇ ℝ
x✝ : Ω
⊢ ∏ s, (f s) (Z x✝) = (f ()) (Z x✝)
Module: Mathlib.Probability.ProbabilityMassFunction.Binomial

Goal state before:
pp: case «0»
p : ℝ≥0
h : p ≤ 1
⊢ (binomial p h 1) ((fun i ↦ i) ⟨0, ⋯⟩) = (map (fun x ↦ bif x then 1 else 0) (bernoulli p h)) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
p : ℝ≥0
h : p ≤ 1
⊢ (binomial p h 1) ((fun i ↦ i) ⟨1, ⋯⟩) = (map (fun x ↦ bif x then 1 else 0) (bernoulli p h)) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
p : ℝ≥0
h : p ≤ 1
⊢ (binomial p h 1) ((fun i ↦ i) ⟨0, ⋯⟩) = (map (fun x ↦ bif x then 1 else 0) (bernoulli p h)) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
p : ℝ≥0
h : p ≤ 1
⊢ (binomial p h 1) ((fun i ↦ i) ⟨1, ⋯⟩) = (map (fun x ↦ bif x then 1 else 0) (bernoulli p h)) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p q : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
⊢ Locally (fun Y ↦ p Y ∧ q Y) 𝓕 X P ↔ Locally p 𝓕 X P ∧ Locally q 𝓕 X P

Tactic:
refine ⟨Locally.of_and, fun ⟨hpX, hqX⟩ ↦
    ⟨_, hpX.isLocalizingSequence_localSeq.min hqX.isLocalizingSequence_localSeq, fun n ↦ ?_⟩⟩
  suffices ∀ (p q : (ι → Ω → E) → Prop) (hp : IsStable 𝓕 p) (hq : IsStable 𝓕 q)
      (hpX : Locally p 𝓕 X P) (hqX : Locally q 𝓕 X P),
      p (stoppedProcess (fun i ↦ {ω | ⊥ < (hpX.localSeq ⊓ hqX.localSeq) n ω}.indicator (X i))
      ((hpX.localSeq ⊓ hqX.localSeq) n)) by
    refine ⟨this p q hp hq hpX hqX, ?_⟩
    simp_rw [inf_comm hpX.localSeq]
    exact this q p hq hp hqX hpX
  intro p q hp hq hpX hqX
  convert!
    hp _ (hpX.stoppedProcess_localSeq n) _ <|
      hqX.isLocalizingSequence_localSeq.isStoppingTime n using 1
  ext i ω
  simp_rw [stoppedProcess_indicator_comm, Pi.inf_apply, lt_inf_iff, inf_comm (hpX.localSeq n)]
  rw [← stoppedProcess_stoppedProcess, ← stoppedProcess_indicator_comm, Set.ofPred_and,
    Set.inter_comm]
  simp_rw [← Set.indicator_indicator]
  rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
σ : Subrepresentation (Representation.ofModule M)
m : M
hm : m ∈ σ.toSubmodule.carrier
g : G
a : A
⊢ MonoidAlgebra.single g 1 • m ∈ σ.toSubmodule.carrier

Tactic:
by
        simpa [Representation.ofModule, RestrictScalars.lsmul] using! σ.apply_mem_toSubmodule g hm

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cX
q : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cY
ω' : Ω'
hmX : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑cX * t ^ 2 / 2)
hmY : ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑cY * t ^ 2 / 2)
hlX : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')
hlY : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * Y ω)) (↑q) (κ ω')
t : ℝ
⊢ mgf (fun ω ↦ X ω + Y ω) (κ ω') t ≤ rexp (↑((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) * t ^ 2 / 2)

Tactic:
calc (κ ω')[fun ω ↦ exp (t * (X ω + Y ω))]
      _ ≤ (κ ω')[fun ω ↦ exp (t * X ω) ^ (p : ℝ)] ^ (1 / (p : ℝ)) *
          (κ ω')[fun ω ↦ exp (t * Y ω) ^ (q : ℝ)] ^ (1 / (q : ℝ)) := by
        simp_rw [mul_add, exp_add]
        apply integral_mul_le_Lp_mul_Lq_of_nonneg
        · exact ⟨by simp [field, p, q], by positivity, by positivity⟩
        · exact ae_of_all _ fun _ ↦ exp_nonneg _
        · exact ae_of_all _ fun _ ↦ exp_nonneg _
        · simpa using (hlX t)
        · simpa using (hlY t)
      _ ≤ exp (cX * (t * p) ^ 2 / 2) ^ (1 / (p : ℝ)) *
          exp (cY * (t * q) ^ 2 / 2) ^ (1 / (q : ℝ)) := by
        simp_rw [← exp_mul _ p, ← exp_mul _ q, mul_right_comm t _ p, mul_right_comm t _ q]
        gcongr
        · exact hmX (t * p)
        · exact hmY (t * q)
      _ = exp ((cX.sqrt + cY.sqrt) ^ 2 * t ^ 2 / 2) := by
        simp_rw [← exp_mul, ← exp_add]
        simp only [NNReal.coe_div, NNReal.coe_add, coe_sqrt, one_div, inv_div, exp_eq_exp, p, q]
        field_simp
        linear_combination t ^ 2 * (-√↑cY * Real.sq_sqrt cX.coe_nonneg
            -√↑cX * Real.sq_sqrt cY.coe_nonneg)

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h₂
Ω : 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 ρ
⊢ ρ.real (Set.Ioc 0 ↑N) ≤ 1

Tactic:
rw [← ENNReal.toReal_one]

Goal state after:
case h₂
Ω : 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 ρ
⊢ ρ.real (Set.Ioc 0 ↑N) ≤ ENNReal.toReal 1
Module: Mathlib.RepresentationTheory.AlgebraRepresentation.Basic

Goal state before:
pp: A : Type u_1
V : Type u_2
k : Type u_3
inst✝⁹ : Field k
inst✝⁸ : Ring A
inst✝⁷ : Algebra k A
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k V
inst✝⁴ : Module A V
inst✝³ : IsScalarTower k A V
inst✝² : IsSimpleModule A V
inst✝¹ : FiniteDimensional k V
inst✝ : IsAlgClosed k
⊢ Function.Bijective ⇑(algebraMap k (Module.End A V))

Tactic:
by
  have : Module.Finite k (Module.End A V) := .of_injective (LinearMap.restrictScalarsₗ k A V V k) <|
    LinearMap.restrictScalars_injective _
  classical exact IsAlgClosed.algebraMap_bijective_of_isIntegral (k := k)

Goal state after: