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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X ↑i) → E
hf : AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)
⊢ ∫ (y : (i : ↥s) → X ↑i), f y ∂Measure.map s.restrict (infinitePi μ) =
    ∫ (y : (i : ↥s) → X ↑i), f y ∂Measure.pi fun i ↦ μ ↑i

pp: case hφ
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X ↑i) → E
hf : AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)
⊢ AEMeasurable s.restrict (infinitePi μ)

pp: case hfm
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X ↑i) → E
hf : AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)
⊢ AEStronglyMeasurable f (Measure.map s.restrict (infinitePi μ))

Tactic:
infinitePi_map_restrict

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X ↑i) → E
hf : AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)
⊢ (∫ (y : (i : ↥s) → X ↑i), f y ∂Measure.pi fun i ↦ μ ↑i) = ∫ (y : (i : ↥s) → X ↑i), f y ∂Measure.pi fun i ↦ μ ↑i

case hφ
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X ↑i) → E
hf : AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)
⊢ AEMeasurable s.restrict (infinitePi μ)

case hfm
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X ↑i) → E
hf : AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)
⊢ AEStronglyMeasurable f (Measure.map s.restrict (infinitePi μ))
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case hfm
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X ↑i) → E
hf : AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)
⊢ AEStronglyMeasurable f (Measure.map s.restrict (infinitePi μ))

Tactic:
infinitePi_map_restrict

Goal state after:
case hfm
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X ↑i) → E
hf : AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)
⊢ AEStronglyMeasurable f (Measure.pi fun i ↦ μ ↑i)
Module: Mathlib.Probability.Distributions.Beta

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ ∫ (a : ℝ) in Ioo 0 1, a ^ (α - 1) * (1 - a) ^ (β - 1) = ((↑α).betaIntegral ↑β).re

Tactic:
betaIntegral,

Goal state after:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ ∫ (a : ℝ) in Ioo 0 1, a ^ (α - 1) * (1 - a) ^ (β - 1) = (∫ (x : ℝ) in 0..1, ↑x ^ (↑α - 1) * (1 - ↑x) ^ (↑β - 1)).re
Module: Mathlib.Probability.Distributions.Beta

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ 0 ≤ 1

Tactic:
norm_num

Goal state after:
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0..x, r * rexp (-(r * a))
⊢ -1 * rexp (-(r * x)) - -1 * rexp (-(r * 0)) = 1 - rexp (-(r * x))

Tactic:
norm_num

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0..x, r * rexp (-(r * a))
⊢ -rexp (-(r * x)) + 1 = 1 - rexp (-(r * x))
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ℝ
⊢ Measurable (geometricPMFReal p)

Tactic:
by
  fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm

Goal state before:
pp: p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun n ↦ ↑n * p n) atTop (𝓝 r)
⊢ 0 < 1 / 2

Tactic:
norm_num

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r : ℝ≥0
t : ℝ
⊢ charFun Po(ℝ, r) t = cexp (↑↑r * (cexp (↑t * I) - 1))

Tactic:
charFun_apply,

Goal state after:
r : ℝ≥0
t : ℝ
⊢ ∫ (x : ℝ), cexp (↑(inner ℝ x t) * I) ∂Po(ℝ, r) = cexp (↑↑r * (cexp (↑t * I) - 1))
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
⊢ ((p a' * if h : p a' = 0 then 0 else (f a' h) b) *
      if h : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0 then 0 else (g b ⋯) a) =
    p a' * if h : p a' = 0 then 0 else (f a' h) b * if h : (f a' h) b = 0 then 0 else (g b ⋯) a

Tactic:
split_ifs with h _ h_1 H h_2

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : p a' = 0
_ : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
⊢ p a' * 0 * 0 = p a' * 0

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : p a' = 0
_ : ¬∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
⊢ p a' * 0 * (g b ⋯) a = p a' * 0

case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
H : (f a' h) b = 0
⊢ p a' * (f a' h) b * 0 = p a' * ((f a' h) b * 0)

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
H : ¬(f a' h) b = 0
⊢ p a' * (f a' h) b * 0 = p a' * ((f a' h) b * (g b ⋯) a)

case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ¬∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
h_2 : (f a' h) b = 0
⊢ p a' * (f a' h) b * (g b ⋯) a = p a' * ((f a' h) b * 0)

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ¬∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
h_2 : ¬(f a' h) b = 0
⊢ p a' * (f a' h) b * (g b ⋯) a = p a' * ((f a' h) b * (g b ⋯) a)
Module: Mathlib.Probability.Distributions.TwoValued

Goal state before:
pp: case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {m₀ : MeasurableSpace Ω},
    m ≤ m₀ →
      ∀ {μ : Measure Ω} [IsFiniteMeasure μ],
        AEMeasurable X μ →
          (∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) → Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
Y : Ω → ℝ
hYmeas : Measurable Y
hXY : X =ᵐ[μ] Y
⊢ μ[Y | m] =ᵐ[μ] μ[X | m]

Tactic:
exact condExp_congr_ae <| by filter_upwards [hXY] with ω hω; simp [hω]

Goal state after:
Module: Mathlib.Probability.Distributions.TwoValued

Goal state before:
pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {m₀ : MeasurableSpace Ω},
    m ≤ m₀ →
      ∀ {μ : Measure Ω} [IsFiniteMeasure μ],
        AEMeasurable X μ →
          (∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) → Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
Y : Ω → ℝ
hYmeas : Measurable Y
hXY : X =ᵐ[μ] Y
⊢ μ[1 - Y | m] =ᵐ[μ] μ[1 - X | m]

Tactic:
exact condExp_congr_ae <| by filter_upwards [hXY] with ω hω; simp [hω]

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ map s.restrict (infinitePi fun i ↦ map (X i) P) = Measure.pi fun i ↦ map (s.restrict X i) P

pp: case hg
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ AEMeasurable s.restrict (map (fun ω i ↦ X i ω) P)

pp: case hf
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ AEMeasurable (fun ω i ↦ X i ω) P

Tactic:
infinitePi_map_restrict

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ (Measure.pi fun i ↦ map (X ↑i) P) = Measure.pi fun i ↦ map (s.restrict X i) P

case hg
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ AEMeasurable s.restrict (map (fun ω i ↦ X i ω) P)

case hf
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ AEMeasurable (fun ω i ↦ X i ω) P
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : Nonempty Ω
ω : Ω
⊢ (condExpKernel μ m) ω = (condDistrib id id μ) (id ω)

Tactic:
by
  simp [condExpKernel_eq, Kernel.comap_apply]

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndepSets m' hm' (fun i ↦ {s i}) μ ↔
    ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω ↦ 1 | m']

Tactic:
rw [iCondIndepSets_iff]

Goal state after:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (s_1 : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s_1, f i ∈ {s i}) →
        μ[(⋂ i ∈ s_1, f i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s_1, μ[(f i).indicator fun ω ↦ 1 | m']) ↔
    ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(s i).indicator fun ω ↦ 1 | m']

case hπ
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ (i : ι), ∀ s_1 ∈ {s i}, MeasurableSet s_1
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁹ : (s : S) → TopologicalSpace (E s)
inst✝⁸ : (s : S) → MeasurableSpace (E s)
inst✝⁷ : ∀ (s : S), BorelSpace (E s)
inst✝⁶ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : IsFiniteMeasure P
inst✝ : Finite S
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ (f fun x ↦ X x ω) * g (U ω)) x ∂P =
      (∫ (x : Ω), (fun ω ↦ f fun x ↦ X x ω) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
this : Fintype S
⊢ (fun ω s ↦ X s ω) ⟂ᵢ[P] U

Tactic:
refine pi_indepFun_of_prod_bcf mX mU fun f g ↦ ?_

Goal state after:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
H : Type u_7
inst✝⁹ : (s : S) → TopologicalSpace (E s)
inst✝⁸ : (s : S) → MeasurableSpace (E s)
inst✝⁷ : ∀ (s : S), BorelSpace (E s)
inst✝⁶ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁵ : TopologicalSpace H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : HasOuterApproxClosed H
X : (s : S) → Ω → E s
U : Ω → H
inst✝¹ : IsFiniteMeasure P
inst✝ : Finite S
mX : ∀ (s : S), AEMeasurable (X s) P
mU : AEMeasurable U P
h :
  ∀ (f : ((s : S) → E s) →ᵇ ℝ) (g : H →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ (f fun x ↦ X x ω) * g (U ω)) x ∂P =
      (∫ (x : Ω), (fun ω ↦ f fun x ↦ X x ω) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
g : H →ᵇ ℝ
⊢ ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ⇑g ∘ U) x ∂P = (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (⇑g ∘ U) x ∂P
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : 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']
i : ι
⊢ i ∈ s → sets i = f i ⁻¹' g i

Tactic:
hi

Goal state after:
Ω : 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']
i : ι
hi : i ∈ s
⊢ sets i = f i ⁻¹' g i
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : 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
⊢ CondIndepFun m' hm' X Y μ

Tactic:
rw [condIndepFun_iff _ hm' _ _ (hX.mono hm' le_rfl) hY]

Goal state after:
Ω : 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
⊢ ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
⊢ ∃ f, Measurable (uncurry f) ∧ ∀ (a : X), Measure.map (f a) volume = κ a

Tactic:
have measurable_f : Measurable (uncurry f) := by
    refine measurable_of_Ioi fun a ↦ ?_
    simp only [preimage, uncurry, mem_Ioi]
    have h_monotone s : Monotone (fun x ↦ (κ s).real (Icc 0 x)) :=
      fun x y hxy ↦ measureReal_mono (by gcongr)
    have sSup_eq_iUnion_rat : {x : X × I | a < f x.1 x.2} =
        ⋃ (q : ℚ) (hqI : ↑q ∈ I) (_ : a < (q : ℝ)), {e | (κ e.1).real (Icc 0 ⟨q, hqI⟩) < e.2} := by
      ext e
      simp_all only [lt_sSup_iff, mem_ofPred_eq, Subtype.exists, mem_Icc, Rat.cast_nonneg,
        mem_iUnion, exists_prop, exists_and_left, f]
      constructor
      · rintro ⟨y, hyI, y_mem, (hy : a.1 < y)⟩
        obtain ⟨q, hqa, hqy⟩ := exists_rat_btwn hy
        refine ⟨q, hqa, ⟨?_, hqy.le.trans hyI.2⟩, lt_of_lt_of_le' y_mem (h_monotone e.1 hqy.le)⟩
        simp [← Rat.cast_nonneg (K := ℝ), a.2.1.trans hqa.le]
      · intro he
        obtain ⟨q, hqa, hqI, h⟩ := he
        refine ⟨q, ⟨by simp [hqI.1], hqI.2⟩, h, ?_⟩
        change a.1 < q
        simp [hqa]
    rw [sSup_eq_iUnion_rat]
    refine MeasurableSet.iUnion (fun b ↦ MeasurableSet.iUnion
      (fun bI ↦ MeasurableSet.iUnion (fun _ ↦ ?_)))
    refine measurableSet_lt ?_ measurable_snd.subtype_val
    simp_rw [measureReal_def]
    have hκ := κ.measurable_coe (s := Icc 0 ⟨b, bI⟩) measurableSet_Icc
    fun_prop

Goal state after:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
⊢ ∃ f, Measurable (uncurry f) ∧ ∀ (a : X), Measure.map (f a) volume = κ a
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✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝² : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst✝¹ : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_countable_range : (Set.range τ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
this : Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i}
i : WithTop ι
⊢ i ∈ Set.range τ → stoppedValue f τ =ᵐ[μ.restrict {x | τ x = i}] μ[f n | hτ.measurableSpace]

Tactic:
hi

Goal state after:
Ω : 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✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝² : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst✝¹ : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_countable_range : (Set.range τ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
this : Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i}
i : WithTop ι
hi : i ∈ Set.range τ
⊢ stoppedValue f τ =ᵐ[μ.restrict {x | τ x = i}] μ[f n | hτ.measurableSpace]
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
⊢ (∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')) → ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')

Tactic:
hi

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
⊢ ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ (∫⁻ (a : Ω), ‖X a‖ₑ ^ (↑p).toReal ∂μ.tilted fun x ↦ t * X x) < ∞

Tactic:
simp_rw [ENNReal.coe_toReal, ← ofReal_norm, norm_eq_abs,
    ENNReal.ofReal_rpow_of_nonneg (x := |X _|) (p := p) (abs_nonneg (X _)) p.2]

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ (∫⁻ (a : Ω), ENNReal.ofReal (|X a| ^ ↑p) ∂μ.tilted fun x ↦ t * X x) < ∞
Module: Mathlib.Probability.ProbabilityMassFunction.Binomial

Goal state before:
pp: case e'_2
p : ℝ≥0
h : p ≤ 1
n i : ℕ
⊢ i ∈ Finset.range (n + 1) →
    (if h : i < n + 1 then p ^ ↑⟨i, h⟩ * (1 - p) ^ (n - ↑⟨i, h⟩) * ↑(n.choose ↑⟨i, h⟩) else 0) =
      p ^ i * (1 - p) ^ (n - i) * ↑(n.choose i)

Tactic:
hi

Goal state after:
case e'_2
p : ℝ≥0
h : p ≤ 1
n i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ (if h : i < n + 1 then p ^ ↑⟨i, h⟩ * (1 - p) ^ (n - ↑⟨i, h⟩) * ↑(n.choose ↑⟨i, h⟩) else 0) =
    p ^ i * (1 - p) ^ (n - i) * ↑(n.choose i)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h'✝ : X =ᵐ[⇑κ ∘ₘ ν] Y
h'' : ∀ᵐ (ω' : Ω') ∂ν, ∀ᵐ (ω : Ω) ∂κ ω', X ω = Y ω
ω' : Ω'
h_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h' : ∀ᵐ (ω : Ω) ∂κ ω', X ω = Y ω
t : ℝ
⊢ mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
exact h_mgf t

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 ρ
i : ℕ
a✝ : i ∈ range N
⊢ (↑i + 1) * ∫ (x : ℝ) in ↑i..↑(i + 1), 1 ∂ρ ≤ ∫ (x : ℝ) in ↑i..↑(i + 1), x + 1 ∂ρ

Tactic:
have I : (i : ℝ) ≤ (i + 1 : ℕ) := by
          simp only [Nat.cast_add, Nat.cast_one, le_add_iff_nonneg_right, zero_le_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 ρ
i : ℕ
a✝ : i ∈ range N
I : ↑i ≤ ↑(i + 1)
⊢ (↑i + 1) * ∫ (x : ℝ) in ↑i..↑(i + 1), 1 ∂ρ ≤ ∫ (x : ℝ) in ↑i..↑(i + 1), x + 1 ∂ρ