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

Goal state before:
pp: case inl
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X ↑((aux n) a)) ≃ ((b : ↥(s n)) → X ↑b) :=
  fun n ↦ Equiv.piCongrLeft (fun i ↦ X ↑i) (aux n)
r_comp_f : ∀ (n : ℕ), (s n).restrict ∘ f = ⇑(g n) ∘ fun x i ↦ x ↑i
B : ℕ → Set ((i : ↑u) → X ↑i) := fun n ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X ↑((aux n) a)) := fun n ↦ ⇑(g n) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem : ∀ (n : ℕ), B n ∈ measurableCylinders fun i ↦ X ↑i
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : ⋂ n, B n = ∅
u_fin : Finite ↑u
x✝ : Fintype ↑u := Fintype.ofFinite ↑u
⊢ Tendsto (fun n ↦ (piContent fun i ↦ μ ↑i) (B n)) atTop (𝓝 0)

Tactic:
fun n ↦ piContent_eq_measure_pi (fun i : u ↦ μ i) (mB n)

Goal state after:
case inl
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X ↑((aux n) a)) ≃ ((b : ↥(s n)) → X ↑b) :=
  fun n ↦ Equiv.piCongrLeft (fun i ↦ X ↑i) (aux n)
r_comp_f : ∀ (n : ℕ), (s n).restrict ∘ f = ⇑(g n) ∘ fun x i ↦ x ↑i
B : ℕ → Set ((i : ↑u) → X ↑i) := fun n ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X ↑((aux n) a)) := fun n ↦ ⇑(g n) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem : ∀ (n : ℕ), B n ∈ measurableCylinders fun i ↦ X ↑i
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : ⋂ n, B n = ∅
u_fin : Finite ↑u
x✝ : Fintype ↑u := Fintype.ofFinite ↑u
⊢ Tendsto (fun n ↦ (Measure.pi fun i ↦ μ ↑i) (B n)) atTop (𝓝 0)
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
⊢ Measurable (lmarginalPartialTraj κ a b f)

Tactic:
unfold lmarginalPartialTraj

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
⊢ Measurable fun x₀ ↦
    ∫⁻ (z : (i : ↥(Iic b)) → X ↑i), f (updateFinset x₀ (Iic b) z) ∂(partialTraj κ a b) (frestrictLe a x₀)
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 : α
h : κ a ≪ η a
s : Set γ
hs : MeasurableSet s
⊢ ((η a).withDensity (∂κ a/∂η a)) s = (κ a) s

Tactic:
(κ a).withDensity_rnDeriv_eq _ h

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : κ a ≪ η a
s : Set γ
hs : MeasurableSet s
⊢ (κ a) s = (κ a) s
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : κ a ≪ η a
h_ae : κ.rnDeriv η a =ᵐ[η a] ∂κ a/∂η a
⊢ (η a).withDensity (∂κ a/∂η a) = κ a

Tactic:
(κ a).withDensity_rnDeriv_eq _ h

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : κ a ≪ η a
h_ae : κ.rnDeriv η a =ᵐ[η a] ∂κ a/∂η a
⊢ κ a = κ a
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.refine_1
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : DependsOn f ↑(Iic b)
mf : Measurable f
x y : (i : ℕ) → X i
hxy : ∀ i ∈ ↑(Iic a), x i = y i
hab : a ≤ b
i : ↥(Iic a)
⊢ frestrictLe a x i = frestrictLe a y i

pp: case inr.refine_2
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : DependsOn f ↑(Iic b)
mf : Measurable f
x y : (i : ℕ) → X i
hxy : ∀ i ∈ ↑(Iic a), x i = y i
hab : a ≤ b
z : (i : ↥(Ioc a b)) → X ↑i
⊢ f (Function.updateFinset x (Ioc a b) z) = f (Function.updateFinset y (Ioc a b) z)

Tactic:
· exact hxy i.1 i.2

Goal state after:
case inr.refine_2
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : DependsOn f ↑(Iic b)
mf : Measurable f
x y : (i : ℕ) → X i
hxy : ∀ i ∈ ↑(Iic a), x i = y i
hab : a ≤ b
z : (i : ↥(Ioc a b)) → X ↑i
⊢ f (Function.updateFinset x (Ioc a b) z) = f (Function.updateFinset y (Ioc a b) z)
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 Ω
⊢ ⇑(κ†μ ×ₖ Kernel.id) ∘ₘ ⇑κ ∘ₘ μ = μ ⊗ₘ κ

Tactic:
rw [← Kernel.swap_prod, ← Measure.comp_assoc, ← Measure.compProd_eq_comp_prod,
    compProd_posterior_eq_swap_comp, Measure.comp_assoc, Kernel.swap_swap, Measure.id_comp]

Goal state after:
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)
a : ℕ
⊢ Measurable (trajFun κ a)

Tactic:
apply Measure.measurable_of_measurable_coe
  refine MeasurableSpace.induction_on_inter
    (C := fun t ht ↦ Measurable (fun x₀ ↦ trajFun κ a x₀ t))
    (s := measurableCylinders X) generateFrom_measurableCylinders.symm
    isPiSystem_measurableCylinders (by simp) (fun t ht ↦ ?cylinder) (fun t mt ht ↦ ?compl)
    (fun f disf mf hf ↦ ?union)
  · obtain ⟨N, S, mS, t_eq⟩ : ∃ N S, MeasurableSet S ∧ t = cylinder (Iic N) S := by
      simpa [measurableCylinders_nat] using ht
    simp_rw [trajFun, AddContent.measure_eq _ _ generateFrom_measurableCylinders.symm _ ht,
      trajContent, projectiveFamilyContent_congr _ t t_eq mS, inducedFamily]
    refine Measure.measurable_measure.1 ?_ _ mS
    exact (Measure.measurable_map _ (measurable_restrict₂ _)).comp (measurable _)
  · have := isProbabilityMeasure_trajFun κ a
    simpa [measure_compl mt (measure_ne_top _ _)] using Measurable.const_sub ht _
  · simpa [measure_iUnion disf mf] using Measurable.tsum hf

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

Goal state before:

Tactic:
μ.map f ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ)
  _ = (Kernel.deterministic f hf ∘ₘ μ)
      ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) := by
    rw [Measure.deterministic_comp_eq_map]
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) ∘ₘ
      Kernel.copy 𝓧 ∘ₘ Kernel.deterministic f hf ∘ₘ μ := by
    rw [Measure.compProd_eq_parallelComp_comp_copy_comp,
      ← Kernel.parallelComp_id_left_comp_parallelComp, ← Measure.comp_assoc]
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.deterministic f hf ∥ₖ Kernel.id) ∘ₘ
      Kernel.copy Ω ∘ₘ μ := by rw [parallelProd_posterior_comp_copy_comp]
  _ = (Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
    rw [Measure.comp_assoc, Kernel.parallelComp_comp_parallelComp, Kernel.id_comp, Kernel.comp_id]
  _ = (Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) ∘ₘ μ := by -- `deterministic` is used here
    rw [Measure.comp_assoc, Kernel.parallelComp_self_comp_copy]
  _ = μ.map f ⊗ₘ Kernel.id := by
    rw [Measure.compProd_id_eq_copy_comp, ← Measure.comp_assoc,
      Measure.deterministic_comp_eq_map]

Goal state after:
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)
a : ℕ
⊢ traj κ a = (Kernel.id ×ₖ (traj κ a).map (Set.Ioi a).domRestrict).map ⇑(IicProdIoi a)

Tactic:
refine (eq_traj' _ (a + 1) _ fun b hb ↦ ?_).symm

Goal state after:
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
⊢ ((Kernel.id ×ₖ (traj κ a).map (Set.Ioi a).domRestrict).map ⇑(IicProdIoi a)).map (frestrictLe b) = partialTraj κ a b
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 : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧},
    MeasurableSet s →
      MeasurableSet t →
        ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod (⇑κ ∘ₘ μ) = (μ ⊗ₘ κ) (s ×ˢ t)
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) x.1 x.2 ∂μ.prod (⇑κ ∘ₘ μ) = (μ ⊗ₘ κ) (s ×ˢ t)

Tactic:
rw [setLIntegral_prod _ (by fun_prop), Measure.compProd_apply_prod hs ht]

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 : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
h1 :
  ∀ {s : Set Ω} {t : Set 𝓧},
    MeasurableSet s →
      MeasurableSet t →
        ∫⁻ (x : Ω × 𝓧) in s ×ˢ t, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x.2 x.1 ∂μ.prod (⇑κ ∘ₘ μ) = (μ ⊗ₘ κ) (s ×ˢ t)
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (x : Ω) in s, ∫⁻ (y : 𝓧) in t, κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) (x, y).1 (x, y).2 ∂⇑κ ∘ₘ μ ∂μ =
    ∫⁻ (a : Ω) in s, (κ a) t ∂μ
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓧' : Type u_3
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓧' : MeasurableSpace 𝓧'
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst✝¹ : IsSFiniteKernel P
π : Measure Θ
η : Kernel (Θ × 𝓧) 𝓧'
inst✝ : IsMarkovKernel η
⊢ P = Kernel.deterministic Prod.fst ⋯ ∘ₖ (P ⊗ₖ η)

Tactic:
rw [Kernel.deterministic_comp_eq_map, ← Kernel.fst_eq, Kernel.fst_compProd]

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

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
x✝ : x ∈ Ioc 0 1
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ x ^ (α - 1) * (1 - x) ^ (β - 1) = RCLike.re (↑x ^ ↑(α - 1) * ↑(1 - x) ^ ↑(β - 1))

Tactic:
← Complex.ofReal_cpow,

Goal state after:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
x✝ : x ∈ Ioc 0 1
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ x ^ (α - 1) * (1 - x) ^ (β - 1) = RCLike.re (↑(x ^ (α - 1)) * ↑(1 - x) ^ ↑(β - 1))

case hx
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
x✝ : x ∈ Ioc 0 1
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ 0 ≤ x
Module: Mathlib.Probability.Distributions.Beta

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
x✝ : x ∈ Ioc 0 1
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ x ^ (α - 1) * (1 - x) ^ (β - 1) = RCLike.re (↑(x ^ (α - 1)) * ↑(1 - x) ^ ↑(β - 1))

pp: case hx
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
x✝ : x ∈ Ioc 0 1
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ 0 ≤ x

Tactic:
← Complex.ofReal_cpow,

Goal state after:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
x✝ : x ∈ Ioc 0 1
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ x ^ (α - 1) * (1 - x) ^ (β - 1) = RCLike.re (↑(x ^ (α - 1)) * ↑((1 - x) ^ (β - 1)))

case hx
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
x✝ : x ∈ Ioc 0 1
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ 0 ≤ 1 - x

case hx
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
x✝ : x ∈ Ioc 0 1
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ 0 ≤ x
Module: Mathlib.Probability.Distributions.Beta

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

pp: case hf
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ 0 ≤ᵐ[volume.restrict (Ioo 0 1)] fun x ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)

pp: case hfm
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ AEStronglyMeasurable (fun x ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) (volume.restrict (Ioo 0 1))

Tactic:
· 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]

Goal state after:
case hf
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ 0 ≤ᵐ[volume.restrict (Ioo 0 1)] fun x ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)

case hfm
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ AEStronglyMeasurable (fun x ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) (volume.restrict (Ioo 0 1))
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: case hfm
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ paretoPDFReal t r =ᵐ[volume.restrict (Ici t)] fun x ↦ r * t ^ r * x ^ (-(r + 1))

Tactic:
refine (ae_restrict_iff' measurableSet_Ici).mpr <| ae_of_all _ fun x (hx : t ≤ x) ↦ ?_

Goal state after:
case hfm
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
x : ℝ
hx : t ≤ x
⊢ paretoPDFReal t r x = (fun x ↦ r * t ^ r * x ^ (-(r + 1))) x
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
⊢ (pure a).bindOnSupport f = f a ⋯

Tactic:
by
  refine PMF.ext fun b => ?_
  simp only [bindOnSupport_apply, pure_apply]
  classical
  refine _root_.trans (tsum_congr fun a' => ?_) (tsum_ite_eq a (fun _ ↦ _))
  by_cases h : a' = a <;> simp [h]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
mR : MeasurableSpace R
inst✝ : MeasurableAdd₂ R
r₁ r₂ : ℝ≥0
⊢ Measure.map ⇑(Nat.castAddMonoidHom R) Po(r₁) ∗ Measure.map ⇑(Nat.castAddMonoidHom R) Po(r₂) =
    Measure.map ⇑(Nat.castAddMonoidHom R) Po(r₁ + r₂)

Tactic:
← Measure.map_conv_addMonoidHom _ (by fun_prop),

Goal state after:
R : Type u_1
inst✝¹ : AddMonoidWithOne R
mR : MeasurableSpace R
inst✝ : MeasurableAdd₂ R
r₁ r₂ : ℝ≥0
⊢ Measure.map (⇑(Nat.castAddMonoidHom R)) (Po(r₁) ∗ Po(r₂)) = Measure.map ⇑(Nat.castAddMonoidHom R) Po(r₁ + r₂)
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 : Ω → 𝓧
inst✝¹ : SFinite P
Y : Ω → 𝓨 × 𝓩
κ : Kernel 𝓧 (𝓨 × 𝓩)
inst✝ : IsSFiniteKernel κ
h : HasCondDistrib Y X κ P
⊢ HasCondDistrib (fun ω ↦ (Y ω).1) X κ.fst P

Tactic:
rw [Kernel.fst_eq]
  exact h.comp_left measurable_fst

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

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : NormedAddCommGroup F
f : Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hm : m ≤ mΩ
hf : StronglyMeasurable f
hf_int : Integrable f μ
⊢ μ[f | m] =ᵐ[μ.trim hm] fun ω ↦ ∫ (y : Ω), f y ∂(condExpKernel μ m) ω

Tactic:
refine StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable hm ?_ ?_ ?_
  · exact stronglyMeasurable_condExp
  · exact hf.integral_condExpKernel
  · exact condExp_ae_eq_integral_condExpKernel hm hf_int

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

Goal state before:
pp: case refine_1
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ i ∈ s, (fun ω ↦ (((condExpKernel μ m') ω) (f i)).toReal) =ᵐ[μ] μ[(f i).indicator fun ω ↦ 1 | m']
h_eq :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ᵐ (ω : Ω) ∂μ, ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = μ[(f i).indicator fun ω ↦ 1 | m'] ω
h_inter_eq :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      (fun ω ↦ (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal) =ᵐ[μ] μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m']
s : Finset ι
f : ι → Set Ω
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (⋂ i ∈ s, f i) = ∏ i ∈ s, ((condExpKernel μ m') a) (f i)
hf : ∀ i ∈ s, f i ∈ π i
⊢ μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).indicator fun ω ↦ 1 | m']

Tactic:
have h' := ae_eq_of_ae_eq_trim h

Goal state after:
case refine_1
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ i ∈ s, (fun ω ↦ (((condExpKernel μ m') ω) (f i)).toReal) =ᵐ[μ] μ[(f i).indicator fun ω ↦ 1 | m']
h_eq :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ᵐ (ω : Ω) ∂μ, ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = μ[(f i).indicator fun ω ↦ 1 | m'] ω
h_inter_eq :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      (fun ω ↦ (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal) =ᵐ[μ] μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m']
s : Finset ι
f : ι → Set Ω
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (⋂ i ∈ s, f i) = ∏ i ∈ s, ((condExpKernel μ m') a) (f i)
hf : ∀ i ∈ s, f i ∈ π i
h' : (fun x ↦ ((condExpKernel μ m') x) (⋂ i ∈ s, f i)) =ᵐ[μ] fun x ↦ ∏ i ∈ s, ((condExpKernel μ m') x) (f i)
⊢ μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).indicator fun ω ↦ 1 | m']
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case refine_1
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᵐ[μ] μ[(s ∩ t).indicator fun ω ↦ 1 | m']
s t : Set Ω
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (s ∩ t) = ((condExpKernel μ m') a) s * ((condExpKernel μ m') a) t
hs : s ∈ s1
ht : t ∈ s2
⊢ μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']

Tactic:
have h' := ae_eq_of_ae_eq_trim h

Goal state after:
case refine_1
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᵐ[μ] μ[(s ∩ t).indicator fun ω ↦ 1 | m']
s t : Set Ω
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (s ∩ t) = ((condExpKernel μ m') a) s * ((condExpKernel μ m') a) t
hs : s ∈ s1
ht : t ∈ s2
h' : (fun x ↦ ((condExpKernel μ m') x) (s ∩ t)) =ᵐ[μ] fun x ↦ ((condExpKernel μ m') x) s * ((condExpKernel μ m') x) t
⊢ μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case refine_2
Ω : 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 ∈ s, sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(sets i).indicator fun ω ↦ 1 | m']

Tactic:
convert! h with i hi i hi

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