awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b : β | (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r}
hs : MeasurableSet s
h_2_le :
  LE.le (α := (x : β) → ℝ≥0∞)
    (s.indicator fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
    (s.indicator fun (x : β) ↦ r)
h_ne_zero :
  Ne (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
        {x : β | (((κCond : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
| (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
rw [← one_mul (κ.fst a s)]

Premises used: DFunLike.coe, ProbabilityTheory.Kernel.fst, one_mul
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b : β | (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r}
hs : MeasurableSet s
h_2_le :
  LE.le (α := (x : β) → ℝ≥0∞)
    (s.indicator fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
    (s.indicator fun (x : β) ↦ r)
h_ne_zero :
  Ne (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
        {x : β | (((κCond : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
pos :
  HMul.hMul (β := ℝ≥0∞) r ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) r ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) <
    (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
conv_rhs => rw [← one_mul (κ.fst a s)]

Premises used: DFunLike.coe, ProbabilityTheory.Kernel.fst, one_mul
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b : β | (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r}
hs : MeasurableSet s
h_2_le :
  LE.le (α := (x : β) → ℝ≥0∞)
    (s.indicator fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
    (s.indicator fun (x : β) ↦ r)
h_ne_zero :
  Ne (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
        {x : β | (((κCond : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
pos : Ne (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) r ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b : β | (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r}
hs : MeasurableSet s
h_2_le :
  LE.le (α := (x : β) → ℝ≥0∞)
    (s.indicator fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
    (s.indicator fun (x : β) ↦ r)
h_ne_zero :
  Ne (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
        {x : β | (((κCond : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond_1 : Kernel (α × β) Ω
inst : Countable α
κCond : α → Kernel β Ω
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
⊢ Measurable (β := Measure Ω) fun (p : α × β) ↦ (κCond p.1 : (a : β) → Measure Ω) p.2

Tactic:
measurable_from_prod_countable_right' (fun a ↦ (κCond a).measurable) fun x y hx hy ↦ ?_

Premises used: measurable_from_prod_countable_right', ProbabilityTheory.Kernel.measurable
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond_1 : Kernel (α × β) Ω
inst : Countable α
κCond : α → Kernel β Ω
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
refine :
  ∀ (x y : α) (hx : β) (hy : y ∈ measurableAtom x),
    Eq.{u_3 + 1} (α := Measure Ω) ((κCond (y, hx).1 : (a : β) → Measure Ω) (y, hx).2 : Measure Ω)
      ((κCond (x, hx).1 : (a : β) → Measure Ω) (x, hx).2 : Measure Ω)
⊢ Measurable (β := Measure Ω) fun (p : α × β) ↦ (κCond p.1 : (a : β) → Measure Ω) p.2

Tactic:
refine measurable_from_prod_countable_right' (fun a ↦ (κCond a).measurable) fun x y hx hy ↦ ?_

Premises used: measurable_from_prod_countable_right'
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond_1 : Kernel (α × β) Ω
inst : Countable α
κCond : α → Kernel β Ω
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
x y : α
hx : β
hy : y ∈ measurableAtom x
⊢ Eq.{u_3 + 1} (α := Measure Ω) ((κCond (y, hx).1 : (a : β) → Measure Ω) (y, hx).2 : Measure Ω)
    ((κCond (x, hx).1 : (a : β) → Measure Ω) (x, hx).2 : Measure Ω)

Tactic:
simpa using DFunLike.congr (h_atom _ _ hy) rfl

Premises used: DFunLike.congr, rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : Countable α
κCond : α → Kernel β Ω
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
p : α × β
⊢ Eq.{u_3 + 1} (α := Measure Ω) ((condKernelCountable κCond h_atom : (a : α × β) → Measure Ω) p : Measure Ω)
    ((κCond p.1 : (a : β) → Measure Ω) p.2 : Measure Ω)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ_1 : Kernel α (β × Ω)
κCond_1 : Kernel (α × β) Ω
inst : Countable α
κCond : α → Kernel β Ω
inst_1 : ∀ (a : α), IsMarkovKernel (κCond a)
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
inst_3 : ∀ (a : α), Measure.IsCondKernel ((κ : (a : α) → Measure (β × Ω)) a) (κCond a)
disintegrate : κ.fst ⊗ₖ condKernelCountable κCond h_atom = κ
⊢ κ.IsCondKernel (condKernelCountable κCond h_atom)

Tactic:
constructor
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ_1 : Kernel α (β × Ω)
κCond_1 : Kernel (α × β) Ω
inst : Countable α
κCond : α → Kernel β Ω
inst_1 : ∀ (a : α), IsMarkovKernel (κCond a)
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
inst_3 : ∀ (a : α), Measure.IsCondKernel ((κ : (a : α) → Measure (β × Ω)) a) (κCond a)
disintegrate :
  ∀ (a : α) (s : Set (β × Ω)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((κ.fst ⊗ₖ condKernelCountable κCond h_atom : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) :
            (a : Set (β × Ω)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ κ.fst ⊗ₖ condKernelCountable κCond h_atom = κ

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ_1 : Kernel α (β × Ω)
κCond_1 : Kernel (α × β) Ω
inst : Countable α
κCond : α → Kernel β Ω
inst_1 : ∀ (a : α), IsMarkovKernel (κCond a)
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
inst_3 : ∀ (a : α), Measure.IsCondKernel ((κ : (a : α) → Measure (β × Ω)) a) (κCond a)
a : α
s : Set (β × Ω)
hs : MeasurableSet s
rw :
  ((Measure.fst.{u_2, u_3} (β := Ω) ((κ : (a : α) → Measure (β × Ω)) a) ⊗ₘ κCond a : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
| ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← (κ a).disintegrate (κCond a)]

Premises used: MeasureTheory.Measure.disintegrate, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ_1 : Kernel α (β × Ω)
κCond_1 : Kernel (α × β) Ω
inst : Countable α
κCond : α → Kernel β Ω
inst_1 : ∀ (a : α), IsMarkovKernel (κCond a)
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
inst_3 : ∀ (a : α), Measure.IsCondKernel ((κ : (a : α) → Measure (β × Ω)) a) (κCond a)
a : α
s : Set (β × Ω)
hs : MeasurableSet s
disintegrate :
  Eq (α := ℝ≥0∞)
    ((((κ.fst ⊗ₖ condKernelCountable κCond h_atom : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) :
          (a : Set (β × Ω)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((Measure.fst.{u_2, u_3} (β := Ω) ((κ : (a : α) → Measure (β × Ω)) a) ⊗ₘ κCond a : (a : Set (β × Ω)) → ℝ≥0∞) s :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((κ.fst ⊗ₖ condKernelCountable κCond h_atom : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) :
          (a : Set (β × Ω)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
conv_rhs => rw [← (κ a).disintegrate (κCond a)]

Premises used: MeasureTheory.Measure.disintegrate, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ_1 : Kernel α (β × Ω)
κCond_1 : Kernel (α × β) Ω
inst : Countable α
κCond : α → Kernel β Ω
inst_1 : ∀ (a : α), IsMarkovKernel (κCond a)
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
inst_3 : ∀ (a : α), Measure.IsCondKernel ((κ : (a : α) → Measure (β × Ω)) a) (κCond a)
a : α
s : Set (β × Ω)
hs : MeasurableSet s
disintegrate :
  ∫⁻ (b : β),
      (((κCond a : (a : β) → Measure Ω) b : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      (((κCond a : (a : β) → Measure Ω) b : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂Measure.fst.{u_2, u_3} (β := Ω) ((κ : (a : α) → Measure (β × Ω)) a)
⊢ Eq (α := ℝ≥0∞)
    ((((κ.fst ⊗ₖ condKernelCountable κCond h_atom : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) :
          (a : Set (β × Ω)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((Measure.fst.{u_2, u_3} (β := Ω) ((κ : (a : α) → Measure (β × Ω)) a) ⊗ₘ κCond a : (a : Set (β × Ω)) → ℝ≥0∞) s :
      ℝ≥0∞)

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

Premises used: MeasureTheory.Measure.compProd_apply, ProbabilityTheory.Kernel.condKernelCountable_apply, ProbabilityTheory.Kernel.compProd_apply
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ_1 : Kernel α (β × Ω)
κCond_1 : Kernel (α × β) Ω
inst : Countable α
κCond : α → Kernel β Ω
inst_1 : ∀ (a : α), IsMarkovKernel (κCond a)
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
inst_3 : ∀ (a : α), Measure.IsCondKernel ((κ : (a : α) → Measure (β × Ω)) a) (κCond a)
a : α
s : Set (β × Ω)
hs : MeasurableSet s
⊢ ∫⁻ (b : β),
      (((κCond a : (a : β) → Measure Ω) b : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(κ.fst : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      (((κCond a : (a : β) → Measure Ω) b : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂Measure.fst.{u_2, u_3} (β := Ω) ((κ : (a : α) → Measure (β × Ω)) a)

Tactic:
congr
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
b : β
hb : IsRatStieltjesPoint f (a, b)
⊢ Monotone (f (a, b))

Tactic:
hb.mono

Premises used: ProbabilityTheory.IsRatStieltjesPoint.mono
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (b : β) ↦ IsRatStieltjesPoint f (a, b)) x} x →
          Membership.mem (γ := Set β) {x : β | (fun (b : β) ↦ Monotone (f (a, b))) x} x}
      a_1
h₁ h₂ : ∀ (b : β) (hb : IsRatStieltjesPoint f (a, b)), Monotone (f (a, b))
⊢ ∀ᵐ (b : β) ∂((ν : (a : α) → Measure β) a : Measure β), Monotone (f (a, b))

Tactic:
filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.mono

Premises used: ProbabilityTheory.IsRatCondKernelCDF.isRatStieltjesPoint_ae
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
b : β
hb : IsRatStieltjesPoint f (a, b)
⊢ Tendsto (f (a, b)) atTop (𝓝 1)

Tactic:
hb.tendsto_atTop_one

Premises used: ProbabilityTheory.IsRatStieltjesPoint.tendsto_atTop_one
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (b : β) ↦ IsRatStieltjesPoint f (a, b)) x} x →
          Membership.mem (γ := Set β) {x : β | (fun (b : β) ↦ Tendsto (f (a, b)) atTop (𝓝 1)) x} x}
      a_1
h₁ h₂ : ∀ (b : β) (hb : IsRatStieltjesPoint f (a, b)), Tendsto (f (a, b)) atTop (𝓝 1)
⊢ ∀ᵐ (b : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (f (a, b)) atTop (𝓝 1)

Tactic:
filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.tendsto_atTop_one

Premises used: ProbabilityTheory.IsRatCondKernelCDF.isRatStieltjesPoint_ae
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
b : β
hb : IsRatStieltjesPoint f (a, b)
⊢ Tendsto (f (a, b)) atBot (𝓝 0)

Tactic:
hb.tendsto_atBot_zero

Premises used: ProbabilityTheory.IsRatStieltjesPoint.tendsto_atBot_zero
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (b : β) ↦ IsRatStieltjesPoint f (a, b)) x} x →
          Membership.mem (γ := Set β) {x : β | (fun (b : β) ↦ Tendsto (f (a, b)) atBot (𝓝 0)) x} x}
      a_1
h₁ h₂ : ∀ (b : β) (hb : IsRatStieltjesPoint f (a, b)), Tendsto (f (a, b)) atBot (𝓝 0)
⊢ ∀ᵐ (b : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (f (a, b)) atBot (𝓝 0)

Tactic:
filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.tendsto_atBot_zero

Premises used: ProbabilityTheory.IsRatCondKernelCDF.isRatStieltjesPoint_ae
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
b : β
hb : IsRatStieltjesPoint f (a, b)
⊢ ∀ (q : ℚ), ⨅ (r : (↑(Ioi q) : Type)), f (a, b) (↑r : ℚ) = f (a, b) q

Tactic:
hb.iInf_rat_gt_eq

Premises used: ProbabilityTheory.IsRatStieltjesPoint.iInf_rat_gt_eq
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (b : β) ↦ IsRatStieltjesPoint f (a, b)) x} x →
          Membership.mem (γ := Set β)
            {x : β | (fun (b : β) ↦ ∀ (q : ℚ), ⨅ (r : (↑(Ioi q) : Type)), f (a, b) (↑r : ℚ) = f (a, b) q) x} x}
      a_1
h₁ h₂ : ∀ (b : β) (hb : IsRatStieltjesPoint f (a, b)) (q : ℚ), ⨅ (r : (↑(Ioi q) : Type)), f (a, b) (↑r : ℚ) = f (a, b) q
⊢ ∀ᵐ (b : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    ∀ (q : ℚ), ⨅ (r : (↑(Ioi q) : Type)), f (a, b) (↑r : ℚ) = f (a, b) q

Tactic:
filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.iInf_rat_gt_eq

Premises used: ProbabilityTheory.IsRatCondKernelCDF.isRatStieltjesPoint_ae
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
h :
  ∀ (a_1 : β) (ha : IsRatStieltjesPoint f (a, a_1)),
    (↑(stieltjesOfMeasurableRat f ⋯ (a, a_1)) : ℝ → ℝ) (↑q : ℝ) = f (a, a_1) q
⊢ (ae (F := Measure β) ((ν : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ)
    (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ)) fun (b : β) ↦ f (a, b) q

Tactic:
filter_upwards [hf.isRatStieltjesPoint_ae a] with a ha

Premises used: ProbabilityTheory.IsRatCondKernelCDF.isRatStieltjesPoint_ae
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a_1 : α
q : ℚ
a : β
ha : IsRatStieltjesPoint f (a_1, a)
h : toRatCDF f (a_1, a) q = f (a_1, a) q
h₁ h₂ : f (a_1, a) q = f (a_1, a) q
⊢ (↑(stieltjesOfMeasurableRat f ⋯ (a_1, a)) : ℝ → ℝ) (↑q : ℝ) = f (a_1, a) q

Tactic:
rw [stieltjesOfMeasurableRat_eq, toRatCDF_of_isRatStieltjesPoint ha]

Premises used: ProbabilityTheory.toRatCDF_of_isRatStieltjesPoint, ProbabilityTheory.stieltjesOfMeasurableRat_eq
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
rw :
  ∀ᵐ (x : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    x ∈ s → (↑(stieltjesOfMeasurableRat f ⋯ (a, x)) : ℝ → ℝ) (↑q : ℝ) = (fun (b : β) ↦ f (a, b) q) x
⊢ (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦
      (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ)) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))

Tactic:
rw [setIntegral_congr_ae hs (g := fun b ↦ f (a, b) q) ?_, hf.setIntegral a hs]

Premises used: ProbabilityTheory.IsRatCondKernelCDF.setIntegral, MeasureTheory.setIntegral_congr_ae
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
b : β
hb : (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ) = f (a, b) q
⊢ b ∈ s → (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ) = f (a, b) q

Tactic:
fun _ ↦ hb