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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → β → E
s : Set α
a : α
ha : a ∈ s
⊢ ∫ (y : β), s.indicator (fun x ↦ f x y) a ∂κ a = s.indicator (fun x ↦ ∫ (y : β), f x y ∂κ x) a

Tactic:
simp [ha]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → β → E
s : Set α
a : α
ha : a ∉ s
⊢ ∫ (y : β), s.indicator (fun x ↦ f x y) a ∂κ a = s.indicator (fun x ↦ ∫ (y : β), f x y ∂κ x) a

Tactic:
simp [ha]

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ (∫⁻ (a : α) in t, ((condDistrib Y X μ) (X a)) s ∂μ).toReal = μ.real (Y ⁻¹' s ∩ t) • 1

Tactic:
smul_eq_mul,

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
a✝ : μ t < ∞
⊢ (∫⁻ (a : α) in t, ((condDistrib Y X μ) (X a)) s ∂μ).toReal = μ.real (Y ⁻¹' s ∩ t) * 1
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun i ↦ ∫ (a_1 : γ), κ.density κ.fst a a_1 (seq i) ∂κ.fst a) atTop (𝓝 ((κ.fst a).real univ • 1))

Tactic:
smul_eq_mul,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun i ↦ ∫ (a_1 : γ), κ.density κ.fst a a_1 (seq i) ∂κ.fst a) atTop (𝓝 ((κ.fst a).real univ * 1))
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
h : ∀ (a b : ℕ) (hab : a ≤ b), Measure.map (frestrictLe₂ hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ inducedFamily μ J = Measure.map (restrict₂ hJI) (inducedFamily μ I)

Tactic:
simp only [inducedFamily]

Goal state after:
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
h : ∀ (a b : ℕ) (hab : a ≤ b), Measure.map (frestrictLe₂ hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measure.map (restrict₂ ⋯) (μ (J.sup id)) = Measure.map (restrict₂ hJI) (Measure.map (restrict₂ ⋯) (μ (I.sup id)))
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)
inst✝ : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι := { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
this : s = cylinder univ (⇑(piCongrLeft X e) ⁻¹' s)
⊢ (piContent μ) s = (Measure.pi μ) s

Tactic:
nth_rw 1 [this]

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι := { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
this : s = cylinder univ (⇑(piCongrLeft X e) ⁻¹' s)
⊢ (piContent μ) (cylinder univ (⇑(piCongrLeft X e) ⁻¹' s)) = (Measure.pi μ) s
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod (⇑κ ∘ₘ μ) = (μ ⊗ₘ κ) (s ×ˢ t)

Tactic:
rw [setLIntegral_prod_symm _ (by fun_prop), ← swap_compProd_posterior, Measure.swap_comp,
      Measure.map_apply measurable_swap (hs.prod ht), Set.preimage_swap_prod,
      Measure.compProd_apply_prod ht hs]

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (y : 𝓧) in t, ∫⁻ (x : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) (x, y).2 (x, y).1 ∂μ ∂⇑κ ∘ₘ μ =
    ∫⁻ (a : 𝓧) in t, ((κ†μ) a) s ∂⇑κ ∘ₘ μ
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: case inr
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst✝² : IsMarkovKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsMarkovKernel κ
π : Measure Θ
inst✝ : IsProbabilityMeasure π
C : ℝ≥0
hℓC : ∀ (θ : Θ) (y : 𝓨), ℓ θ y ≤ ↑C
h✝ : Nonempty Θ
⊢ ↑C * κ.bound * P.bound * π Set.univ ≤ ↑C

Tactic:
· rcases isEmpty_or_nonempty 𝓧 <;> simp

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ (infinitePi fun p ↦ μ p.1 p.2) =
    map (⇑(MeasurableEquiv.curry ι κ X).symm) (infinitePi fun i ↦ infinitePi fun j ↦ μ i j)

Tactic:
infinitePi_map_curry_symm

Goal state after:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ (infinitePi fun p ↦ μ p.1 p.2) = infinitePi fun p ↦ μ p.1 p.2
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
x : 𝓧
h✝ : ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x
h_ac' : (κ†μ) x ≪ μ
s : Set Ω
hs : MeasurableSet s
ω : Ω
h : (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x
h_eq : (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = (∂(κ†μ) x/∂(Kernel.const 𝓧 μ) x) ω
hωs : ω ∈ s
⊢ (∂(κ†μ) x/∂μ) ω = (∂(κ†μ) x/∂(Kernel.const 𝓧 μ) x) ω

Tactic:
Kernel.const_apply

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
x : 𝓧
h✝ : ∀ᵐ (ω : Ω) ∂μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x
h_ac' : (κ†μ) x ≪ μ
s : Set Ω
hs : MeasurableSet s
ω : Ω
h : (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x
h_eq : (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = (∂(κ†μ) x/∂(Kernel.const 𝓧 μ) x) ω
hωs : ω ∈ s
⊢ (∂(κ†μ) x/∂μ) ω = (∂(κ†μ) x/∂μ) ω
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
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
i_f :
  (∀ᵐ (y : (i : ↥(Iic b)) → X ↑i) ∂(partialTraj κ a b) x₀, Integrable f ((traj κ b) y)) ∧
    Integrable (fun y ↦ ∫ (z : (n : ℕ) → X n), ‖f z‖ ∂(traj κ b) y) ((partialTraj κ a b) x₀)
⊢ ∀ᵐ (x : (i : ℕ) → X i) ∂(traj κ a) x₀, Integrable f ((traj κ b) (frestrictLe b x))

pp: case hf
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
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
i_f : Integrable f ((traj κ b ∘ₖ partialTraj κ a b) x₀)
⊢ AEStronglyMeasurable f ((traj κ b ∘ₖ partialTraj κ a b) x₀)

Tactic:
· apply ae_of_ae_map (p := fun x ↦ Integrable f (traj κ b x))
    · fun_prop
    · convert! i_f.1
      rw [← traj_map_frestrictLe, Kernel.map_apply _ (measurable_frestrictLe _)]

Goal state after:
case hf
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
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
i_f : Integrable f ((traj κ b ∘ₖ partialTraj κ a b) x₀)
⊢ AEStronglyMeasurable f ((traj κ b ∘ₖ partialTraj κ a b) x₀)
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
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
i_f : Integrable f ((traj κ a) x₀)
⊢ ∀ᵐ (x : (i : ℕ) → X i) ∂(traj κ a) x₀, Integrable f ((traj κ b) (frestrictLe b x))

Tactic:
by
  rw [← traj_comp_partialTraj hab, integrable_comp_iff] at i_f
  · apply ae_of_ae_map (p := fun x ↦ Integrable f (traj κ b x))
    · fun_prop
    · convert! i_f.1
      rw [← traj_map_frestrictLe, Kernel.map_apply _ (measurable_frestrictLe _)]
  · exact i_f.aestronglyMeasurable

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

Goal state before:
pp: x₀ : ℝ
γ : ℝ≥0
⊢ Measurable (cauchyPDFReal x₀ γ)

Tactic:
unfold cauchyPDFReal

Goal state after:
x₀ : ℝ
γ : ℝ≥0
⊢ Measurable fun x ↦ π⁻¹ * ↑γ * ((x - x₀) ^ 2 + ↑γ ^ 2)⁻¹
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ EqOn (fun x ↦ ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0))
    (fun x ↦ ENNReal.ofReal (r * rexp (-(r * x)))) (Icc 0 x)

Tactic:
intro a ha; simp [ha.1]

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

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) =
    (if 0 ≤ x then 1 else -1) • ∫ (x : ℝ) in uIoc 0 x, r * rexp (-(r * x)) ∂volume

Tactic:
smul_eq_mul,

Goal state after:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫ (a : ℝ) in uIoc 0 x, r * rexp (-(r * a)) =
    (if 0 ≤ x then 1 else -1) * ∫ (x : ℝ) in uIoc 0 x, r * rexp (-(r * x)) ∂volume
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))
⊢ Continuous fun a ↦ rexp (-(r * a))

Tactic:
simp only [← neg_mul]

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))
⊢ Continuous fun a ↦ rexp (-r * a)
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))
⊢ ContinuousOn (fun a ↦ -1 * rexp (-(r * a))) (Icc 0 x)

Tactic:
have : Continuous (fun a ↦ rexp (-(r * a))) := by
          simp only [← neg_mul]; exact (continuous_const_mul (-r)).rexp
        exact Continuous.continuousOn (Continuous.comp' (continuous_const_mul (-1)) this)

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

Goal state before:
pp: case pos
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : t ≤ x
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))

pp: case neg
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : ¬t ≤ x
⊢ 0 ≤ 0

Tactic:
· cases le_iff_eq_or_lt.1 ht with
    | inl ht0 =>
      rw [← ht0] at h
      positivity
    | inr htp =>
      positivity [lt_of_lt_of_le htp h]

Goal state after:
case neg
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : ¬t ≤ x
⊢ 0 ≤ 0
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ℝ
n : ℕ
hp_pos : 0 < p
hp_lt_one : p < 1
⊢ 0 < geometricPMFReal p n

Tactic:
rw [geometricPMFReal]

Goal state after:
p : ℝ
n : ℕ
hp_pos : 0 < p
hp_lt_one : p < 1
⊢ 0 < (1 - p) ^ n * p
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ℝ
n : ℕ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ 0 ≤ geometricPMFReal p n

Tactic:
rw [geometricPMFReal]

Goal state after:
p : ℝ
n : ℕ
hp_pos : 0 < p
hp_le_one : p ≤ 1
⊢ 0 ≤ (1 - p) ^ n * p
Module: Mathlib.Probability.Distributions.Exponential

Goal state before:
pp: r : ℝ
hr : 0 < r
x : ℝ
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (if 0 ≤ x then 1 - rexp (-(r * x)) else 0)

Tactic:
split_ifs with h
  case neg =>
    simp only [exponentialPDF_eq]
    rw [setLIntegral_congr_fun measurableSet_Iic, lintegral_zero, ENNReal.ofReal_zero]
    exact fun a (_ : a ≤ _) ↦ by rw [if_neg (by linarith), ENNReal.ofReal_eq_zero]
  case pos =>
    rw [lintegral_Iic_eq_lintegral_Iio_add_Icc _ h, lintegral_exponentialPDF_of_nonpos (le_refl 0),
      zero_add]
    simp only [exponentialPDF_eq]
    rw [setLIntegral_congr_fun measurableSet_Icc (g := fun x ↦ ENNReal.ofReal (r * rexp (-(r * x))))
      (by intro a ha; simp [ha.1])]
    rw [← ENNReal.toReal_eq_toReal_iff' _ ENNReal.ofReal_ne_top,
        ← integral_eq_lintegral_of_nonneg_ae (Eventually.of_forall fun _ ↦ le_of_lt
        (mul_pos hr (exp_pos _)))]
    · have : ∫ a in uIoc 0 x, r * rexp (-(r * a)) = ∫ a in 0..x, r * rexp (-(r * a)) := by
        rw [intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_eq_mul, if_pos h, one_mul]
      rw [integral_Icc_eq_integral_Ioc, ← uIoc_of_le h, this]
      rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h
        (f := fun a ↦ -1 * rexp (-(r * a))) _ _]
      · rw [ENNReal.toReal_ofReal_eq_iff.2
          (sub_nonneg.2 (Real.exp_le_one_iff.2 <| by nlinarith))]
        norm_num; ring
      · simp only [intervalIntegrable_iff, uIoc_of_le h]
        exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
      · have : Continuous (fun a ↦ rexp (-(r * a))) := by
          simp only [← neg_mul]; exact (continuous_const_mul (-r)).rexp
        exact Continuous.continuousOn (Continuous.comp' (continuous_const_mul (-1)) this)
      · simp only [neg_mul, one_mul]
        exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp
    · refine Integrable.aestronglyMeasurable (Integrable.const_mul ?_ _)
      rw [← IntegrableOn, integrableOn_Icc_iff_integrableOn_Ioc]
      exact exp_neg_integrableOn_Ioc hr
    · refine ne_of_lt (IntegrableOn.setLIntegral_lt_top ?_)
      rw [integrableOn_Icc_iff_integrableOn_Ioc]
      exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _

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

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
b : Bool
⊢ (bernoulli p h) b = ↑(bif b then p else 1 - p)

Tactic:
by
  simp only [bernoulli, ofFintype_apply]
  exact Eq.symm (Bool.apply_cond ofNNReal)

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

Goal state before:
pp: E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ∞
hu : 0 = (μ s)⁻¹ • μ.restrict s
h : ¬AEMeasurable X ℙ
⊢ (μ s)⁻¹ • μ s = 1

Tactic:
smul_eq_mul,

Goal state after:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ∞
hu : 0 = (μ s)⁻¹ • μ.restrict s
h : ¬AEMeasurable X ℙ
⊢ (μ s)⁻¹ * μ s = 1
Module: Mathlib.Probability.HasLawExists

Goal state before:
pp: case h
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ map (fun ω i ↦ Function.eval i ω) (infinitePi μ) = infinitePi fun i ↦ map (Function.eval i) (infinitePi μ)

Tactic:
map_id'

Goal state after:
case h
ι : Type v
𝓧 : ι → Type u
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
μ : (i : ι) → Measure (𝓧 i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ infinitePi μ = infinitePi fun i ↦ map (Function.eval i) (infinitePi μ)
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ∞
hu : IsUniform X s ℙ μ
this : X ⁻¹' Set.univ = Set.univ
⊢ ℙ Set.univ = 1

Tactic:
← this,

Goal state after:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ∞
hu : IsUniform X s ℙ μ
this : X ⁻¹' Set.univ = Set.univ
⊢ ℙ (X ⁻¹' Set.univ) = 1
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 (fun ω i ↦ s.restrict X i ω) P = Measure.pi fun i ↦ map (s.restrict X i) P

Tactic:
← this,

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 ω
⊢ map (s.restrict ∘ fun ω i ↦ X i ω) P = Measure.pi fun i ↦ map (s.restrict X i) P
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ s
⊢ (uniformOfFinset s hs) a = (↑(#s))⁻¹

Tactic:
simp [ha]

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

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
a : α
ha : a ∉ s
⊢ (uniformOfFinset s hs) a = 0

Tactic:
simp [ha]

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

Goal state before:
pp: case refine_1
α : 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 κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
⊢ ∃ a, ∀ b ≤ a, b ∉ t

Tactic:
obtain ⟨b, hb⟩ : ∃ b, b < a := exists_lt a

Goal state after:
case refine_1
α : 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 κ μα
ns : ι → Set ι := Set.Ici
hnsp : ∀ (i : ι), BddBelow (ns i)
t : Set ι
a : ι
ha : a ∈ {x | ∀ ⦃a : ι⦄, a ∈ t → x ≤ a}
b : ι
hb : b < a
⊢ ∃ a, ∀ b ≤ a, b ∉ t
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst✝⁹ : (t : T) → TopologicalSpace (F t)
inst✝⁸ : (t : T) → MeasurableSpace (F t)
inst✝⁷ : ∀ (t : T), BorelSpace (F t)
inst✝⁶ : ∀ (t : T), HasOuterApproxClosed (F t)
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst✝¹ : IsFiniteMeasure P
inst✝ : Finite T
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : ((t : T) → F t) →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ f (Z ω) * g fun x ↦ Y x ω) x ∂P =
      (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (fun ω ↦ g fun x ↦ Y x ω) x ∂P
this : Fintype T
f : G →ᵇ ℝ
g : (t : T) → F t →ᵇ ℝ
⊢ ∫ (x : Ω), (⇑f ∘ Z * ∏ t, ⇑(g t) ∘ Y t) x ∂P = (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P

Tactic:
convert! h f (∏ t, (g t).compContinuous ⟨Function.eval t, by fun_prop⟩)

Goal state after:
case e'_2
Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst✝⁹ : (t : T) → TopologicalSpace (F t)
inst✝⁸ : (t : T) → MeasurableSpace (F t)
inst✝⁷ : ∀ (t : T), BorelSpace (F t)
inst✝⁶ : ∀ (t : T), HasOuterApproxClosed (F t)
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst✝¹ : IsFiniteMeasure P
inst✝ : Finite T
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : ((t : T) → F t) →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ f (Z ω) * g fun x ↦ Y x ω) x ∂P =
      (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (fun ω ↦ g fun x ↦ Y x ω) x ∂P
this : Fintype T
f : G →ᵇ ℝ
g : (t : T) → F t →ᵇ ℝ
x✝¹ x✝ : Ω
⊢ (⇑f ∘ Z * ∏ t, ⇑(g t) ∘ Y t) x✝ =
    f (Z x✝) * (∏ t, (g t).compContinuous { toFun := Function.eval t, continuous_toFun := ⋯ }) fun x ↦ Y x x✝

case e'_3
Ω : Type u_1
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
F : T → Type u_5
G : Type u_6
inst✝⁹ : (t : T) → TopologicalSpace (F t)
inst✝⁸ : (t : T) → MeasurableSpace (F t)
inst✝⁷ : ∀ (t : T), BorelSpace (F t)
inst✝⁶ : ∀ (t : T), HasOuterApproxClosed (F t)
inst✝⁵ : TopologicalSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : HasOuterApproxClosed G
Y : (t : T) → Ω → F t
Z : Ω → G
inst✝¹ : IsFiniteMeasure P
inst✝ : Finite T
mZ : AEMeasurable Z P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : G →ᵇ ℝ) (g : ((t : T) → F t) →ᵇ ℝ),
    ∫ (x : Ω), (fun ω ↦ f (Z ω) * g fun x ↦ Y x ω) x ∂P =
      (∫ (x : Ω), (⇑f ∘ Z) x ∂P) * ∫ (x : Ω), (fun ω ↦ g fun x ↦ Y x ω) x ∂P
this : Fintype T
f : G →ᵇ ℝ
g : (t : T) → F t →ᵇ ℝ
x✝¹ x✝ : Ω
⊢ (∏ t, ⇑(g t) ∘ Y t) x✝ =
    (∏ t, (g t).compContinuous { toFun := Function.eval t, continuous_toFun := ⋯ }) fun x ↦ Y x x✝
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X : SFinKer
⊢ Kernel.discard X.carrier ∥ₖ Kernel.id ∘ₖ Kernel.copy X.carrier = Kernel.id.map fun x ↦ (PUnit.unit, x)

Tactic:
simp only [Kernel.discard, Kernel.copy, Kernel.id]

Goal state after:
X : SFinKer
⊢ Kernel.deterministic (fun x ↦ PUnit.unit) ⋯ ∥ₖ Kernel.deterministic 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.id ∥ₖ Kernel.discard X.carrier ∘ₖ Kernel.copy X.carrier = Kernel.id.map fun x ↦ (x, PUnit.unit)

Tactic:
simp only [Kernel.discard, Kernel.copy, Kernel.id]

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