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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto (fun m ↦ ∫ (c : α), (preCDF ρ (s m) c).toReal ∂(Kernel.const Unit ρ.fst) a) atTop
    (𝓝 (((Kernel.const Unit ρ.fst) a).real univ))

Tactic:
Kernel.const_apply,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto (fun m ↦ ∫ (c : α), (preCDF ρ (s m) c).toReal ∂ρ.fst) atTop (𝓝 (ρ.fst.real univ))
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : Set α
hs : MeasurableSet s
q : ℚ
⊢ ∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂(Kernel.const Unit ρ.fst) a =
    ((Kernel.const Unit ρ) a).real (s ×ˢ Iic ↑q)

Tactic:
Kernel.const_apply,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : Set α
hs : MeasurableSet s
q : ℚ
⊢ ∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂ρ.fst = ((Kernel.const Unit ρ) a).real (s ×ˢ Iic ↑q)
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : Set α
hs : MeasurableSet s
q : ℚ
⊢ ∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂ρ.fst = ((Kernel.const Unit ρ) a).real (s ×ˢ Iic ↑q)

Tactic:
Kernel.const_apply,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : Set α
hs : MeasurableSet s
q : ℚ
⊢ ∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂ρ.fst = ρ.real (s ×ˢ Iic ↑q)
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
t : ℝ
⊢ Tendsto (fun n ↦ charFun (Measure.map X P) ((√↑n)⁻¹ * t) ^ n) atTop (𝓝 (cexp (-↑t ^ 2 / 2)))

Tactic:
by
  apply tendsto_pow_exp_of_isLittleO_sub_add_div
  suffices (fun (n : ℕ) ↦ charFun (Measure.map X P) ((√n)⁻¹ * t) -
      (1 + (-(((√n)⁻¹ * t) ^ 2 / 2) : ℂ))) =o[atTop] fun n ↦ ((√n)⁻¹ * t) ^ 2 by
    have aux : (fun (n : ℕ) ↦ ‖(1 / n : ℂ)‖) = fun (n : ℕ) ↦ ‖(1 / n : ℝ)‖ := by simp
    rw [← Asymptotics.isLittleO_norm_right, aux, Asymptotics.isLittleO_norm_right]
    refine .of_const_mul_right (c := t ^ 2) ?_
    convert! this using 4 with n <;> norm_cast <;> simp [field]
  have : Tendsto (fun (n : ℕ) ↦ (√n)⁻¹ * t) atTop (𝓝 0) := by
    rw [← zero_mul t]
    exact .mul_const t (tendsto_inv_atTop_zero.comp <| Real.tendsto_sqrt_atTop.comp <|
      tendsto_natCast_atTop_atTop)
  convert! (taylor_charFun_two hX h0 h1).comp_tendsto this using 2
  simp
  ring

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel β γ
inst✝ : IsSFiniteKernel η
hμ : SFinite μ
⊢ ⇑(Kernel.id ∥ₖ η) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)

Tactic:
Measure.compProd_eq_comp_prod,

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel β γ
inst✝ : IsSFiniteKernel η
hμ : SFinite μ
⊢ ⇑(Kernel.id ∥ₖ η) ∘ₘ ⇑(Kernel.id ×ₖ κ) ∘ₘ μ = μ ⊗ₘ (η ∘ₖ κ)
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel β γ
inst✝ : IsSFiniteKernel η
hμ : SFinite μ
⊢ ⇑(Kernel.id ∥ₖ η) ∘ₘ ⇑(Kernel.id ×ₖ κ) ∘ₘ μ = μ ⊗ₘ (η ∘ₖ κ)

Tactic:
Measure.compProd_eq_comp_prod,

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel β γ
inst✝ : IsSFiniteKernel η
hμ : SFinite μ
⊢ ⇑(Kernel.id ∥ₖ η) ∘ₘ ⇑(Kernel.id ×ₖ κ) ∘ₘ μ = ⇑(Kernel.id ×ₖ (η ∘ₖ κ)) ∘ₘ μ
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = ((κ.fst ⊗ₖ κCond).fst a) s

Tactic:
rw [fst_compProd_apply _ _ _ hs]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : 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
⊢ HasGaussianLaw (Y - X) P

Tactic:
rw [hasGaussianLaw_iff_charFunDual_map_eq (by fun_prop)]

Goal state after:
Ω : 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 - X) P) L = cexp (↑(∫ (x : Ω), (⇑L ∘ (Y - X)) x ∂P) * I - ↑Var[⇑L ∘ (Y - X); P] / 2)
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω), f x ∂κ a

Tactic:
conv_rhs => rw [← κ.disintegrate κ.condKernel]
  rw [Kernel.lintegral_compProd _ _ _ hf]

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
⊢ ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)

Tactic:
suffices ∫ x in A, density κ ν a x s ∂(ν a) = ∫ x in A, densityProcess κ ν n a x s ∂(ν a) by
    exact this ▸ setIntegral_densityProcess hκν _ _ hs hA

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
⊢ ∫ (x : γ) in A, κ.density ν a x s ∂ν a = ∫ (x : γ) in A, κ.densityProcess ν n a x s ∂ν a
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
⊢ IsMarkovKernel (if hα : Countable α then condKernelCountable (fun a ↦ (κ a).condKernel) ⋯ else κ.condKernelBorel)

Tactic:
split_ifs <;> infer_instance

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

Goal state before:
pp: case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
x : ((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a b)) → X ↑i)
x✝ :
  (∀ (a_1 : ι) (b_1 : a_1 ≤ a), x.1 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩) ∧
    ∀ (a_1 : ι) (b_1 : a < a_1 ∧ a_1 ≤ b), x.2 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩
i : ι
hi : i ≤ b
h1 : ∀ (a_1 : ι) (b_1 : a_1 ≤ a), x.1 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩
h2 : ∀ (a_1 : ι) (b_1 : a < a_1 ∧ a_1 ≤ b), x.2 ⟨a_1, ⋯⟩ ∈ s ⟨a_1, ⋯⟩
hi3 : i ≤ a
⊢ x.1 ⟨i, ⋯⟩ ∈ s ⟨i, ⋯⟩

Tactic:
exact h1 i hi3

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

Goal state before:
pp: α : 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 Ω
t : Set β
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (a : α) in X ⁻¹' t, ((condDistrib Y X μ) (X a)) s ∂μ = μ (X ⁻¹' t ∩ Y ⁻¹' s)

Tactic:
by
  rw [← lintegral_map (Kernel.measurable_coe _ hs) hX, condDistrib, ← Measure.restrict_map hX ht,
    ← Measure.fst_map_prodMk₀ hY, Measure.setLIntegral_condKernel_eq_measure_prod ht hs,
    Measure.map_apply_of_aemeasurable (hX.aemeasurable.prodMk hY) (ht.prod hs), mk_preimage_prod]

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

Goal state before:
pp: case refine_2
α : 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
⊢ ∀ (s_1 : Set α), MeasurableSet s_1 → μ s_1 < ∞ → IntegrableOn (fun a ↦ ((condDistrib Y X μ) (X a)).real s) s_1 μ

Tactic:
exact fun t _ _ => (integrable_toReal_condDistrib hX.aemeasurable hs).integrableOn

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ Tendsto (fun m ↦ (κ a).real (univ ×ˢ seq m)) atTop (𝓝 0)

Tactic:
rw [← ENNReal.toReal_zero]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ Tendsto (fun m ↦ (κ a).real (univ ×ˢ seq m)) atTop (𝓝 (ENNReal.toReal 0))
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)
inst✝ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ IsProbabilityMeasure (Measure.map (restrict₂ ⋯) (μ (I.sup id)))

Tactic:
exact Measure.isProbabilityMeasure_map (measurable_restrict₂ _).aemeasurable

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

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
⊢ 0 ≤ κ.rnDerivAux η a x

Tactic:
rw [rnDerivAux]

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
⊢ 0 ≤ if hα : Countable α then ((∂κ a/∂η a) x).toReal else (κ.map fun a ↦ (a, ())).density η a x univ
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ✝ η : Kernel α γ
hα : Countable α
a a' : α
c : γ
ha'_mem_a : a' ∈ measurableAtom a
κ : Kernel α γ
⊢ κ a' = κ a

Tactic:
by
      ext s hs
      exact mem_of_mem_measurableAtom ha'_mem_a
        (Kernel.measurable_coe κ hs (measurableSet_singleton (κ a s))) rfl

Goal state after:
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)
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)
A_cyl : ∀ (n : ℕ), ∃ s S, MeasurableSet S ∧ A n = cylinder s S
⊢ Tendsto (fun n ↦ (piContent μ) (A n)) atTop (𝓝 0)

Tactic:
choose s S mS A_eq using A_cyl

Goal state after:
ι : 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)
⊢ Tendsto (fun n ↦ (piContent μ) (A n)) atTop (𝓝 0)
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 κ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
h_ae : (κ.withDensity f).rnDeriv κ a =ᵐ[κ a] ∂(κ.withDensity f) a/∂κ a
hf' : ∀ (a : α), Measurable (f a)
⊢ (κ.withDensity f).rnDeriv κ a =ᵐ[κ a] f a

Tactic:
filter_upwards [h_ae, (κ a).rnDeriv_withDensity (hf' a)] with x hx1 hx2

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel (κ.withDensity f)
hf : Measurable (Function.uncurry f)
a : α
h_ae : (κ.withDensity f).rnDeriv κ a =ᵐ[κ a] ∂(κ.withDensity f) a/∂κ a
hf' : ∀ (a : α), Measurable (f a)
x : γ
hx1 : (κ.withDensity f).rnDeriv κ a x = (∂(κ.withDensity f) a/∂κ a) x
hx2 : (∂(κ a).withDensity (f a)/∂κ a) x = f a x
⊢ (κ.withDensity f).rnDeriv κ a x = f a x
Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
inst✝ : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ⟂ₘ η a
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
h_eq : ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a
h1 : ∀ (a : α), (η a) (Prod.mk a ⁻¹' s) = 0
h2 : ∀ᵐ (a : α) ∂μ, (κ a) (Prod.mk a ⁻¹' s)ᶜ = 0
⊢ ∫⁻ (a : α), (η a) (Prod.mk a ⁻¹' s) ∂ν = 0 ∧ ∫⁻ (a : α), (κ a) (Prod.mk a ⁻¹' sᶜ) ∂μ = 0

Tactic:
simp [h1, lintegral_congr_ae h2]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
inst✝ : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂ν, κ a ⟂ₘ η a
⊢ ∀ᵐ (a : α) ∂ν, η a ⟂ₘ κ a

Tactic:
MutuallySingular.comm,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
inst✝ : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂ν, κ a ⟂ₘ η a
⊢ ∀ᵐ (a : α) ∂ν, κ a ⟂ₘ η a
Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
inst✝ : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂ν, κ a ⟂ₘ η a
⊢ ∀ᵐ (a : α) ∂ν, κ a ⟂ₘ η a

Tactic:
hκη

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
f : (i : ι) → X i
⊢ ∀ (s : Finset ι) (t : (i : ι) → Set (X i)),
    (∀ (i : ι), MeasurableSet (t i)) → (dirac f) ((↑s).pi t) = ∏ i ∈ s, (dirac (f i)) (t i)

Tactic:
by simp +contextual [MeasurableSet.pi, Finset.countable_toSet]

Goal state after:
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.swap Ω 𝓨) ∘ₘ μ ⊗ₘ (η ∘ₖ κ)

Tactic:
Measure.compProd_eq_comp_prod,

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.swap Ω 𝓨) ∘ₘ ⇑(Kernel.id ×ₖ (η ∘ₖ κ)) ∘ₘ μ
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 : ∀ᵐ (b : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) b ≪ μ
⊢ μ ⊗ₘ κ ≪ μ.prod (⇑κ ∘ₘ μ)

Tactic:
suffices (κ ∘ₘ μ) ⊗ₘ κ†μ ≪ (κ ∘ₘ μ).prod μ by
    rw [← swap_compProd_posterior, ← Measure.prod_swap, Measure.swap_comp]
    exact this.map measurable_swap

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 : ∀ᵐ (b : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) b ≪ μ
⊢ (⇑κ ∘ₘ μ) ⊗ₘ κ†μ ≪ (⇑κ ∘ₘ μ).prod μ
Module: Mathlib.Probability.Distributions.Cauchy

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

Tactic:
unfold cauchyPDF

Goal state after:
x₀ : ℝ
γ : ℝ≥0
⊢ Measurable fun x ↦ ENNReal.ofReal (cauchyPDFReal x₀ γ x)
Module: Mathlib.Probability.Distributions.Cauchy

Goal state before:
pp: x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
⊢ ∫⁻ (x : ℝ), cauchyPDF x₀ γ x = 1

Tactic:
unfold cauchyPDF

Goal state after:
x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
⊢ ∫⁻ (x : ℝ), ENNReal.ofReal (cauchyPDFReal x₀ γ x) = 1
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case e'_6
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
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
x : (i : ↥(Iic b)) → X ↑i
y : (n : ℕ) → X n
⊢ uncurry (fun x y ↦ A.indicator (fun x ↦ f x y) x) (x, y) = (A ×ˢ Set.univ).indicator (uncurry f) (x, y)

Tactic:
by_cases hx : x ∈ A

Goal state after:
case pos
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
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
x : (i : ↥(Iic b)) → X ↑i
y : (n : ℕ) → X n
hx : x ∈ A
⊢ uncurry (fun x y ↦ A.indicator (fun x ↦ f x y) x) (x, y) = (A ×ˢ Set.univ).indicator (uncurry f) (x, y)

case neg
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
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
x : (i : ↥(Iic b)) → X ↑i
y : (n : ℕ) → X n
hx : x ∉ A
⊢ uncurry (fun x y ↦ A.indicator (fun x ↦ f x y) x) (x, y) = (A ×ˢ Set.univ).indicator (uncurry f) (x, y)
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)
μ₀ : Measure (X 0)
inst✝ : IsProbabilityMeasure μ₀
a : ℕ
⊢ Measure.map (frestrictLe a) (trajMeasure μ₀ κ) ⊗ₘ κ a =
    Measure.map (fun x ↦ (frestrictLe a x, x (a + 1))) (trajMeasure μ₀ κ)

Tactic:
Measure.compProd_eq_comp_prod,

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)
μ₀ : Measure (X 0)
inst✝ : IsProbabilityMeasure μ₀
a : ℕ
⊢ ⇑(Kernel.id ×ₖ κ a) ∘ₘ Measure.map (frestrictLe a) (trajMeasure μ₀ κ) =
    Measure.map (fun x ↦ (frestrictLe a x, x (a + 1))) (trajMeasure μ₀ κ)
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
R : Type u_2
inst✝⁵ : NatCast R
inst✝⁴ : MeasurableSpace R
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : Countable R
inst✝ : MeasurableSingletonClass R
r : ℝ≥0
f : R → E
hf : Integrable f Po(R, r)
⊢ ∫ (x : R), f x ∂Po(R, r) = ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f ↑n

Tactic:
integral_map .of_discrete .of_discrete

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
R : Type u_2
inst✝⁵ : NatCast R
inst✝⁴ : MeasurableSpace R
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : Countable R
inst✝ : MeasurableSingletonClass R
r : ℝ≥0
f : R → E
hf : Integrable f Po(R, r)
⊢ ∫ (x : ℕ), f ↑x ∂Po(r) = ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f ↑n
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

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

Tactic:
simp only [← tsum_dite_right, ENNReal.tsum_mul_left.symm, ENNReal.tsum_mul_right.symm]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
⊢ (∑' (a_1 : β) (i : α),
      (p i * if h : p i = 0 then 0 else (f i h) a_1) *
        if h : (∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) a_1) = 0 then 0 else (g a_1 h) a) =
    ∑' (a_1 : α) (i : β),
      p a_1 * if h : p a_1 = 0 then 0 else (f a_1 h) i * if h : (f a_1 h) i = 0 then 0 else (g i ⋯) a
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: case false
p : ℝ≥0
h : p ≤ 1
⊢ ¬1 - ↑p = 0 ↔ false ∈ {b | bif b then ¬p = 0 else ¬p = 1}

Tactic:
Bool.cond_prop,

Goal state after:
case false
p : ℝ≥0
h : p ≤ 1
⊢ ¬1 - ↑p = 0 ↔ false ∈ {b | if b = true then ¬p = 0 else ¬p = 1}