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

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝³ : NormedSpace ℝ E
inst✝² : BorelSpace E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ∫ (x : E), L₁ (x - ∫ (x : E), x ∂μ) * L₂ (x - ∫ (x : E), x ∂μ) ∂μ =
    ∫ (x : E), (L₁ x - ∫ (x : E), L₁ x ∂μ) * (L₂ x - ∫ (x : E), L₂ x ∂μ) ∂μ

Tactic:
have hL (L : StrongDual ℝ E) : μ[L] = L (∫ x, x ∂μ) :=
      L.integral_comp_comm (h.integrable (by simp))

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝³ : NormedSpace ℝ E
inst✝² : BorelSpace E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
hL : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = L (∫ (x : E), x ∂μ)
⊢ ∫ (x : E), L₁ (x - ∫ (x : E), x ∂μ) * L₂ (x - ∫ (x : E), x ∂μ) ∂μ =
    ∫ (x : E), (L₁ x - ∫ (x : E), L₁ x ∂μ) * (L₂ x - ∫ (x : E), L₂ x ∂μ) ∂μ
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: case refine_2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
C C' : ℝ
hint : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
y : E
hy : Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
this : ∀ (x : E), rexp (C' * ‖x‖ ^ 2) ≤ rexp (C / ε * ‖y‖ ^ 2) * rexp (C * ‖x - y‖ ^ 2)
⊢ (fun x ↦ rexp (C' * ‖x‖ ^ 2)) ≤ᵐ[μ] fun x ↦ rexp (C / ε * ‖y‖ ^ 2) * rexp (C * ‖x - y‖ ^ 2)

Tactic:
· exact ae_of_all _ this

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
t : EuclideanSpace ℝ ι
⊢ charFun (Measure.map (toLp 2) (Measure.pi fun x ↦ gaussianReal 0 1)) t = cexp (-↑‖t‖ ^ 2 / 2)

Tactic:
charFun_pi,

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
t : EuclideanSpace ℝ ι
⊢ ∏ i, charFun (gaussianReal 0 1) (t.ofLp i) = cexp (-↑‖t‖ ^ 2 / 2)
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case pos
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : a = 0
⊢ 0 < (1 - c).toReal

Tactic:
simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hc_lt, true_and]
      finiteness

Goal state after:
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)

Tactic:
exact (IsGaussian.hasGaussianLaw_id.prodMk s t).sub

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

Goal state before:
pp: q : ℚ
⊢ 0 ≤ if q < 0 then 0 else 1

Tactic:
split_ifs

Goal state after:
case pos
q : ℚ
h✝ : q < 0
⊢ 0 ≤ 0

case neg
q : ℚ
h✝ : ¬q < 0
⊢ 0 ≤ 1
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: q : ℚ
⊢ (if q < 0 then 0 else 1) ≤ 1

Tactic:
split_ifs

Goal state after:
case pos
q : ℚ
h✝ : q < 0
⊢ 0 ≤ 1

case neg
q : ℚ
h✝ : ¬q < 0
⊢ 1 ≤ 1
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: t : ℚ
y : ↑(Ioi t)
hx : (fun r ↦ if ↑r < 0 then 0 else 1) y ∈ range fun r ↦ if ↑r < 0 then 0 else 1
⊢ 0 ≤ if ↑y < 0 then 0 else 1

Tactic:
split_ifs

Goal state after:
case pos
t : ℚ
y : ↑(Ioi t)
hx : (fun r ↦ if ↑r < 0 then 0 else 1) y ∈ range fun r ↦ if ↑r < 0 then 0 else 1
h✝ : ↑y < 0
⊢ 0 ≤ 0

case neg
t : ℚ
y : ↑(Ioi t)
hx : (fun r ↦ if ↑r < 0 then 0 else 1) y ∈ range fun r ↦ if ↑r < 0 then 0 else 1
h✝ : ¬↑y < 0
⊢ 0 ≤ 1
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: case pos.refine_2
t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : t < 0
x : ↑(Ioi t)
⊢ 0 ≤ if ↑x < 0 then 0 else 1

Tactic:
split_ifs

Goal state after:
case pos
t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : t < 0
x : ↑(Ioi t)
h✝ : ↑x < 0
⊢ 0 ≤ 0

case neg
t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : t < 0
x : ↑(Ioi t)
h✝ : ¬↑x < 0
⊢ 0 ≤ 1
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: case neg.refine_1
t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : ¬t < 0
⊢ (if ↑⟨t + 1, ⋯⟩ < 0 then 0 else 1) ≤ 1

Tactic:
split_ifs

Goal state after:
case pos
t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : ¬t < 0
h✝ : ↑⟨t + 1, ⋯⟩ < 0
⊢ 0 ≤ 1

case neg
t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : ¬t < 0
h✝ : ¬↑⟨t + 1, ⋯⟩ < 0
⊢ 1 ≤ 1
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : (ν a).restrict s = 0
⊢ ∫⁻ (b : β), ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂0 = (κ a) (s ×ˢ Iic x)

Tactic:
lintegral_zero_measure

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : (ν a).restrict s = 0
⊢ 0 = (κ a) (s ×ˢ Iic x)
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t : ℝ≥0
⊢ HasLaw ((-B) t) (gaussianReal 0 t) P

Tactic:
simpa using gaussianReal_neg (hB.hasLaw_eval t)

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ IsCondKernelCDF (fun p ↦ condCDF ρ p.2) (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst)

Tactic:
condCDF_eq_stieltjesOfMeasurableRat_unit_prod ρ

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ IsCondKernelCDF (fun p ↦ stieltjesOfMeasurableRat (fun p r ↦ (preCDF ρ r p.2).toReal) ⋯ ((), p.2))
    (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst)
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
⊢ (fun a ↦ ↑(condCDF ρ a) ↑r) =ᵐ[ρ.fst] fun a ↦ (preCDF ρ r a).toReal

Tactic:
condCDF_eq_stieltjesOfMeasurableRat_unit_prod ρ

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
⊢ (fun a ↦ ↑(stieltjesOfMeasurableRat (fun p r ↦ (preCDF ρ r p.2).toReal) ⋯ ((), a)) ↑r) =ᵐ[ρ.fst] fun a ↦
    (preCDF ρ r a).toReal
Module: Mathlib.Probability.CDF

Goal state before:
pp: μ : Measure ↑I
inst✝ : IsProbabilityMeasure μ
x : ↑I
⊢ ↑(cdf (Measure.map Subtype.val μ)) ↑x = μ.real (Icc 0 x)

Tactic:
by
  have : IsProbabilityMeasure (μ.map Subtype.val) := isProbabilityMeasure_map (by fun_prop)
  rw [ProbabilityTheory.cdf_eq_real,
    map_measureReal_apply measurable_subtype_coe measurableSet_Iic, subtype_Iic_eq_Icc]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
B : ℝ≥0 → Ω → ℝ
hB : IsBrownianReal B P
ω : Ω
⊢ (Continuous fun x ↦ B x ω) → B 0 ω = 0 → Filter.Tendsto (fun x ↦ B x ω) (𝓝 0) (𝓝 0)

Tactic:
h1

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
B : ℝ≥0 → Ω → ℝ
hB : IsBrownianReal B P
ω : Ω
h1 : Continuous fun x ↦ B x ω
⊢ B 0 ω = 0 → Filter.Tendsto (fun x ↦ B x ω) (𝓝 0) (𝓝 0)
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: case hg
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Measurable fun b ↦ ((η ∘ₖ deterministic f hf) ω) (Prod.mk b ⁻¹' s)

Tactic:
exact measurable_measure_prodMk_left hs

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: case convert_9
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 1) P'
hX : Var[X 0; P] ≠ 0
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
mX0 : AEMeasurable (X 0) P
intX0 : Integrable (X 0) P
this :
  ∀ (n : ℕ) (ω : Ω),
    (√(↑n * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P) =
      (√↑n)⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]
⊢ ∀ (i : ℕ),
    IdentDistrib (fun ω ↦ (X i ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P])
      (fun ω ↦ (X 0 ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) P P

Tactic:
· convert! fun n ↦ (hident n).comp (u := fun x ↦ (x - P[X 0]) / √Var[X 0; P]) (by fun_prop)

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

Goal state before:
pp: case hg
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ Measurable fun b ↦ ((η ∘ₖ deterministic f hf) ω) (Prod.mk b ⁻¹' s)

Tactic:
exact measurable_measure_prodMk_left hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) univ ∂ν a -
      ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a =
    (κ a) (s ×ˢ univ) - (κ a) (s ×ˢ t)

Tactic:
setLIntegral_toKernel_univ hf a hs,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ (κ a) (s ×ˢ univ) - ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a =
    (κ a) (s ×ˢ univ) - (κ a) (s ×ˢ t)
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: case e_f.e_f.hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
a : α
b : β
⊢ Measurable fun x ↦ (κ (a, b).2) (Prod.mk x ⁻¹' s)

Tactic:
exact measurable_measure_prodMk_left hs

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

Goal state before:
pp: case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (⋃ i, f i) ∂ν a = (κ a) (s ×ˢ ⋃ i, f i)

Tactic:
simp_rw [measure_iUnion hf_disj hf_meas]

Goal state after:
case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ ∫⁻ (b : β) in s, ∑' (i : ℕ), ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ ⋃ i, f i)
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s : Set Ω
hs : MeasurableSet s
⊢ (ρCond x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)

Tactic:
have := isSFiniteKernel ρ ρCond (by rintro rfl; simp at hx)
  nth_rewrite 2 [← ρ.disintegrate ρCond]
  rw [Measure.compProd_apply (measurableSet_prod.mpr (Or.inl ⟨measurableSet_singleton x, hs⟩))]
  have (a : _) : ρCond a (Prod.mk a ⁻¹' {x} ×ˢ s) = ({x} : Set α).indicator (ρCond · s) a := by
    obtain rfl | hax := eq_or_ne a x
    · simp only [singleton_prod, mem_singleton_iff, indicator_of_mem]
      congr with y
      simp
    · simp only [singleton_prod, mem_singleton_iff, hax, not_false_eq_true, indicator_of_notMem]
      have : Prod.mk a ⁻¹' Prod.mk x '' s = ∅ := by ext y; simp [Ne.symm hax]
      simp only [this, measure_empty]
  simp_rw [this]
  rw [MeasureTheory.lintegral_indicator (measurableSet_singleton x)]
  simp only [Measure.restrict_singleton, lintegral_smul_measure, lintegral_dirac, smul_eq_mul]
  rw [← mul_assoc, ENNReal.inv_mul_cancel hx (measure_ne_top _ _), one_mul]

Goal state after:
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
this : (∀ᵐ (b : β) ∂κ.fst a, (κCond (a, b)) univ ≤ 1) ∧ ∀ᵐ (b : β) ∂κ.fst a, 1 ≤ (κCond (a, b)) univ
b : β
⊢ (κCond (a, b)) univ ≤ 1 → 1 ≤ (κCond (a, b)) univ → (κCond (a, b)) univ = 1

Tactic:
h1

Goal state after:
α : 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
this : (∀ᵐ (b : β) ∂κ.fst a, (κCond (a, b)) univ ≤ 1) ∧ ∀ᵐ (b : β) ∂κ.fst a, 1 ≤ (κCond (a, b)) univ
b : β
h1 : (κCond (a, b)) univ ≤ 1
⊢ 1 ≤ (κCond (a, b)) univ → (κCond (a, b)) univ = 1
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst✝² : Nonempty Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
⊢ Measure.comap (embeddingReal Ω)
      (if (η a) (range (embeddingReal Ω))ᶜ = 0 then η a else Measure.dirac (Exists.choose ⋯)) =
    if (η a) (range (embeddingReal Ω))ᶜ = 0 then Measure.comap (embeddingReal Ω) (η a)
    else Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose ⋯))

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst✝² : Nonempty Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
h✝ : (η a) (range (embeddingReal Ω))ᶜ = 0
⊢ Measure.comap (embeddingReal Ω) (η a) = Measure.comap (embeddingReal Ω) (η a)

case neg
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst✝² : Nonempty Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
h✝ : ¬(η a) (range (embeddingReal Ω))ᶜ = 0
⊢ Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose ⋯)) =
    Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose ⋯))
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst✝² : Nonempty Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
s : Set Ω
hs : MeasurableSet s
he : MeasurableEmbedding (embeddingReal Ω)
h : (η a) (range (embeddingReal Ω))ᶜ = 0
⊢ (Measure.comap (embeddingReal Ω) (η a)) s = (η a) (embeddingReal Ω '' s)

Tactic:
rw [Measure.comap_apply _ he.injective he.measurableSet_image' _ hs]

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
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : ↑S ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ ↑S)
h_disj : Pairwise (Disjoint on fun i ↦ ↑i)
⊢ ∑' (n_1 : ↑↑S), ∫ (x : γ) in ↑n_1, κ.densityProcess ν n a x s ∂ν a = ∑' (a_1 : ↑↑S), ((κ a) (↑a_1 ×ˢ s)).toReal

Tactic:
congr with u
    rw [setIntegral_densityProcess_of_mem hκν _ _ hs (hS_subset (by simp))]
    rfl

Goal state after:
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✝³ : Countable α
κCond : α → Kernel β Ω
inst✝² : ∀ (a : α), IsMarkovKernel (κCond a)
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
inst✝ : ∀ (a : α), (κ a).IsCondKernel (κCond a)
a : α
s : Set (β × Ω)
hs : MeasurableSet s
⊢ ((κ.fst ⊗ₖ condKernelCountable κCond h_atom) a) s = ((κ a).fst ⊗ₘ κCond a) s

Tactic:
simp_rw [compProd_apply hs, condKernelCountable_apply, Measure.compProd_apply hs]

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ✝ : Kernel α (β × Ω)
κCond✝ : Kernel (α × β) Ω
inst✝³ : Countable α
κCond : α → Kernel β Ω
inst✝² : ∀ (a : α), IsMarkovKernel (κCond a)
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
inst✝ : ∀ (a : α), (κ a).IsCondKernel (κCond a)
a : α
s : Set (β × Ω)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), ((κCond a) b) (Prod.mk b ⁻¹' s) ∂κ.fst a = ∫⁻ (b : β), ((κCond a) b) (Prod.mk b ⁻¹' s) ∂(κ a).fst
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 ≤ ν
a : α
inst✝ : IsFiniteKernel ν
s : Set β
hs : MeasurableSet s
t : γ
⊢ Tendsto (fun n ↦ κ.densityProcess ν n a t s) atTop
      (𝓝 (Filtration.limitProcess (fun n x ↦ κ.densityProcess ν n a x s) (countableFiltration γ) (ν a) t)) →
    κ.density ν a t s = Filtration.limitProcess (fun n x ↦ κ.densityProcess ν n a x s) (countableFiltration γ) (ν a) t →
      Tendsto (fun n ↦ κ.densityProcess ν n a t s) atTop (𝓝 (κ.density ν a t s))

Tactic:
h1

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
a : α
inst✝ : IsFiniteKernel ν
s : Set β
hs : MeasurableSet s
t : γ
h1 :
  Tendsto (fun n ↦ κ.densityProcess ν n a t s) atTop
    (𝓝 (Filtration.limitProcess (fun n x ↦ κ.densityProcess ν n a x s) (countableFiltration γ) (ν a) t))
⊢ κ.density ν a t s = Filtration.limitProcess (fun n x ↦ κ.densityProcess ν n a x s) (countableFiltration γ) (ν a) t →
    Tendsto (fun n ↦ κ.densityProcess ν n a t s) atTop (𝓝 (κ.density ν a t s))
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 ≤ ν
a : α
x : γ
s : Set β
⊢ 0 ≤ κ.density ν a x s

Tactic:
refine le_limsup_of_frequently_le ?_ ?_

Goal state after:
case refine_1
α : 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 β
⊢ ∃ᶠ (i : ℕ) in atTop, 0 ≤ κ.densityProcess ν i a x s

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
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

Goal state after:
case pos
α : 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 κ
h✝ : Countable α
⊢ IsMarkovKernel (condKernelCountable (fun a ↦ (κ a).condKernel) ⋯)

case neg
α : 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 κ
h✝ : ¬Countable α
⊢ IsMarkovKernel κ.condKernelBorel
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : DecidableLE ι
X : ι → Type u_2
a b c : ι
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
⊢ IocProdIoc a b c ⁻¹' Set.univ.pi s = Set.univ.pi (restrict₂ ⋯ s) ×ˢ Set.univ.pi (restrict₂ ⋯ s)

Tactic:
by
  ext x
  simp
  grind [IocProdIoc]

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

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 ρ
κ : Kernel (α × β) Ω
inst✝ : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a✝ : α
a : β
⊢ ρ.condKernel (a✝, a) = (ρ a✝).condKernel a → κ (a✝, a) = (ρ a✝).condKernel a → κ (a✝, a) = ρ.condKernel (a✝, a)

Tactic:
h1

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : CountableOrCountablyGenerated α β
ρ : Kernel α (β × Ω)
inst✝¹ : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst✝ : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a✝ : α
a : β
h1 : ρ.condKernel (a✝, a) = (ρ a✝).condKernel a
⊢ κ (a✝, a) = (ρ a✝).condKernel a → κ (a✝, a) = ρ.condKernel (a✝, a)