awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
⊢ StronglyMeasurable (β := ℝ) fun (a : α) ↦ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x

Tactic:
(measurable_stieltjesFunction hf x).stronglyMeasurable

Premises used: Measurable.stronglyMeasurable, ProbabilityTheory.IsMeasurableRatCDF.measurable_stieltjesFunction
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
rw :
  ((hf.stieltjesFunction a).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) =
    ENNReal.ofReal ((↑(hf.stieltjesFunction a) : ℝ → ℝ) x - 0)
⊢ ((hf.stieltjesFunction a).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) =
    ENNReal.ofReal ((↑(hf.stieltjesFunction a) : ℝ → ℝ) x)

Tactic:
rw [← sub_zero (hf.stieltjesFunction a x)]

Premises used: sub_zero, StieltjesFunction.toFun, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ ((hf.stieltjesFunction a).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) =
    ENNReal.ofReal ((↑(hf.stieltjesFunction a) : ℝ → ℝ) x - 0)

Tactic:
(hf.stieltjesFunction a).measure_Iic (tendsto_stieltjesFunction_atBot hf a) _

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction, StieltjesFunction.measure_Iic, ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atBot
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ ((hf.stieltjesFunction a).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) =
    ENNReal.ofReal ((↑(hf.stieltjesFunction a) : ℝ → ℝ) x - 0)

Tactic:
exact (hf.stieltjesFunction a).measure_Iic (tendsto_stieltjesFunction_atBot hf a) _

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction, StieltjesFunction.measure_Iic, ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atBot
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
rw : ((hf.stieltjesFunction a).measure : (a : Set ℝ) → ℝ≥0∞) univ = ENNReal.ofReal (HSub.hSub (α := ℝ) 1 0)
⊢ Eq (α := ℝ≥0∞) (((hf.stieltjesFunction a).measure : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [← ENNReal.ofReal_one, ← sub_zero (1 : ℝ)]

Premises used: sub_zero, ENNReal.ofReal_one, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ ((hf.stieltjesFunction a).measure : (a : Set ℝ) → ℝ≥0∞) univ = ENNReal.ofReal (HSub.hSub (α := ℝ) 1 0)

Tactic:
StieltjesFunction.measure_univ _ (tendsto_stieltjesFunction_atBot hf a)
    (tendsto_stieltjesFunction_atTop hf a)

Premises used: StieltjesFunction.measure_univ, ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atTop, ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atBot
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ ((hf.stieltjesFunction a).measure : (a : Set ℝ) → ℝ≥0∞) univ = ENNReal.ofReal (HSub.hSub (α := ℝ) 1 0)

Tactic:
exact StieltjesFunction.measure_univ _ (tendsto_stieltjesFunction_atBot hf a)
    (tendsto_stieltjesFunction_atTop hf a)

Premises used: StieltjesFunction.measure_univ, ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atTop, ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atBot
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ IsProbabilityMeasure (m0 := Real.measurableSpace) (hf.stieltjesFunction a).measure

Tactic:
⟨measure_stieltjesFunction_univ hf a⟩

Premises used: ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_univ, MeasureTheory.IsProbabilityMeasure.mk
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
⊢ Measurable (β := Measure ℝ) fun (a : α) ↦ (hf.stieltjesFunction a).measure

Tactic:
apply_rules [StieltjesFunction.measurable_measure, measurable_stieltjesFunction,
    tendsto_stieltjesFunction_atBot, tendsto_stieltjesFunction_atTop]

Premises used: StieltjesFunction.measurable_measure, ProbabilityTheory.IsMeasurableRatCDF.measurable_stieltjesFunction, ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atTop, ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atBot
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
r : ℚ
⊢ (↑(stieltjesOfMeasurableRat f hf a) : ℝ → ℝ) (↑r : ℝ) = toRatCDF f a r

Tactic:
IsMeasurableRatCDF.stieltjesFunction_eq _ a r

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_eq
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
simp_rw :
  Eq (α := StieltjesFunction ℝ)
    { toFun := IsMeasurableRatCDF.stieltjesFunctionAux (toRatCDF fun (p : Unit × α) ↦ f p.2) ((), a), mono' := ⋯,
      right_continuous' := ⋯ }
    { toFun := IsMeasurableRatCDF.stieltjesFunctionAux (fun (p : Unit × α) ↦ toRatCDF f p.2) ((), a), mono' := ⋯,
      right_continuous' := ⋯ }
⊢ stieltjesOfMeasurableRat (fun (p : Unit × α) ↦ f p.2) ⋯ ((), a) = stieltjesOfMeasurableRat f hf a

Tactic:
simp_rw [stieltjesOfMeasurableRat, IsMeasurableRatCDF.stieltjesFunction,
    ← IsMeasurableRatCDF.stieltjesFunctionAux_unit_prod a]

Premises used: ProbabilityTheory.stieltjesOfMeasurableRat, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_unit_prod, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
e_toFun :
  ∀ (x : ℝ),
    IsMeasurableRatCDF.stieltjesFunctionAux (toRatCDF fun (p : Unit × α) ↦ f p.2) ((), a) x =
      IsMeasurableRatCDF.stieltjesFunctionAux (fun (p : Unit × α) ↦ toRatCDF f p.2) ((), a) x
⊢ Eq (α := StieltjesFunction ℝ)
    { toFun := IsMeasurableRatCDF.stieltjesFunctionAux (toRatCDF fun (p : Unit × α) ↦ f p.2) ((), a), mono' := ⋯,
      right_continuous' := ⋯ }
    { toFun := IsMeasurableRatCDF.stieltjesFunctionAux (fun (p : Unit × α) ↦ toRatCDF f p.2) ((), a), mono' := ⋯,
      right_continuous' := ⋯ }

Tactic:
congr 1 with x
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
x : ℝ
e_toFun : ∀ (p : Unit × α), toRatCDF (fun (p : Unit × α) ↦ f p.2) p = toRatCDF f p.2
⊢ IsMeasurableRatCDF.stieltjesFunctionAux (toRatCDF fun (p : Unit × α) ↦ f p.2) ((), a) x =
    IsMeasurableRatCDF.stieltjesFunctionAux (fun (p : Unit × α) ↦ toRatCDF f p.2) ((), a) x

Tactic:
congr 1 with p : 1
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
x : ℝ
fst : Unit
b : α
e_toFun e_toFun₁ : toRatCDF (fun (p : Unit × α) ↦ f p.2) (fst, b) = toRatCDF (fun (p : Unit × α) ↦ f p.2) ((), b)
⊢ toRatCDF (fun (p : Unit × α) ↦ f p.2) (fst, b) = toRatCDF f (fst, b).2

Tactic:
rw [← toRatCDF_unit_prod b]

Premises used: ProbabilityTheory.toRatCDF_unit_prod
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
x : ℝ
p : Unit × α
e_toFun : ∀ (fst : Unit) (b : α), toRatCDF (fun (p : Unit × α) ↦ f p.2) (fst, b) = toRatCDF f (fst, b).2
⊢ toRatCDF (fun (p : Unit × α) ↦ f p.2) p = toRatCDF f p.2

Tactic:
cases p with
  | mk _ b => rw [← toRatCDF_unit_prod b]
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
r : ℝ
⊢ 0 ≤ (↑(stieltjesOfMeasurableRat f hf a) : ℝ → ℝ) r

Tactic:
IsMeasurableRatCDF.stieltjesFunction_nonneg _ a r

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
x : ℝ
⊢ (↑(stieltjesOfMeasurableRat f hf a) : ℝ → ℝ) x ≤ 1

Tactic:
IsMeasurableRatCDF.stieltjesFunction_le_one _ a x

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
⊢ Tendsto (↑(stieltjesOfMeasurableRat f hf a) : ℝ → ℝ) atBot (𝓝 0)

Tactic:
IsMeasurableRatCDF.tendsto_stieltjesFunction_atBot _ a

Premises used: ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atBot
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
⊢ Tendsto (↑(stieltjesOfMeasurableRat f hf a) : ℝ → ℝ) atTop (𝓝 1)

Tactic:
IsMeasurableRatCDF.tendsto_stieltjesFunction_atTop _ a

Premises used: ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atTop
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
x : ℝ
⊢ Measurable (β := ℝ) fun (a : α) ↦ (↑(stieltjesOfMeasurableRat f hf a) : ℝ → ℝ) x

Tactic:
IsMeasurableRatCDF.measurable_stieltjesFunction _ x

Premises used: ProbabilityTheory.IsMeasurableRatCDF.measurable_stieltjesFunction
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
x : ℝ
⊢ StronglyMeasurable (β := ℝ) fun (a : α) ↦ (↑(stieltjesOfMeasurableRat f hf a) : ℝ → ℝ) x

Tactic:
IsMeasurableRatCDF.stronglyMeasurable_stieltjesFunction _ x

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stronglyMeasurable_stieltjesFunction
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
x : ℝ
⊢ ((stieltjesOfMeasurableRat f hf a).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) =
    ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f hf a) : ℝ → ℝ) x)

Tactic:
IsMeasurableRatCDF.measure_stieltjesFunction_Iic _ _ _

Premises used: ProbabilityTheory.stieltjesOfMeasurableRat, ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_Iic
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
⊢ Eq (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f hf a).measure : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
IsMeasurableRatCDF.measure_stieltjesFunction_univ _ _

Premises used: ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_univ, ProbabilityTheory.stieltjesOfMeasurableRat
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
⊢ IsProbabilityMeasure (m0 := Real.measurableSpace) (stieltjesOfMeasurableRat f hf a).measure

Tactic:
IsMeasurableRatCDF.instIsProbabilityMeasure_stieltjesFunction _ _

Premises used: ProbabilityTheory.IsMeasurableRatCDF.instIsProbabilityMeasure_stieltjesFunction, ProbabilityTheory.stieltjesOfMeasurableRat
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
⊢ Measurable (β := Measure ℝ) fun (a : α) ↦ (stieltjesOfMeasurableRat f hf a).measure

Tactic:
IsMeasurableRatCDF.measurable_measure_stieltjesFunction _

Premises used: ProbabilityTheory.stieltjesOfMeasurableRat, ProbabilityTheory.IsMeasurableRatCDF.measurable_measure_stieltjesFunction
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
q r : ℚ
hqr : q ≤ r
c : γ
⊢ LE.le (α := ℝ) (↑q : ℝ) (↑r : ℝ)

Tactic:
exact_mod_cast hqr
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
⊢ Tendsto (β := ℝ)
    (fun (m : ℕ) ↦
      @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (c : γ) ↦
        κ.density κ.fst (a, c).1 (a, c).2 (Iic (↑(s m) : ℝ)))
    atTop (𝓝 0)

Tactic:
tendsto_integral_density_of_antitone le_rfl a s' ?_ ?_ (fun _ ↦ measurableSet_Iic)

Premises used: le_rfl, measurableSet_Iic, ProbabilityTheory.Kernel.tendsto_integral_density_of_antitone
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
refine_1 : Antitone s'
refine_2 : Eq (α := Set ℝ) (⋂ (i : ℕ), s' i) ∅
⊢ Tendsto (β := ℝ)
    (fun (m : ℕ) ↦
      @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (c : γ) ↦
        κ.density κ.fst (a, c).1 (a, c).2 (Iic (↑(s m) : ℝ)))
    atTop (𝓝 0)

Tactic:
refine tendsto_integral_density_of_antitone le_rfl a s' ?_ ?_ (fun _ ↦ measurableSet_Iic)

Premises used: le_rfl, measurableSet_Iic, ProbabilityTheory.Kernel.tendsto_integral_density_of_antitone
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
⊢ Antitone s'

Tactic:
fun i j hij ↦ Iic_subset_Iic.mpr ?_

Premises used: Iff.mpr, Set.Iic_subset_Iic, Antitone
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
refine_1 : ∀ (i j : ℕ) (hij : i ≤ j), LE.le (α := ℝ) (↑(s j) : ℝ) (↑(s i) : ℝ)
⊢ Antitone s'

Tactic:
refine fun i j hij ↦ Iic_subset_Iic.mpr ?_

Premises used: Iff.mpr, Set.Iic_subset_Iic
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
i j : ℕ
hij : i ≤ j
⊢ LE.le (α := ℝ) (↑(s j) : ℝ) (↑(s i) : ℝ)

Tactic:
mod_cast hs_anti hij

Premises used: cast, Eq.symm, Rat.cast_le._simp_1
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
i j : ℕ
hij : i ≤ j
⊢ LE.le (α := ℝ) (↑(s j) : ℝ) (↑(s i) : ℝ)

Tactic:
exact mod_cast hs_anti hij
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
refine_2 : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), s' i) x ↔ Membership.mem (γ := Set ℝ) ∅ x
⊢ Eq (α := Set ℝ) (⋂ (i : ℕ), s' i) ∅

Tactic:
ext x
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
refine_2 : ∃ (x_1 : ℕ), (↑(s x_1) : ℝ) < x
⊢ Membership.mem (γ := Set ℝ) (⋂ (i : ℕ), s' i) x ↔ Membership.mem (γ := Set ℝ) ∅ x

Tactic:
simp only [mem_iInter, mem_Iic, mem_empty_iff_false, iff_false, not_forall, not_le, s']

Premises used: not_le, iff_false, Set.mem_iInter, Set.mem_Iic, Set.mem_empty_iff_false, Classical.not_forall
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : Tendsto s atTop atBot
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
refine_2 : ∀ (hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → s a ≤ b) (x : ℝ), ∃ (x_1 : ℕ), (↑(s x_1) : ℝ) < x
⊢ ∃ (x_1 : ℕ), (↑(s x_1) : ℝ) < x

Tactic:
rw [tendsto_atTop_atBot] at hs_tendsto

Premises used: Filter.tendsto_atTop_atBot
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
refine_2 : ∀ (q : ℚ) (hq : (↑q : ℝ) < x), ∃ (x_1 : ℕ), (↑(s x_1) : ℝ) < x
⊢ ∃ (x_1 : ℕ), (↑(s x_1) : ℝ) < x

Tactic:
have ⟨q, hq⟩ := exists_rat_lt x
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
q : ℚ
hq : (↑q : ℝ) < x
refine_2 : ∀ (i : ℕ) (hi : ∀ (a : ℕ), i ≤ a → s a ≤ q), ∃ (x_1 : ℕ), (↑(s x_1) : ℝ) < x
⊢ ∃ (x_1 : ℕ), (↑(s x_1) : ℝ) < x

Tactic:
obtain ⟨i, hi⟩ := hs_tendsto q
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
q : ℚ
hq : (↑q : ℝ) < x
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → s a ≤ q
⊢ ∃ (x_1 : ℕ), (↑(s x_1) : ℝ) < x

Tactic:
⟨i, lt_of_le_of_lt ?_ hq⟩

Premises used: lt_of_le_of_lt, Exists.intro
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
q : ℚ
hq : (↑q : ℝ) < x
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → s a ≤ q
refine_2 : LE.le (α := ℝ) (↑(s i) : ℝ) (↑q : ℝ)
⊢ ∃ (x_1 : ℕ), (↑(s x_1) : ℝ) < x

Tactic:
refine ⟨i, lt_of_le_of_lt ?_ hq⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
q : ℚ
hq : (↑q : ℝ) < x
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → s a ≤ q
⊢ LE.le (α := ℝ) (↑(s i) : ℝ) (↑q : ℝ)

Tactic:
mod_cast hi i le_rfl

Premises used: le_rfl, cast, Eq.symm, Rat.cast_le._simp_1
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_anti : Antitone s
hs_tendsto : ∀ (b : ℚ), ∃ (i : ℕ), ∀ (a : ℕ), i ≤ a → s a ≤ b
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
x : ℝ
q : ℚ
hq : (↑q : ℝ) < x
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → s a ≤ q
⊢ LE.le (α := ℝ) (↑(s i) : ℝ) (↑q : ℝ)

Tactic:
exact mod_cast hi i le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
rw :
  Tendsto
    (fun (m : ℕ) ↦
      @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (c : γ) ↦
        κ.density κ.fst (a, c).1 (a, c).2 (Iic (↑(s m) : ℝ)))
    atTop
    (𝓝
      (Measure.real.{u_3} (α := γ × ℝ) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × ℝ)) a)
        {p : γ × ℝ | Membership.mem (γ := Set γ) univ p.1}))
⊢ Tendsto
    (fun (m : ℕ) ↦
      @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (c : γ) ↦
        κ.density κ.fst (a, c).1 (a, c).2 (Iic (↑(s m) : ℝ)))
    atTop (𝓝 (Measure.real.{u_3} (α := γ) (m := mγ) ((κ.fst : (a : α) → Measure γ) a) univ))

Tactic:
rw [fst_real_apply _ _ MeasurableSet.univ]

Premises used: ProbabilityTheory.Kernel.fst_real_apply, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
⊢ Tendsto
    (fun (m : ℕ) ↦
      @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (c : γ) ↦
        κ.density κ.fst (a, c).1 (a, c).2 (Iic (↑(s m) : ℝ)))
    atTop
    (𝓝
      (Measure.real.{u_3} (α := γ × ℝ) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × ℝ)) a)
        {p : γ × ℝ | Membership.mem (γ := Set γ) univ p.1}))

Tactic:
tendsto_integral_density_of_monotone (le_rfl : fst κ ≤ fst κ)
      a s' ?_ ?_ (fun _ ↦ measurableSet_Iic)

Premises used: le_rfl, Set.Mem, Set.univ, setOf, ProbabilityTheory.Kernel.tendsto_integral_density_of_monotone, measurableSet_Iic
-- Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
a : α
s : ℕ → ℚ
hs_mono : Monotone s
hs_tendsto : Tendsto s atTop atTop
s' : ℕ → Set ℝ := fun (n : ℕ) ↦ Iic (↑(s n) : ℝ)
refine_1 : Monotone s'
refine_2 : Eq (α := Set ℝ) (⋃ (i : ℕ), s' i) univ
⊢ Tendsto
    (fun (m : ℕ) ↦
      @integral _ _ _ _ mγ ((κ.fst : (a : α) → Measure γ) a) fun (c : γ) ↦
        κ.density κ.fst (a, c).1 (a, c).2 (Iic (↑(s m) : ℝ)))
    atTop
    (𝓝
      (Measure.real.{u_3} (α := γ × ℝ) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × ℝ)) a)
        {p : γ × ℝ | Membership.mem (γ := Set γ) univ p.1}))

Tactic:
refine tendsto_integral_density_of_monotone (le_rfl : fst κ ≤ fst κ)
      a s' ?_ ?_ (fun _ ↦ measurableSet_Iic)

Premises used: le_rfl, ProbabilityTheory.Kernel.tendsto_integral_density_of_monotone, measurableSet_Iic