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

Tactic:
stieltjesFunctionAux_eq hf a r

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_eq
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
⊢ 0 ≤ (↑(hf.stieltjesFunction a) : ℝ → ℝ) r

Tactic:
stieltjesFunctionAux_nonneg hf a r

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
obtain : ∀ (r : ℚ) (hrx : x < (↑r : ℝ)), (↑(hf.stieltjesFunction a) : ℝ → ℝ) x ≤ 1
⊢ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x ≤ 1

Tactic:
obtain ⟨r, hrx⟩ := exists_rat_gt x

Premises used: exists_rat_gt
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < (↑r : ℝ)
rw : LE.le (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ)) 1
⊢ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x ≤ 1

Tactic:
rw [← StieltjesFunction.iInf_rat_gt_eq]

Premises used: StieltjesFunction.iInf_rat_gt_eq
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < (↑r : ℝ)
simp_rw : LE.le (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)) 1
⊢ LE.le (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ)) 1

Tactic:
simp_rw [IsMeasurableRatCDF.stieltjesFunction_eq]

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_eq
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < (↑r : ℝ)
⊢ LE.le (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)) 1

Tactic:
ciInf_le_of_le ?_ ?_ (hf.le_one _ _)

Premises used: ciInf_le_of_le, ProbabilityTheory.IsMeasurableRatCDF.le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < (↑r : ℝ)
refine_1 : BddBelow (α := ℝ) (range fun (r : { r' : ℚ // x < (↑r' : ℝ) }) ↦ f a (↑r : ℚ))
refine_2 : { r' : ℚ // x < (↑r' : ℝ) }
⊢ LE.le (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)) 1

Tactic:
refine ciInf_le_of_le ?_ ?_ (hf.le_one _ _)

Premises used: ciInf_le_of_le, ProbabilityTheory.IsMeasurableRatCDF.le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < (↑r : ℝ)
⊢ BddBelow (α := ℝ) (range fun (r : { r' : ℚ // x < (↑r' : ℝ) }) ↦ f a (↑r : ℚ))

Tactic:
⟨0, fun z ↦ ?_⟩

Premises used: Set.Nonempty, BddBelow, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < (↑r : ℝ)
refine_1 : ∀ (z : ℝ), Membership.mem (γ := Set ℝ) (range fun (r : { r' : ℚ // x < (↑r' : ℝ) }) ↦ f a (↑r : ℚ)) z → 0 ≤ z
⊢ BddBelow (α := ℝ) (range fun (r : { r' : ℚ // x < (↑r' : ℝ) }) ↦ f a (↑r : ℚ))

Tactic:
refine ⟨0, fun z ↦ ?_⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < (↑r : ℝ)
u : { r' : ℚ // x < (↑r' : ℝ) }
⊢ LE.le (α := ℝ) 0 ((fun (r : { r' : ℚ // x < (↑r' : ℝ) }) ↦ f a (↑r : ℚ)) u)

Tactic:
hf.nonneg a _

Premises used: ProbabilityTheory.IsMeasurableRatCDF.nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < (↑r : ℝ)
u : { r' : ℚ // x < (↑r' : ℝ) }
⊢ LE.le (α := ℝ) 0 ((fun (r : { r' : ℚ // x < (↑r' : ℝ) }) ↦ f a (↑r : ℚ)) u)

Tactic:
exact hf.nonneg a _

Premises used: ProbabilityTheory.IsMeasurableRatCDF.nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < (↑r : ℝ)
⊢ { r' : ℚ // x < (↑r' : ℝ) }

Tactic:
exact ⟨r, hrx⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ ∀ (x : ℝ), ∃ (q : ℚ), x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1

Tactic:
have h_exists : ∀ x : ℝ, ∃ q : ℚ, x < q ∧ ↑q < x + 1 := fun x ↦ exists_rat_btwn (lt_add_one x)
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1)
rw : ∀ (b : ℚ), ∃ (i : ℝ), ∀ a ≤ i, qs a ≤ b
⊢ Tendsto qs atBot atBot

Tactic:
rw [tendsto_atBot_atBot]

Premises used: Filter.tendsto_atBot_atBot
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1)
⊢ ∀ (b : ℚ), ∃ (i : ℝ), ∀ a ≤ i, qs a ≤ b

Tactic:
fun q ↦ ⟨q - 1, fun y hy ↦ ?_⟩

Premises used: HSub.hSub, Rat.cast, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1)
refine : ∀ (q : ℚ) (y : ℝ) (hy : y ≤ HSub.hSub (α := ℝ) (↑q : ℝ) 1), qs y ≤ q
⊢ ∀ (b : ℚ), ∃ (i : ℝ), ∀ a ≤ i, qs a ≤ b

Tactic:
refine fun q ↦ ⟨q - 1, fun y hy ↦ ?_⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1)
q : ℚ
y : ℝ
hy : y ≤ HSub.hSub (α := ℝ) (↑q : ℝ) 1
⊢ (↑(qs y) : ℝ) ≤ HSub.hSub (α := ℝ) (↑q : ℝ) 1 + 1

Tactic:
have h_le : ↑(qs y) ≤ (q : ℝ) - 1 + 1 :=
      (h_exists y).choose_spec.2.le.trans (add_le_add hy le_rfl)
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1)
q : ℚ
y : ℝ
hy : y ≤ HSub.hSub (α := ℝ) (↑q : ℝ) 1
h_le : (↑(qs y) : ℝ) ≤ HSub.hSub (α := ℝ) (↑q : ℝ) 1 + 1
⊢ LE.le (α := ℝ) (↑(qs y) : ℝ) (↑q : ℝ)

Tactic:
rw [sub_add_cancel] at h_le

Premises used: sub_add_cancel
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1)
q : ℚ
y : ℝ
hy : y ≤ HSub.hSub (α := ℝ) (↑q : ℝ) 1
h_le : LE.le (α := ℝ) (↑(qs y) : ℝ) (↑q : ℝ)
⊢ qs y ≤ q

Tactic:
mod_cast h_le

Premises used: cast, Rat.cast_le._simp_1
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1)
q : ℚ
y : ℝ
hy : y ≤ HSub.hSub (α := ℝ) (↑q : ℝ) 1
h_le : LE.le (α := ℝ) (↑(qs y) : ℝ) (↑q : ℝ)
⊢ qs y ≤ q

Tactic:
exact mod_cast h_le
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1)
⊢ Tendsto qs atBot atBot

Tactic:
have hqs_tendsto : Tendsto qs atBot atBot := by
    rw [tendsto_atBot_atBot]
    refine fun q ↦ ⟨q - 1, fun y hy ↦ ?_⟩
    have h_le : ↑(qs y) ≤ (q : ℝ) - 1 + 1 :=
      (h_exists y).choose_spec.2.le.trans (add_le_add hy le_rfl)
    rw [sub_add_cancel] at h_le
    exact mod_cast h_le
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1)
hqs_tendsto : Tendsto qs atBot atBot
⊢ Tendsto (↑(hf.stieltjesFunction a) : ℝ → ℝ) atBot (𝓝 0)

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    ((hf.tendsto_atBot_zero a).comp hqs_tendsto) (stieltjesFunction_nonneg hf a) fun x ↦ ?_

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds, ProbabilityTheory.IsMeasurableRatCDF.tendsto_atBot_zero, Filter.Tendsto.comp, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1)
hqs_tendsto : Tendsto qs atBot atBot
refine : ∀ (x : ℝ), (↑(hf.stieltjesFunction a) : ℝ → ℝ) x ≤ (f a ∘ qs) x
⊢ Tendsto (↑(hf.stieltjesFunction a) : ℝ → ℝ) atBot (𝓝 0)

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    ((hf.tendsto_atBot_zero a).comp hqs_tendsto) (stieltjesFunction_nonneg hf a) fun x ↦ ?_

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds, ProbabilityTheory.IsMeasurableRatCDF.tendsto_atBot_zero, Filter.Tendsto.comp, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1)
hqs_tendsto : Tendsto qs atBot atBot
x : ℝ
rw : (↑(hf.stieltjesFunction a) : ℝ → ℝ) x ≤ (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(qs x) : ℝ)
⊢ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x ≤ (f a ∘ qs) x

Tactic:
rw [Function.comp_apply, ← stieltjesFunction_eq hf]

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_eq, Function.comp_apply
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1)
hqs_tendsto : Tendsto qs atBot atBot
x : ℝ
⊢ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x ≤ (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(qs x) : ℝ)

Tactic:
(hf.stieltjesFunction a).mono (h_exists x).choose_spec.1.le

Premises used: Exists.choose_spec, LT.lt.le, StieltjesFunction.mono, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction, And.left
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x < (↑q : ℝ) ∧ (↑q : ℝ) < x + 1)
hqs_tendsto : Tendsto qs atBot atBot
x : ℝ
⊢ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x ≤ (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(qs x) : ℝ)

Tactic:
exact (hf.stieltjesFunction a).mono (h_exists x).choose_spec.1.le

Premises used: Exists.choose_spec, LT.lt.le, StieltjesFunction.mono, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction, And.left
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x

Tactic:
have h_exists : ∀ x : ℝ, ∃ q : ℚ, x - 1 < q ∧ ↑q < x := fun x ↦ exists_rat_btwn (sub_one_lt x)
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
rw : ∀ (b : ℚ), ∃ (i : ℝ), ∀ (a : ℝ), i ≤ a → b ≤ qs a
⊢ Tendsto qs atTop atTop

Tactic:
rw [tendsto_atTop_atTop]

Premises used: Filter.tendsto_atTop_atTop
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
⊢ ∀ (b : ℚ), ∃ (i : ℝ), ∀ (a : ℝ), i ≤ a → b ≤ qs a

Tactic:
fun q ↦ ⟨q + 1, fun y hy ↦ ?_⟩

Premises used: Rat.cast, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
refine : ∀ (q : ℚ) (y : ℝ) (hy : HAdd.hAdd (α := ℝ) (↑q : ℝ) 1 ≤ y), q ≤ qs y
⊢ ∀ (b : ℚ), ∃ (i : ℝ), ∀ (a : ℝ), i ≤ a → b ≤ qs a

Tactic:
refine fun q ↦ ⟨q + 1, fun y hy ↦ ?_⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
q : ℚ
y : ℝ
hy : HAdd.hAdd (α := ℝ) (↑q : ℝ) 1 ≤ y
⊢ y - 1 ≤ (↑(qs y) : ℝ)

Tactic:
have h_le : y - 1 ≤ qs y := (h_exists y).choose_spec.1.le
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
q : ℚ
y : ℝ
hy : HAdd.hAdd (α := ℝ) (↑q : ℝ) 1 ≤ y
h_le : y - 1 ≤ (↑(qs y) : ℝ)
⊢ y ≤ HAdd.hAdd (α := ℝ) (↑(qs y) : ℝ) 1

Tactic:
rw [sub_le_iff_le_add] at h_le

Premises used: sub_le_iff_le_add
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
q : ℚ
y : ℝ
hy : HAdd.hAdd (α := ℝ) (↑q : ℝ) 1 ≤ y
h_le : y ≤ HAdd.hAdd (α := ℝ) (↑(qs y) : ℝ) 1
⊢ q ≤ qs y

Tactic:
exact_mod_cast le_of_add_le_add_right (hy.trans h_le)

Premises used: le_of_add_le_add_right, LE.le.trans
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
⊢ Tendsto qs atTop atTop

Tactic:
have hqs_tendsto : Tendsto qs atTop atTop := by
    rw [tendsto_atTop_atTop]
    refine fun q ↦ ⟨q + 1, fun y hy ↦ ?_⟩
    have h_le : y - 1 ≤ qs y := (h_exists y).choose_spec.1.le
    rw [sub_le_iff_le_add] at h_le
    exact_mod_cast le_of_add_le_add_right (hy.trans h_le)
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
hqs_tendsto : Tendsto qs atTop atTop
⊢ Tendsto (↑(hf.stieltjesFunction a) : ℝ → ℝ) atTop (𝓝 1)

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le ((hf.tendsto_atTop_one a).comp hqs_tendsto)
      tendsto_const_nhds ?_ (stieltjesFunction_le_one hf a)

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds, Filter.Tendsto.comp, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_le_one, ProbabilityTheory.IsMeasurableRatCDF.tendsto_atTop_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
hqs_tendsto : Tendsto qs atTop atTop
refine : f a ∘ qs ≤ (↑(hf.stieltjesFunction a) : ℝ → ℝ)
⊢ Tendsto (↑(hf.stieltjesFunction a) : ℝ → ℝ) atTop (𝓝 1)

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le ((hf.tendsto_atTop_one a).comp hqs_tendsto)
      tendsto_const_nhds ?_ (stieltjesFunction_le_one hf a)

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds, Filter.Tendsto.comp, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_le_one, ProbabilityTheory.IsMeasurableRatCDF.tendsto_atTop_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
hqs_tendsto : Tendsto qs atTop atTop
x : ℝ
rw : (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(qs x) : ℝ) ≤ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x
⊢ (f a ∘ qs) x ≤ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x

Tactic:
rw [Function.comp_apply, ← stieltjesFunction_eq hf]

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_eq, Function.comp_apply
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
hqs_tendsto : Tendsto qs atTop atTop
x : ℝ
⊢ (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(qs x) : ℝ) ≤ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x

Tactic:
(hf.stieltjesFunction a).mono (le_of_lt (h_exists x).choose_spec.2)

Premises used: Exists.choose_spec, le_of_lt, StieltjesFunction.mono, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction, And.right
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ (q : ℚ), x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x
qs : ℝ → ℚ := fun (x : ℝ) ↦ ⋯.choose (p := fun (q : ℚ) ↦ x - 1 < (↑q : ℝ) ∧ (↑q : ℝ) < x)
hqs_tendsto : Tendsto qs atTop atTop
x : ℝ
⊢ (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(qs x) : ℝ) ≤ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x

Tactic:
exact (hf.stieltjesFunction a).mono (le_of_lt (h_exists x).choose_spec.2)

Premises used: Exists.choose_spec, le_of_lt, StieltjesFunction.mono, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction, And.right
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
h : ∀ (a : α), (↑(hf.stieltjesFunction a) : ℝ → ℝ) x = ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)
⊢ Eq.{u_1 + 1} (α := (a : α) → ℝ) (fun (a : α) ↦ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x) fun (a : α) ↦
    ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)

Tactic:
ext1 a
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
a : α
h :
  Eq (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ))
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ))
⊢ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x = ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)

Tactic:
rw [← StieltjesFunction.iInf_rat_gt_eq]

Premises used: StieltjesFunction.iInf_rat_gt_eq
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
a : α
h : ∀ (q : { r' : ℚ // x < (↑r' : ℝ) }), (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(↑q : ℚ) : ℝ) = f a (↑q : ℚ)
⊢ Eq (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ))
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ))

Tactic:
congr with q
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
a : α
q : { r' : ℚ // x < (↑r' : ℝ) }
h h₁ : f a (↑q : ℚ) = f a (↑q : ℚ)
⊢ (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(↑q : ℚ) : ℝ) = f a (↑q : ℚ)

Tactic:
rw [stieltjesFunction_eq]

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_eq
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
⊢ Eq.{u_1 + 1} (α := (a : α) → ℝ) (fun (a : α) ↦ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x) fun (a : α) ↦
    ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)

Tactic:
have : (fun a ↦ hf.stieltjesFunction a x) = fun a ↦ ⨅ r : { r' : ℚ // x < r' }, f a ↑r := by
    ext1 a
    rw [← StieltjesFunction.iInf_rat_gt_eq]
    congr with q
    rw [stieltjesFunction_eq]
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
this :
  Eq.{u_1 + 1} (α := (a : α) → ℝ) (fun (a : α) ↦ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x) fun (a : α) ↦
    ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)
rw : Measurable (β := ℝ) fun (a : α) ↦ ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)
⊢ Measurable (β := ℝ) fun (a : α) ↦ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x

Tactic:
rw [this]
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
this :
  Eq.{u_1 + 1} (α := (a : α) → ℝ) (fun (a : α) ↦ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x) fun (a : α) ↦
    ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)
⊢ Measurable (β := ℝ) fun (a : α) ↦ ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)

Tactic:
.iInf (fun q ↦ hf.measurable.eval)

Premises used: Measurable.eval, Measurable.iInf, ProbabilityTheory.IsMeasurableRatCDF.measurable
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
x : ℝ
this :
  Eq.{u_1 + 1} (α := (a : α) → ℝ) (fun (a : α) ↦ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x) fun (a : α) ↦
    ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)
⊢ Measurable (β := ℝ) fun (a : α) ↦ ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)

Tactic:
exact .iInf (fun q ↦ hf.measurable.eval)