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

Goal state before:
pp: X : ℕ → Type u_1
a : ℕ
x : (i : ↥(Iic a)) → X ↑i
ind : (n : ℕ) → ((i : ↥(Iic n)) → X ↑i) → X (n + 1)
i : ↥(Iic a)
⊢ frestrictLe a (iterateInduction x ind) i = x i

Tactic:
simp only [frestrictLe_apply]

Goal state after:
X : ℕ → Type u_1
a : ℕ
x : (i : ↥(Iic a)) → X ↑i
ind : (n : ℕ) → ((i : ↥(Iic n)) → X ↑i) → X (n + 1)
i : ↥(Iic a)
⊢ iterateInduction x ind ↑i = x i
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a) = 0

Tactic:
by
  rw [Kernel.withDensity_apply']
  · exact setLIntegral_measure_zero _ _ (measure_mutuallySingularSetSlice κ η a)
  · exact measurable_rnDeriv κ η

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
a b : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
g : ((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n) → ℝ≥0∞ := fun c ↦ f (updateFinset c.2 (Iic b) c.1)
η : Kernel ((n : ℕ) → X n) ((i : ↥(Iic b)) → X ↑i) := (partialTraj κ a b).comap (frestrictLe a) ⋯
⊢ Measurable fun x₀ ↦
    ∫⁻ (z : (i : ↥(Iic b)) → X ↑i), f (updateFinset x₀ (Iic b) z) ∂(partialTraj κ a b) (frestrictLe a x₀)

Tactic:
change Measurable fun x₀ ↦ ∫⁻ z : (i : Iic b) → X i, g (z, x₀) ∂η x₀

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
a b : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
g : ((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n) → ℝ≥0∞ := fun c ↦ f (updateFinset c.2 (Iic b) c.1)
η : Kernel ((n : ℕ) → X n) ((i : ↥(Iic b)) → X ↑i) := (partialTraj κ a b).comap (frestrictLe a) ⋯
⊢ Measurable fun x₀ ↦ ∫⁻ (z : (i : ↥(Iic b)) → X ↑i), g (z, x₀) ∂η x₀
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ⇑(Kernel.copy Ω) ∘ₘ μ = ⇑(Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω) ∘ₘ μ

Tactic:
Kernel.swap_copy

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ⇑(Kernel.copy Ω) ∘ₘ μ = ⇑(Kernel.copy Ω) ∘ₘ μ
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
⊢ (fun b ↦ (η b) s) ≤ fun a ↦ 1

Tactic:
intro b

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
b : β
⊢ (fun b ↦ (η b) s) b ≤ (fun a ↦ 1) b
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁶ : IsFiniteMeasure μ
inst✝⁵ : IsFiniteKernel κ
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace 𝓧
inst✝¹ : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst✝ : IsFiniteKernel η
⊢ ⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) ∘ₘ μ =
    ⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ (Kernel.swap Ω Ω ∘ₖ Kernel.copy Ω))) ∘ₘ μ

Tactic:
Kernel.swap_copy

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁶ : IsFiniteMeasure μ
inst✝⁵ : IsFiniteKernel κ
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace 𝓧
inst✝¹ : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst✝ : IsFiniteKernel η
⊢ ⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) ∘ₘ μ =
    ⇑(η ∥ₖ Kernel.id ∘ₖ (κ ∥ₖ Kernel.id ∘ₖ Kernel.copy Ω)) ∘ₘ μ
Module: Mathlib.Probability.Distributions.Beta

Goal state before:
pp: case e'_4
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
hx : x ∈ Ioo 0 1
⊢ (fun x ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) x = betaPDFReal α β x

Tactic:
rw [betaPDFReal, if_pos ⟨hx.1, hx.2⟩]

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

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ ∫⁻ (x : ℝ), betaPDF α β x = 1

Tactic:
by
  rw [lintegral_betaPDF, ← ENNReal.toReal_eq_one_iff, ← integral_eq_lintegral_of_nonneg_ae]
  · simp_rw [mul_assoc, integral_const_mul]
    field_simp
    rw [div_eq_one_iff_eq (ne_of_gt (beta_pos hα hβ)), beta_eq_betaIntegralReal α β hα hβ,
      betaIntegral, intervalIntegral.integral_of_le (by norm_num),
      ← integral_Ioc_eq_integral_Ioo, ← RCLike.re_to_complex, ← integral_re]
    · refine setIntegral_congr_fun measurableSet_Ioc fun x ⟨hx1, hx₂⟩ ↦ ?_
      norm_cast
      rw [← Complex.ofReal_cpow, ← Complex.ofReal_cpow, RCLike.re_to_complex,
        Complex.re_mul_ofReal, Complex.ofReal_re]
      all_goals linarith
    convert! betaIntegral_convergent (u := α) (v := β) (by simpa) (by simpa)
    rw [intervalIntegrable_iff_integrableOn_Ioc_of_le (by simp), IntegrableOn]
  · refine ae_restrict_of_forall_mem measurableSet_Ioo (fun x hx ↦ ?_)
    convert! betaPDFReal_pos hx.1 hx.2 hα hβ |>.le using 1
    rw [betaPDFReal, if_pos ⟨hx.1, hx.2⟩]
  · exact Measurable.aestronglyMeasurable (by fun_prop)

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
⊢ False

Tactic:
suffices 1 < ∑' a, p a from ne_of_lt this p.tsum_coe.symm

Goal state after:
α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
⊢ 1 < ∑' (a : α), p a
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
p : PMF α
a : α
h : p a = 1
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : 0 < ∑' (b : α), if b = a then 0 else p b
⊢ ((if a = a then p a else 0) + ∑' (b : α), if b = a then 0 else p b) =
    (∑' (b : α), if b = a then p b else 0) + ∑' (b : α), if b = a then 0 else p b

Tactic:
congr
      exact symm (tsum_eq_single a fun b hb => if_neg hb)

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
⊢ Function.Injective toMeasure

Tactic:
intro p q h

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
p q : PMF α
h : p.toMeasure = q.toMeasure
⊢ p = q
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝⁴ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝³ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_f : Integrable f ((traj κ a) x₀)
i_f' : Integrable (fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) (Measure.map (frestrictLe b) ((traj κ a) x₀))
⊢ ((traj κ a) x₀)[f | ↑piLE b] =ᵐ[(traj κ a) x₀] fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) (frestrictLe b x)

Tactic:
refine ae_eq_condExp_of_forall_setIntegral_eq (piLE.le _) i_f
    (fun s _ _ ↦ i_f'.comp_aemeasurable (measurable_frestrictLe b).aemeasurable |>.integrableOn)
    ?_ ?_ |>.symm <;> rw [piLE_eq_comap_frestrictLe]

Goal state after:
case refine_1
X : ℕ → Type u_1
inst✝⁴ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝³ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_f : Integrable f ((traj κ a) x₀)
i_f' : Integrable (fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) (Measure.map (frestrictLe b) ((traj κ a) x₀))
⊢ ∀ (s : Set ((i : ℕ) → X i)),
    MeasurableSet s →
      ((traj κ a) x₀) s < ∞ →
        ∫ (x : (i : ℕ) → X i) in s,
            ((fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) ∘ frestrictLe b) x ∂(traj κ a) x₀ =
          ∫ (x : (i : ℕ) → X i) in s, f x ∂(traj κ a) x₀

case refine_2
X : ℕ → Type u_1
inst✝⁴ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝³ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_f : Integrable f ((traj κ a) x₀)
i_f' : Integrable (fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) (Measure.map (frestrictLe b) ((traj κ a) x₀))
⊢ AEStronglyMeasurable ((fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) ∘ frestrictLe b) ((traj κ a) x₀)
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: case e'_6
r : ℝ≥0
⊢ 1 = rexp (-↑r) * NormedSpace.exp ↑r

Tactic:
· simp [← exp_eq_exp_ℝ, ← exp_add]

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)
⊢ Tendsto (fun n ↦ (1 - p n) ^ (n - k)) atTop (𝓝 (Real.exp (-r)))

Tactic:
have hp_lt_half : ∀ᶠ n in atTop, p n < 1 / 2 :=
    (tendsto_zero_of_tendsto_mul_atTop hr).eventually (Iio_mem_nhds (by norm_num))

Goal state after:
p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun n ↦ ↑n * p n) atTop (𝓝 r)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
⊢ Tendsto (fun n ↦ (1 - p n) ^ (n - k)) atTop (𝓝 (Real.exp (-r)))
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
⊢ (p.bindOnSupport f).toOuterMeasure s = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h).toOuterMeasure s

Tactic:
simp only [toOuterMeasure_apply]

Goal state after:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
⊢ ∑' (x : β), s.indicator (⇑(p.bindOnSupport f)) x =
    ∑' (a : α), p a * if h : p a = 0 then 0 else ∑' (x : β), s.indicator (⇑(f a ⋯)) x
Module: Mathlib.Probability.HasCondDistrib

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
𝓩 : Type u_4
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
m𝓩 : MeasurableSpace 𝓩
P : Measure Ω
X : Ω → 𝓧
Y : Ω → 𝓨
κ : Kernel 𝓧 𝓨
inst✝² : SFinite P
inst✝¹ : IsSFiniteKernel κ
Z : Ω → 𝓩
η : Kernel (𝓧 × 𝓨) 𝓩
inst✝ : IsMarkovKernel η
h : HasCondDistrib (fun a ↦ (Y a, Z a)) X (κ ⊗ₖ η) P
hZ : AEMeasurable Z P
hY : AEMeasurable Y P
⊢ Measure.map X P ⊗ₘ κ ⊗ₘ η = Measure.map (fun a ↦ (X a, Y a)) P ⊗ₘ η

Tactic:
by simp [h.fst.map_eq]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : Nonempty α
s : Set α
inst✝¹ : MeasurableSpace α
hs : MeasurableSet s
inst✝ : Fintype ↑s
⊢ (uniformOfFintype α).toMeasure s = ↑(Fintype.card ↑s) / ↑(Fintype.card α)

Tactic:
classical
  simp [uniformOfFintype, Fintype.card_subtype, hs]

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

Goal state before:
pp: case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ map (fun f ↦ f i) (infinitePi fun i ↦ map (fun f j ↦ X i j (f j)) (infinitePi (μ i))) =
    infinitePi fun i_1 ↦ map (fun ω ↦ X i i_1 (ω i i_1)) (infinitePi fun i ↦ infinitePi (μ i))

pp: case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ ∀ (i : ι), Measurable fun f j ↦ X i j (f j)

Tactic:
@infinitePi_map_eval ..,

Goal state after:
case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ map (fun f j ↦ X i j (f j)) (infinitePi (μ i)) =
    infinitePi fun i_1 ↦ map (fun ω ↦ X i i_1 (ω i i_1)) (infinitePi fun i ↦ infinitePi (μ i))

ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ ∀ (i : ι), IsProbabilityMeasure (map (fun f j ↦ X i j (f j)) (infinitePi (μ i)))

case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ ∀ (i : ι), Measurable fun f j ↦ X i j (f j)
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
⊢ map (X i j) (μ i j) =
    map (fun f ↦ f j) (map (fun f ↦ f i) (infinitePi fun i ↦ map (fun f j ↦ X i j (f j)) (infinitePi (μ i))))

pp: case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
⊢ ∀ (i : ι), Measurable fun f j ↦ X i j (f j)

Tactic:
@infinitePi_map_eval ..,

Goal state after:
case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
⊢ map (X i j) (μ i j) = map (fun f ↦ f j) (map (fun f j ↦ X i j (f j)) (infinitePi (μ i)))

ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
⊢ ∀ (i : ι), IsProbabilityMeasure (map (fun f j ↦ X i j (f j)) (infinitePi (μ i)))

case refine_2
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
⊢ ∀ (i : ι), Measurable fun f j ↦ X i j (f j)
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: case pos
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : (κ a) (t ∩ t) = (κ a) t * (κ a) t
h0 : (κ a) t = 0
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ∞

Tactic:
exact Or.inl h0

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

Goal state before:
pp: α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1

Tactic:
by
  apply measure_eq_zero_or_one_of_indepSet_self' ?_
    ((indep_limsup_atBot_self h_le h_indep).indepSet_of_measurableSet ht_tail ht_tail)
  filter_upwards [h_indep.ae_isProbabilityMeasure] with a ha using by infer_instance

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✝⁵ : 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 ⋯)
x : Ω
⊢ x ∈ Set.univ ↔ x ∈ ⋃ i ∈ Set.range τ, {x | τ x = i}

Tactic:
simp only [Set.mem_univ, Set.mem_range, Set.iUnion_exists, Set.iUnion_iUnion_eq',
      Set.mem_iUnion, Set.mem_ofPred_eq, exists_apply_eq_apply']

Goal state after:
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst✝² : Nonempty Y
mY : MeasurableSpace Y
inst✝¹ : StandardBorelSpace Y
κ : Kernel X Y
inst✝ : IsMarkovKernel κ
g : Y → ↑I := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (κ.map g)
hg'κ : κ = (κ.map g).map hg.invFun
f' : X → ↑I → ↑I
hf' : Measurable (uncurry f')
hf'κ : ∀ (a : X), Measure.map (f' a) volume = (κ.map g) a
a : X
⊢ Measure.map ((fun a u ↦ hg.invFun (f' a u)) a) volume = κ a

Tactic:
hg'κ,

Goal state after:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst✝² : Nonempty Y
mY : MeasurableSpace Y
inst✝¹ : StandardBorelSpace Y
κ : Kernel X Y
inst✝ : IsMarkovKernel κ
g : Y → ↑I := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (κ.map g)
hg'κ : κ = (κ.map g).map hg.invFun
f' : X → ↑I → ↑I
hf' : Measurable (uncurry f')
hf'κ : ∀ (a : X), Measure.map (f' a) volume = (κ.map g) a
a : X
⊢ Measure.map ((fun a u ↦ hg.invFun (f' a u)) a) volume = ((κ.map g).map hg.invFun) a
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsKolmogorovProcess X P p q M
s t : T
⊢ StronglyMeasurable fun ω ↦ edist (X s ω) (X t ω)

Tactic:
by
  borelize (E × E)
  exact continuous_edist.stronglyMeasurable.comp_measurable (hX.measurablePair s t)

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 : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ω' : Ω'
⊢ (∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)) → ∀ (t : ℝ), mgf (-X) (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
hm

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ω' : Ω'
hm : ∀ (t : ℝ), mgf X (κ ω') 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
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : {ω | 0 < X ω} = ⋃ ε, {ω | ↑↑ε ≤ X ω}
ε : ℚ
ω' : Ω'
⊢ (∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ↑ε ≤ X ω} ≤ rexp (-t * ↑ε + ↑0 * t ^ 2 / 2)) →
    IsFiniteMeasure (κ ω') → 0 < ε → (κ ω') {ω | ↑ε ≤ X ω} = 0

Tactic:
hm

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : {ω | 0 < X ω} = ⋃ ε, {ω | ↑↑ε ≤ X ω}
ε : ℚ
ω' : Ω'
hm : ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ↑ε ≤ X ω} ≤ rexp (-t * ↑ε + ↑0 * t ^ 2 / 2)
⊢ IsFiniteMeasure (κ ω') → 0 < ε → (κ ω') {ω | ↑ε ≤ X ω} = 0
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case pos
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hY : HasSubgaussianMGF Y cY κ ν
hX0 : cX = 0
hX : HasSubgaussianMGF X 0 κ ν
⊢ HasSubgaussianMGF (fun ω ↦ X ω + Y ω) cY κ ν

Tactic:
refine hY.congr ?_

Goal state after:
case pos
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hY : HasSubgaussianMGF Y cY κ ν
hX0 : cX = 0
hX : HasSubgaussianMGF X 0 κ ν
⊢ Y =ᵐ[⇑κ ∘ₘ ν] fun ω ↦ X ω + Y ω
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
h : MemLp (fun ω ↦ rexp (t * X ω)) 2 (⇑κ ∘ₘ ν)
⊢ ⇑κ ∘ₘ ν = Measure.map Prod.fst (⇑(κ ⊗ₖ η) ∘ₘ ν)

Tactic:
Measure.map_comp _ _ measurable_fst,

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
h : MemLp (fun ω ↦ rexp (t * X ω)) 2 (⇑κ ∘ₘ ν)
⊢ ⇑κ ∘ₘ ν = ⇑((κ ⊗ₖ η).map Prod.fst) ∘ₘ ν
Module: Mathlib.Probability.StrongLaw

Goal state before:

Tactic:
∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc (j : ℝ) N} =
        ∑ j ∈ range K, ENNReal.ofReal (∫ _ in Set.Ioc (j : ℝ) N, (1 : ℝ) ∂ρ) := by simp_rw [B]
    _ = ENNReal.ofReal (∑ j ∈ range K, ∫ _ in Set.Ioc (j : ℝ) N, (1 : ℝ) ∂ρ) := by
      simp [ENNReal.ofReal_sum_of_nonneg]
    _ = ENNReal.ofReal (∑ j ∈ range K, ∫ _ in (j : ℝ)..N, (1 : ℝ) ∂ρ) := by
      congr 1
      refine sum_congr rfl fun j hj => ?_
      rw [intervalIntegral.integral_of_le (Nat.cast_le.2 ((mem_range.1 hj).le.trans hKN))]
    _ ≤ ENNReal.ofReal (𝔼[X] + 1) := ENNReal.ofReal_le_ofReal A

Goal state after: