mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ charFunDual (Measure.map Y P) L =
    cexp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2) *
      cexp (↑(∫ (x : Ω), (⇑L ∘ (Y - X)) x ∂P) * I - ↑Var[⇑L ∘ (Y - X); P] / 2)

pp: case h.mX
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ AEMeasurable X P

pp: case h.mY
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ AEMeasurable (Y - X) P

Tactic:
← exp_add,

Goal state after:
case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ charFunDual (Measure.map Y P) L =
    cexp
      (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2 +
        (↑(∫ (x : Ω), (⇑L ∘ (Y - X)) x ∂P) * I - ↑Var[⇑L ∘ (Y - X); P] / 2))

case h.mX
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ AEMeasurable X P

case h.mY
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ AEMeasurable (Y - X) P
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
⊢ ∀ᵐ (t : β) ∂κ'.fst a, (a, t) ∈ {p | (η p) (range e)ᶜ = 0}

Tactic:
have h_compProd : κ' a (univ ×ˢ range e)ᶜ = 0 := by
      unfold κ'
      rw [map_apply' _ (by fun_prop)]
      swap; · exact (MeasurableSet.univ.prod he.measurableSet_range).compl
      suffices Prod.map id e ⁻¹' (univ ×ˢ range e)ᶜ = ∅ by rw [this]; simp
      ext x
      simp

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd : (κ' a) (univ ×ˢ range e)ᶜ = 0
⊢ ∀ᵐ (t : β) ∂κ'.fst a, (a, t) ∈ {p | (η p) (range e)ᶜ = 0}
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
s : Set α
hs : MeasurableSet s
⊢ (Measure.map (Prod.map id f) ρ).fst s = ρ.fst s

Tactic:
Measure.fst_apply,

Goal state after:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
s : Set α
hs : MeasurableSet s
⊢ (Measure.map (Prod.map id f) ρ) (Prod.fst ⁻¹' s) = ρ.fst s

α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
s : Set α
hs : MeasurableSet s
⊢ (Measure.map (Prod.map id f) ρ) (Prod.fst ⁻¹' s) = ρ.fst s

pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
Measure.fst_apply,

Goal state after:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
s : Set α
hs : MeasurableSet s
⊢ (Measure.map (Prod.map id f) ρ) (Prod.fst ⁻¹' s) = ρ (Prod.fst ⁻¹' s)

α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s

α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ κ.densityProcess ν n a x s'

Tactic:
exact isBoundedUnder_of ⟨1, fun n ↦ densityProcess_le_one hκν _ _ _ _⟩

Goal state after:
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 α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
x : γ
s : Set β
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun n ↦ κ.densityProcess ν n a x s

Tactic:
exact isBoundedUnder_of ⟨1, fun n ↦ densityProcess_le_one hκν _ _ _ _⟩

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
⊢ ⇑(condDistrib Y X μ) =ᵐ[Measure.map X μ] ⇑κ

Tactic:
suffices condDistrib (hY.mk Y) (hX.mk X) μ =ᵐ[μ.map (hX.mk X)] κ by
    rwa [Measure.map_congr hX.ae_eq_mk, condDistrib_congr hY.ae_eq_mk hX.ae_eq_mk]

Goal state after:
case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
⊢ ⇑(condDistrib (AEMeasurable.mk Y hY) (AEMeasurable.mk X hX) μ) =ᵐ[Measure.map (AEMeasurable.mk X hX) μ] ⇑κ
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ μ[X ^ 2 | m] - 2 * μ[X | m] ^ 2 + μ[X | m] ^ 2 = μ[X ^ 2 | m] - μ[X | m] ^ 2

Tactic:
ring

Goal state after:
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), (X ^ 2) x ∂μ - ∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ +
      (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2) =
    ∫ (x : Ω), (X ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2

Tactic:
ring

Goal state after:
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
ω : Ω
hω : μ[-X | m] ω = (-μ[X | m]) ω
⊢ (-X ω + μ[X | m] ω) ^ 2 = (X ω - μ[X | m] ω) ^ 2

Tactic:
ring

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
⊢ map (_root_.IicProdIoc a b) ((Measure.pi fun i ↦ μ ↑i).prod (Measure.pi fun i ↦ μ ↑i)) = Measure.pi fun i ↦ μ ↑i

Tactic:
· rw [IicProdIoc_le hba, ← Measure.map_map, ← Measure.fst, Measure.fst_prod]
    · exact isProjectiveMeasureFamily_pi μ (Iic a) (Iic b) (Iic_subset_Iic.2 hba) |>.symm
    all_goals fun_prop

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

Goal state before:

Tactic:
fs n a b ≤ min (f a b) (n + 1) := tsub_le_self
    _ ≤ n + 1 := min_le_right _ _
    _ = ↑(n + 1) := by norm_cast

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
A : Set ((n : ℕ) → X n)
hA : A ∈ measurableCylinders X
⊢ (piContent μ) A = (infinitePiNat μ) A

Tactic:
obtain ⟨s, S, mS, rfl⟩ : ∃ s S, MeasurableSet S ∧ A = cylinder s S := by
    simpa [mem_measurableCylinders] using hA

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
s : Finset ℕ
S : Set ((i : ↥s) → X ↑i)
mS : MeasurableSet S
hA : cylinder s S ∈ measurableCylinders X
⊢ (piContent μ) (cylinder s S) = (infinitePiNat μ) (cylinder s S)
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable fun b ↦
    ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b) * κ.rnDeriv η a b

Tactic:
exact measurable_singularPart_fun_right κ η a

Goal state after:
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 ≤ κ a

Tactic:
by
  refine Measure.le_intro (fun s hs _ ↦ ?_)
  rw [Kernel.withDensity_apply']
  · exact setLIntegral_rnDeriv_le hs
  · exact κ.measurable_rnDeriv _

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this : ((κ ∥ₖ κ ∘ₖ copy α) a) (s ×ˢ s) = ((copy β ∘ₖ κ) a) (s ×ˢ s)
⊢ (κ a) s = 0 ∨ (κ a) s = 1

Tactic:
rw [parallelComp_comp_copy, prod_apply_prod, copy_comp_apply_prod, inter_self] at this

Goal state after:
case mp
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this : (κ a) s * (κ a) s = (κ a) s
⊢ (κ a) s = 0 ∨ (κ a) s = 1

case mp.hs
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this : (κ a) s * (κ a) s = ((copy β ∘ₖ κ) a) (s ×ˢ s)
⊢ MeasurableSet s

case mp.ht
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this : (κ a) s * (κ a) s = ((copy β ∘ₖ κ) a) (s ×ˢ s)
⊢ MeasurableSet s
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case cylinder
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
ht : t ∈ measurableCylinders X
⊢ Measurable fun x₀ ↦ (trajFun κ a x₀) t

Tactic:
obtain ⟨N, S, mS, t_eq⟩ : ∃ N S, MeasurableSet S ∧ t = cylinder (Iic N) S := by
      simpa [measurableCylinders_nat] using ht

Goal state after:
case cylinder
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
ht : t ∈ measurableCylinders X
N : ℕ
S : Set ((i : ↥(Iic N)) → X ↑i)
mS : MeasurableSet S
t_eq : t = cylinder (Iic N) S
⊢ Measurable fun x₀ ↦ (trajFun κ a x₀) t
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ (⇑(Kernel.deterministic f hf) ∘ₘ μ) ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) =
    ⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ
      ⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) ∘ₘ ⇑(Kernel.copy 𝓧) ∘ₘ ⇑(Kernel.deterministic f hf) ∘ₘ μ

Tactic:
Measure.compProd_eq_parallelComp_comp_copy_comp,

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ ⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ)) ∘ₘ
      ⇑(Kernel.copy 𝓧) ∘ₘ ⇑(Kernel.deterministic f hf) ∘ₘ μ =
    ⇑(Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ
      ⇑(Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) ∘ₘ ⇑(Kernel.copy 𝓧) ∘ₘ ⇑(Kernel.deterministic f hf) ∘ₘ μ
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)
α : Type u_3
e : α ≃ ι
⊢ map (⇑(piCongrLeft X e)) (infinitePi fun i ↦ μ (e i)) = infinitePi μ

Tactic:
by
  refine eq_infinitePi μ fun s t ht ↦ ?_
  conv_lhs => enter [2, 1]; rw [← e.image_preimage s, ← coe_preimage _ e.injective.injOn]
  rw [map_apply, coe_piCongrLeft, Equiv.piCongrLeft_preimage_pi, infinitePi_pi,
    prod_equiv e]
  · simp
  · simp
  · simp_all
  · fun_prop
  · exact .pi ((countable_toSet _).image e) (by simp_all)

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

Goal state before:
pp: n k : ℕ
p : ↑I
⊢ Bin(n, p) {k} = ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k))

Tactic:
← ENNReal.ofReal_toReal (a := Bin(n, p) _) (by simp),

Goal state after:
n k : ℕ
p : ↑I
⊢ ENNReal.ofReal (Bin(n, p) {k}).toReal = ENNReal.ofReal (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k))
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))
⊢ -rexp (-(r * x)) + 1 = 1 - rexp (-(r * x))

Tactic:
ring

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

Goal state before:
pp: case e_f
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 c : ℕ
hab : a ≤ b
hbc : b ≤ c
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_cf : Integrable ((traj κ a) x₀)[f | ↑piLE c] ((traj κ a) x₀)
mcf : StronglyMeasurable ((traj κ a) x₀)[f | ↑piLE c]
x : (n : ℕ) → X n
h1 : ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x = ((traj κ a) x₀)[f | ↑piLE b] x
h2 :
  ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x =
    ∫ (y : (n : ℕ) → X n), ((traj κ a) x₀)[f | ↑piLE c] y ∂(traj κ b) (frestrictLe b x)
y : (n : ℕ) → X n
⊢ ∀ i ∈ Set.Iic c, y i = updateFinset x (Iic c) (frestrictLe c y) i

Tactic:
simp only [Set.mem_Iic, updateFinset, mem_Iic, frestrictLe_apply, dite_eq_ite]

Goal state after:
case e_f
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 c : ℕ
hab : a ≤ b
hbc : b ≤ c
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_cf : Integrable ((traj κ a) x₀)[f | ↑piLE c] ((traj κ a) x₀)
mcf : StronglyMeasurable ((traj κ a) x₀)[f | ↑piLE c]
x : (n : ℕ) → X n
h1 : ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x = ((traj κ a) x₀)[f | ↑piLE b] x
h2 :
  ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x =
    ∫ (y : (n : ℕ) → X n), ((traj κ a) x₀)[f | ↑piLE c] y ∂(traj κ b) (frestrictLe b x)
y : (n : ℕ) → X n
⊢ ∀ i ≤ c, y i = if i ≤ c then y i else x i
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r₁ r₂ : ℝ≥0
t : ℝ
⊢ ↑↑r₁ * (Complex.exp (↑t * Complex.I) - 1) + ↑↑r₂ * (Complex.exp (↑t * Complex.I) - 1) =
    (↑↑r₁ + ↑↑r₂) * (Complex.exp (↑t * Complex.I) - 1)

Tactic:
ring

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
b : β
a : α
h1 : p a = 0
h2 : q b = 0
⊢ p a * 0 = q b * 0

Tactic:
ring

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
b : β
a : α
h1 : p a = 0
h2 : ¬q b = 0
⊢ p a * 0 = q b * (p a * 0)

Tactic:
ring

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
b : β
a : α
h1 : ¬p a = 0
h2 : q b = 0
⊢ p a * (q b * 0) = q b * 0

Tactic:
ring

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
b : β
a : α
h1 : ¬p a = 0
h2 : ¬q b = 0
⊢ p a * (q b * (f a h1 b h2) c) = q b * (p a * (f a h1 b ⋯) c)

Tactic:
ring

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

Goal state before:
pp: case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ∞
this : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := (volume s)⁻¹ • 1
⊢ ∫⁻ (x : ℝ), ‖x‖ₑ * s.indicator ind x ≠ ∞

Tactic:
have : ∀ x, ‖x‖ₑ * s.indicator ind x = s.indicator (fun x => ‖x‖ₑ * ind x) x := fun x =>
    (s.indicator_mul_right (fun x => ↑‖x‖₊) ind).symm

Goal state after:
case neg.right
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
hcs : IsCompact s
huX : IsUniform X s ℙ volume
hnt : ¬volume s = 0 ∧ ¬volume s = ∞
this✝ : IsProbabilityMeasure ℙ
ind : ℝ → ℝ≥0∞ := (volume s)⁻¹ • 1
this : ∀ (x : ℝ), ‖x‖ₑ * s.indicator ind x = s.indicator (fun x ↦ ‖x‖ₑ * ind x) x
⊢ ∫⁻ (x : ℝ), ‖x‖ₑ * s.indicator ind x ≠ ∞
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: case refine_1
Ω : 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 μ
⊢ StronglyMeasurable μ[f | m]

Tactic:
exact stronglyMeasurable_condExp

Goal state after: