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

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')}
h_real : ∃ ns, Tendsto ns atTop (𝓝[≠] t) ∧ ∀ (n : ℕ), complexMGF X μ ↑(ns n) = complexMGF Y μ' ↑(ns n)
⊢ ∃ ns, Tendsto ns atTop (𝓝[≠] ↑t) ∧ ∀ (n : ℕ), complexMGF X μ (ns n) = complexMGF Y μ' (ns n)

Tactic:
obtain ⟨xs, hx_tendsto, hx_eq⟩ := h_real

Goal state after:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')}
xs : ℕ → ℝ
hx_tendsto : Tendsto xs atTop (𝓝[≠] t)
hx_eq : ∀ (n : ℕ), complexMGF X μ ↑(xs n) = complexMGF Y μ' ↑(xs n)
⊢ ∃ ns, Tendsto ns atTop (𝓝[≠] ↑t) ∧ ∀ (n : ℕ), complexMGF X μ (ns n) = complexMGF Y μ' (ns n)
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ (-↑↑(2 * v)⁻¹).re < 0

Tactic:
simpa using pos_iff_ne_zero.mpr hv

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

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp id p (Measure.map (⇑L) μ)

Tactic:
IsGaussian.map_eq_gaussianReal L

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp id p (gaussianReal (∫ (x : E), L x ∂μ) Var[⇑L; μ].toNNReal)
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ charFun (Measure.map (⇑L) μ) 1 = charFun (gaussianReal (∫ (x : E), L x ∂μ) Var[⇑L; μ].toNNReal) 1

Tactic:
IsGaussian.map_eq_gaussianReal L

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ charFun (gaussianReal (∫ (x : E), L x ∂μ) Var[⇑L; μ].toNNReal) 1 =
    charFun (gaussianReal (∫ (x : E), L x ∂μ) Var[⇑L; μ].toNNReal) 1
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: case e_a
E : Type u_1
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : MeasurableSpace E
inst✝⁷ : BorelSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopologyEither E F
ν : Measure F
inst✝ : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inl ℝ E F
hL₁ : L₁ = L ∘SL ContinuousLinearMap.inl ℝ E F
L₂ : F →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inr ℝ E F
hL₂ : L₂ = L ∘SL ContinuousLinearMap.inr ℝ E F
⊢ ↑Var[⇑L₁; μ] + ↑Var[⇑L₂; ν] = ↑Var[⇑L; μ.prod ν]

Tactic:
rw [variance_dual_prod' (IsGaussian.memLp_dual μ (L.comp (.inl ℝ E F)) 2 (by simp))
      (IsGaussian.memLp_dual ν (L.comp (.inr ℝ E F)) 2 (by simp))]

Goal state after:
case e_a
E : Type u_1
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : MeasurableSpace E
inst✝⁷ : BorelSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopologyEither E F
ν : Measure F
inst✝ : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inl ℝ E F
hL₁ : L₁ = L ∘SL ContinuousLinearMap.inl ℝ E F
L₂ : F →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inr ℝ E F
hL₂ : L₂ = L ∘SL ContinuousLinearMap.inr ℝ E F
⊢ ↑Var[⇑L₁; μ] + ↑Var[⇑L₂; ν] =
    ↑(Var[⇑(L ∘SL ContinuousLinearMap.inl ℝ E F); μ] + Var[⇑(L ∘SL ContinuousLinearMap.inr ℝ E F); ν])
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: a : ℝ
n : ℕ
⊢ √2 ^ (2 * (n + 2)) = 2 ^ (n + 2)

Tactic:
pow_mul,

Goal state after:
a : ℝ
n : ℕ
⊢ (√2 ^ 2) ^ (n + 2) = 2 ^ (n + 2)
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
hμ : ∫ (x : E), id x ∂μ = 0
L : StrongDual ℝ E
⊢ charFunDual μ L = cexp (-↑Var[⇑L; μ] / 2)

Tactic:
refine charFunDual_eq_of_forall_strongDual_eq_zero (fun L ↦ ?_) L
  simp only [id_eq] at hμ
  simp [integral_dual, hμ]

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
⊢ ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * a ^ 2)) ∂μ =
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))

Tactic:
simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter]

Goal state after:
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
⊢ ENNReal.ofReal (rexp (C * a ^ 2)) * μ (closedBall 0 a) = μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s t : ↥I
⊢ cov[fun x ↦ x s, fun x ↦ x t; projectiveFamily I] = ↑(min ↑s ↑t)

Tactic:
covariance_fun_projectiveFamily,

Goal state after:
I : Finset ℝ≥0
s t : ↥I
⊢ cov[fun x ↦ x.ofLp s, fun x ↦ x.ofLp t; multivariateGaussian 0 (covMatrix I)] = ↑(min ↑s ↑t)
Module: Mathlib.Probability.Process.FiniteDimensionalLaws

Goal state before:
pp: T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
h : ∀ (t : T), X t =ᵐ[P] Y t
⊢ Measure.map (fun ω x ↦ X x ω) P = Measure.map (fun ω x ↦ Y x ω) P

Tactic:
rw [map_eq_iff_forall_finset_map_restrict_eq hX hY]
  exact fun I ↦ map_restrict_eq_of_forall_ae_eq h I

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ¬∃ a, 0 < a ∧ 2⁻¹ < μ {x | ‖x‖ ≤ a} ∧ μ {x | ‖x‖ ≤ a} < 1
⊢ ∃ b, μ {x | ‖x‖ ≤ b} = 1

Tactic:
by
    by_contra h_ne
    push Not at h_meas_Ioo h_ne
    suffices μ .univ ≤ 2⁻¹ by simp at this
    have h_le a : μ {x | ‖x‖ ≤ a} ≤ 2⁻¹ := by
      have h_of_pos a' (ha : 0 < a') : μ {x | ‖x‖ ≤ a'} ≤ 2⁻¹ := by
        by_contra h_lt
        refine h_ne a' ?_
        exact le_antisymm prob_le_one (h_meas_Ioo a' ha (not_le.mp h_lt))
      rcases le_or_gt a 0 with ha | ha
      · calc μ {x | ‖x‖ ≤ a}
        _ ≤ μ {x | ‖x‖ ≤ 1} := measure_mono fun x hx ↦ hx.trans (ha.trans (by positivity))
        _ ≤ 2⁻¹ := h_of_pos _ (by positivity)
      · exact h_of_pos a ha
    have h_univ : (Set.univ : Set E) = ⋃ a : ℕ, {x | ‖x‖ ≤ a} := by
      ext x
      simp only [Set.mem_univ, Set.mem_iUnion, Set.mem_ofPred_eq, true_iff]
      exact exists_nat_ge _
    rw [h_univ, Monotone.measure_iUnion]
    · simp [h_le]
    · intro a b hab x hx
      simp only [Set.mem_ofPred_eq] at hx ⊢
      exact hx.trans (mod_cast hab)

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

Goal state before:
pp: case refine_2
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
t : { q' // ↑r < ↑q' }
⊢ f a ↑({ toFun := fun t ↦ ⟨↑t, ⋯⟩, invFun := fun t ↦ ⟨↑t, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } t) = f a ↑t

Tactic:
simp only [Equiv.coe_fn_mk, Subtype.coe_mk]

Goal state after:
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 : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = (κ a) (s ×ˢ Iic x)

Tactic:
rw [hρ_zero, lintegral_zero_measure]
    have ⟨q, hq⟩ := exists_rat_gt x
    suffices κ a (s ×ˢ Iic (q : ℝ)) = 0 by
      symm
      refine measure_mono_null (fun p ↦ ?_) this
      simp only [mem_prod, mem_Iic, and_imp]
      exact fun h1 h2 ↦ ⟨h1, h2.trans hq.le⟩
    suffices (κ a).real (s ×ˢ Iic (q : ℝ)) = 0 by
      rw [measureReal_eq_zero_iff] at this
      simpa [measure_ne_top] using this
    rw [← hf.setIntegral a hs q]
    simp [hρ_zero]

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

Goal state before:
pp: case neg.h_directed
α : 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
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a =
    ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a
h_nonempty : Nonempty { r' // x < ↑r' }
⊢ Directed (fun x1 x2 ↦ x1 ≥ x2) fun r b ↦ ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r)

Tactic:
refine Monotone.directed_ge fun i j hij b ↦ ?_

Goal state after:
case neg.h_directed
α : 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
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a =
    ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a
h_nonempty : Nonempty { r' // x < ↑r' }
i j : { r' // x < ↑r' }
hij : i ≤ j
b : β
⊢ ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑i) ≤
    ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑j)
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
⊢ ∫ (x : α) in s, (preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd ↑r).real s

Tactic:
by
  rw [integral_toReal]
  · rw [setLIntegral_preCDF_fst _ _ hs, measureReal_def]
  · exact measurable_preCDF.aemeasurable
  · refine ae_restrict_of_ae ?_
    filter_upwards [preCDF_le_one ρ] with a ha
    exact (ha r).trans_lt ENNReal.one_lt_top

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ ∫ (t : β) in A, ⨅ r, f (a, t) ↑r ∂ν a ≤ (κ a).real (A ×ˢ Iic ↑q)

Tactic:
have h : ∀ r : Ioi q, ∫ t in A, ⨅ r' : Ioi q, f (a, t) r' ∂(ν a)
        ≤ (κ a).real (A ×ˢ Iic (r : ℝ)) := by
      intro r
      rw [← hf.setIntegral a hA]
      refine setIntegral_mono_ae ?_ ?_ ?_
      · exact (hf.integrable_iInf_rat_gt _ _).integrableOn
      · exact (hf.integrable _ _).integrableOn
      · filter_upwards [hf.bddBelow_range a] with t ht using ciInf_le (ht _) r
    calc ∫ t in A, ⨅ r : Ioi q, f (a, t) r ∂(ν a)
      ≤ ⨅ r : Ioi q, (κ a).real (A ×ˢ Iic (r : ℝ)) := le_ciInf h
    _ = (κ a).real (A ×ˢ Iic (q : ℝ)) := by
        rw [measureReal_def, ← Measure.iInf_rat_gt_prod_Iic hA q]
        exact (ENNReal.toReal_iInf (fun r ↦ measure_ne_top _ _)).symm

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: case convert_7
Ω : 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]
⊢ Var[X 0; P] / Var[X 0; P] = 1

Tactic:
div_self hX

Goal state after:
case convert_7
Ω : 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]
⊢ 1 = 1
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
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) univ ∂ν a = (κ a) (s ×ˢ univ)

Tactic:
by
  rw [← Real.iUnion_Iic_rat, prod_iUnion]
  have h_dir : Directed (fun x y ↦ x ⊆ y) fun q : ℚ ↦ Iic (q : ℝ) := by
    refine Monotone.directed_le fun r r' hrr' ↦ Iic_subset_Iic.mpr ?_
    exact mod_cast hrr'
  have h_dir_prod : Directed (fun x y ↦ x ⊆ y) fun q : ℚ ↦ s ×ˢ Iic (q : ℝ) := by
    refine Monotone.directed_le fun i j hij ↦ ?_
    refine prod_subset_prod_iff.mpr (Or.inl ⟨subset_rfl, Iic_subset_Iic.mpr ?_⟩)
    exact mod_cast hij
  simp_rw [h_dir.measure_iUnion, h_dir_prod.measure_iUnion]
  rw [lintegral_iSup_directed]
  · simp_rw [setLIntegral_toKernel_Iic hf _ _ hs]
  · refine fun q ↦ Measurable.aemeasurable ?_
    exact (Kernel.measurable_coe _ measurableSet_Iic).comp measurable_prodMk_left
  · refine Monotone.directed_le fun i j hij t ↦ measure_mono (Iic_subset_Iic.mpr ?_)
    exact mod_cast hij

Goal state after:
Module: Mathlib.Probability.Process.PartitionFiltration

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
ht_range : generateFrom (Set.range t) = m
⊢ ⨆ n, ↑(partitionFiltration ht) n = m

Tactic:
iSup_partitionFiltration_eq_generateFrom_range ht,

Goal state after:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
ht_range : generateFrom (Set.range t) = m
⊢ generateFrom (Set.range t) = m
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 ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
⊢ ∫⁻ (a_1 : γ) in u, (κ a) (countablePartitionSet n a_1 ×ˢ s) / (ν a) (countablePartitionSet n a_1) ∂ν a =
    (κ a) (u ×ˢ s)

Tactic:
have : ∫⁻ x in u, κ a (countablePartitionSet n x ×ˢ s) / ν a (countablePartitionSet n x) ∂(ν a)
      = ∫⁻ _ in u, κ a (u ×ˢ s) / ν a u ∂(ν a) := by
    refine setLIntegral_congr_fun hu_meas (fun t ht ↦ ?_)
    rw [countablePartitionSet_of_mem hu ht]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this✝ : IsFiniteKernel κ
hu_meas : MeasurableSet u
this :
  ∫⁻ (x : γ) in u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ∂ν a =
    ∫⁻ (x : γ) in u, (κ a) (u ×ˢ s) / (ν a) u ∂ν a
⊢ ∫⁻ (a_1 : γ) in u, (κ a) (countablePartitionSet n a_1 ×ˢ s) / (ν a) (countablePartitionSet n a_1) ∂ν a =
    (κ a) (u ×ˢ s)
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
⊢ (κ a) (Prod.map id e ⁻¹' (univ ×ˢ range e)ᶜ) = 0

Tactic:
suffices Prod.map id e ⁻¹' (univ ×ˢ range e)ᶜ = ∅ by rw [this]; 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
⊢ Prod.map id e ⁻¹' (univ ×ˢ range e)ᶜ = ∅
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
⊢ (∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω ↦ f (a, ω)) (ρ.condKernel a)) ∧
      Integrable (fun a ↦ ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔
    Integrable f (ρ.fst ⊗ₘ ρ.condKernel)

Tactic:
rw [Measure.integrable_compProd_iff hf]

Goal state after:
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)
⊢ κ = κ'.comapRight h_prod_embed

Tactic:
ext c t : 2

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)
c : α
t : Set (β × Ω)
a✝ : MeasurableSet t
⊢ (κ c) t = ((κ'.comapRight h_prod_embed) c) t
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 Ω
κ : Kernel α (γ × Ω)
inst✝ : IsFiniteKernel κ
⊢ κ.fst ⊗ₖ κ.condKernelBorel = κ

Tactic:
rw [condKernelBorel, compProd_fst_borelMarkovFromReal _ _ (compProd_fst_condKernelReal _)]

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 μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst✝¹ : StandardBorelSpace Ω'
inst✝ : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : AEMeasurable X μ
⊢ Measure.map (Prod.map id f) (Measure.map X μ ⊗ₘ condDistrib Y X μ) = Measure.map X μ ⊗ₘ (condDistrib Y X μ).map f

Tactic:
Measure.compProd_map hf

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst✝¹ : StandardBorelSpace Ω'
inst✝ : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : AEMeasurable X μ
⊢ Measure.map (Prod.map id f) (Measure.map X μ ⊗ₘ condDistrib Y X μ) =
    Measure.map (Prod.map id f) (Measure.map X μ ⊗ₘ condDistrib Y X μ)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case refl
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
⊢ Measure.map (cast ⋯) (μ a) = μ a

Tactic:
exact Measure.map_id

Goal state after: