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

Tactic:
classical
    exact IsRatStieltjesPoint.ite (IsRatStieltjesPoint f) id
      (fun _ ↦ isRatStieltjesPoint_defaultRatCDF a)
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
a : α
h : ∀ (t : ℝ), stieltjesFunctionAux f a t = ⨅ (r : { r' : ℚ // t < (↑r' : ℝ) }), f a (↑r : ℚ)
⊢ stieltjesFunctionAux f a = fun (t : ℝ) ↦ ⨅ (r : { r' : ℚ // t < (↑r' : ℝ) }), f a (↑r : ℚ)

Tactic:
ext t
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
a : α
t : ℝ
⊢ stieltjesFunctionAux f a t = ⨅ (r : { r' : ℚ // t < (↑r' : ℝ) }), f a (↑r : ℚ)

Tactic:
IsMeasurableRatCDF.stieltjesFunctionAux_def f a t

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_def
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
a : α
t : ℝ
⊢ stieltjesFunctionAux f a t = ⨅ (r : { r' : ℚ // t < (↑r' : ℝ) }), f a (↑r : ℚ)

Tactic:
exact IsMeasurableRatCDF.stieltjesFunctionAux_def f a t

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_def
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ stieltjesFunctionAux (fun (p : Unit × α) ↦ f p.2) ((), a) = stieltjesFunctionAux f a

Tactic:
simp_rw [IsMeasurableRatCDF.stieltjesFunctionAux_def']

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_def'
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
rw :
  Eq (α := ℝ) (⨅ (q : { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) }), f a (↑q : ℚ))
    (⨅ (r_1 : (↑(Ioi r) : Type)), f a (↑r_1 : ℚ))
⊢ stieltjesFunctionAux f a (↑r : ℝ) = f a r

Tactic:
rw [← hf.iInf_rat_gt_eq a r, IsMeasurableRatCDF.stieltjesFunctionAux]

Premises used: ProbabilityTheory.IsMeasurableRatCDF.iInf_rat_gt_eq, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
⊢ Eq (α := ℝ) (⨅ (q : { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) }), f a (↑q : ℚ))
    (⨅ (r_1 : (↑(Ioi r) : Type)), f a (↑r_1 : ℚ))

Tactic:
Equiv.iInf_congr ?_ ?_

Premises used: Equiv.iInf_congr
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
refine_1 : { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) } ≃ (↑(Ioi r) : Type)
refine_2 :
  ∀ (x : { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) }),
    f a
        (↑(({
                  toFun := fun (t : { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) }) ↦
                    Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi r) (↑t : ℚ) ⋯,
                  invFun := fun (t : (↑(Ioi r) : Type)) ↦
                    Subtype.mk (p := fun (q' : ℚ) ↦ LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ)) (↑t : ℚ) ⋯,
                  left_inv := ⋯, right_inv := ⋯ :
                  { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) } ≃ (↑(Ioi r) : Type) } :
                (a : { q' : ℚ // (↑r : ℝ) < (↑q' : ℝ) }) → (↑(Ioi r) : Type))
              x) :
          ℚ) =
      f a (↑x : ℚ)
⊢ Eq (α := ℝ) (⨅ (q : { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) }), f a (↑q : ℚ))
    (⨅ (r_1 : (↑(Ioi r) : Type)), f a (↑r_1 : ℚ))

Tactic:
refine Equiv.iInf_congr ?_ ?_

Premises used: Equiv.iInf_congr
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
t : { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) }
⊢ (fun (t : (↑(Ioi r) : Type)) ↦
        (Subtype.mk (p := fun (q' : ℚ) ↦ LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ)) (↑t : ℚ) ⋯ :
          { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) }))
      ((fun (t : { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) }) ↦
          Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi r) (↑t : ℚ) ⋯)
        t) =
    t

Tactic:
simp only [Subtype.coe_eta]

Premises used: Subtype.coe_eta
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
t : (↑(Ioi r) : Type)
⊢ (fun (t : { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) }) ↦ Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi r) (↑t : ℚ) ⋯)
      ((fun (t : (↑(Ioi r) : Type)) ↦
          (Subtype.mk (p := fun (q' : ℚ) ↦ LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ)) (↑t : ℚ) ⋯ :
            { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) }))
        t) =
    t

Tactic:
simp only [Subtype.coe_eta]

Premises used: Subtype.coe_eta
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
⊢ { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) } ≃ (↑(Ioi r) : Type)

Tactic:
exact
      { toFun := fun t ↦ ⟨t.1, mod_cast t.2⟩
        invFun := fun t ↦ ⟨t.1, mod_cast t.2⟩
        left_inv := fun t ↦ by simp only [Subtype.coe_eta]
        right_inv := fun t ↦ by simp only [Subtype.coe_eta] }
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
t : { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) }
⊢ f a
      (↑(({
                toFun := fun (t : { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) }) ↦
                  Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi r) (↑t : ℚ) ⋯,
                invFun := fun (t : (↑(Ioi r) : Type)) ↦
                  Subtype.mk (p := fun (q' : ℚ) ↦ LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ)) (↑t : ℚ) ⋯,
                left_inv := ⋯, right_inv := ⋯ : { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) } ≃ (↑(Ioi r) : Type) } :
              (a : { q' : ℚ // (↑r : ℝ) < (↑q' : ℝ) }) → (↑(Ioi r) : Type))
            t) :
        ℚ) =
    f a (↑t : ℚ)

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

Premises used: Subtype.coe_mk, Equiv.coe_fn_mk
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
obtain : ∀ (r_1 : ℚ) (hrx : r < (↑r_1 : ℝ)), Nonempty { r' : ℚ // r < (↑r' : ℝ) }
⊢ Nonempty { r' : ℚ // r < (↑r' : ℝ) }

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

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

Tactic:
⟨⟨r, hrx⟩⟩

Premises used: Nonempty.intro, Subtype.mk
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r_1 : ℝ
r : ℚ
hrx : r_1 < (↑r : ℝ)
⊢ Nonempty { r' : ℚ // r_1 < (↑r' : ℝ) }

Tactic:
exact ⟨⟨r, hrx⟩⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
⊢ Nonempty { r' : ℚ // r < (↑r' : ℝ) }

Tactic:
have : Nonempty { r' : ℚ // r < ↑r' } := by
    obtain ⟨r, hrx⟩ := exists_rat_gt r
    exact ⟨⟨r, hrx⟩⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
this : Nonempty { r' : ℚ // r < (↑r' : ℝ) }
rw : LE.le (α := ℝ) 0 (⨅ (q : { q' : ℚ // r < (↑q' : ℝ) }), f a (↑q : ℚ))
⊢ 0 ≤ stieltjesFunctionAux f a r

Tactic:
rw [IsMeasurableRatCDF.stieltjesFunctionAux_def]

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

Tactic:
le_ciInf fun r' ↦ hf.nonneg a _

Premises used: ProbabilityTheory.IsMeasurableRatCDF.nonneg, le_ciInf, Subtype.val
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
this : Nonempty { r' : ℚ // r < (↑r' : ℝ) }
⊢ LE.le (α := ℝ) 0 (⨅ (q : { q' : ℚ // r < (↑q' : ℝ) }), f a (↑q : ℚ))

Tactic:
exact le_ciInf fun r' ↦ hf.nonneg a _

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

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

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

Tactic:
⟨⟨r, hrx⟩⟩

Premises used: Nonempty.intro, Subtype.mk
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
r : ℚ
hrx : y < (↑r : ℝ)
⊢ Nonempty { r' : ℚ // y < (↑r' : ℝ) }

Tactic:
exact ⟨⟨r, hrx⟩⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
⊢ Nonempty { r' : ℚ // y < (↑r' : ℝ) }

Tactic:
have : Nonempty { r' : ℚ // y < ↑r' } := by
    obtain ⟨r, hrx⟩ := exists_rat_gt y
    exact ⟨⟨r, hrx⟩⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
this : Nonempty { r' : ℚ // y < (↑r' : ℝ) }
simp_rw :
  LE.le (α := ℝ) (⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f a (↑q : ℚ)) (⨅ (q : { q' : ℚ // y < (↑q' : ℝ) }), f a (↑q : ℚ))
⊢ stieltjesFunctionAux f a x ≤ stieltjesFunctionAux f a y

Tactic:
simp_rw [IsMeasurableRatCDF.stieltjesFunctionAux_def]

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

Tactic:
le_ciInf fun r ↦ (ciInf_le ?_ ?_).trans_eq ?_

Premises used: LE.le.trans_eq, le_ciInf, ciInf_le
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
this : Nonempty { r' : ℚ // y < (↑r' : ℝ) }
refine_1 :
  ∀ (r : { q' : ℚ // y < (↑q' : ℝ) }), BddBelow (α := ℝ) (range fun (q : { q' : ℚ // x < (↑q' : ℝ) }) ↦ f a (↑q : ℚ))
refine_2 : (r : { q' : ℚ // y < (↑q' : ℝ) }) → { q' : ℚ // x < (↑q' : ℝ) }
refine_3 :
  ∀ (r : { q' : ℚ // y < (↑q' : ℝ) }),
    f a (↑(Subtype.mk (p := fun (q' : ℚ) ↦ x < (↑q' : ℝ)) (↑r : ℚ) ⋯) : ℚ) = f a (↑r : ℚ)
⊢ LE.le (α := ℝ) (⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f a (↑q : ℚ)) (⨅ (q : { q' : ℚ // y < (↑q' : ℝ) }), f a (↑q : ℚ))

Tactic:
refine le_ciInf fun r ↦ (ciInf_le ?_ ?_).trans_eq ?_

Premises used: LE.le.trans_eq, le_ciInf, ciInf_le
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
this : Nonempty { r' : ℚ // y < (↑r' : ℝ) }
r : { q' : ℚ // y < (↑q' : ℝ) }
⊢ BddBelow (α := ℝ) (range fun (q : { q' : ℚ // x < (↑q' : ℝ) }) ↦ f a (↑q : ℚ))

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 y : ℝ
hxy : x ≤ y
this : Nonempty { r' : ℚ // y < (↑r' : ℝ) }
r : { q' : ℚ // y < (↑q' : ℝ) }
refine_1 : ∀ (z : ℝ), Membership.mem (γ := Set ℝ) (range fun (q : { q' : ℚ // x < (↑q' : ℝ) }) ↦ f a (↑q : ℚ)) z → 0 ≤ z
⊢ BddBelow (α := ℝ) (range fun (q : { q' : ℚ // x < (↑q' : ℝ) }) ↦ f a (↑q : ℚ))

Tactic:
refine ⟨0, fun z ↦ ?_⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
this : Nonempty { r' : ℚ // y < (↑r' : ℝ) }
r : { q' : ℚ // y < (↑q' : ℝ) }
u : { q' : ℚ // x < (↑q' : ℝ) }
⊢ LE.le (α := ℝ) 0 ((fun (q : { q' : ℚ // x < (↑q' : ℝ) }) ↦ f a (↑q : ℚ)) 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 y : ℝ
hxy : x ≤ y
this : Nonempty { r' : ℚ // y < (↑r' : ℝ) }
r : { q' : ℚ // y < (↑q' : ℝ) }
u : { q' : ℚ // x < (↑q' : ℝ) }
⊢ LE.le (α := ℝ) 0 ((fun (q : { q' : ℚ // x < (↑q' : ℝ) }) ↦ f a (↑q : ℚ)) 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 y : ℝ
hxy : x ≤ y
this : Nonempty { r' : ℚ // y < (↑r' : ℝ) }
r : { q' : ℚ // y < (↑q' : ℝ) }
⊢ { q' : ℚ // x < (↑q' : ℝ) }

Tactic:
exact ⟨r.1, hxy.trans_lt r.prop⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
this : Nonempty { r' : ℚ // y < (↑r' : ℝ) }
r : { q' : ℚ // y < (↑q' : ℝ) }
⊢ f a (↑(Subtype.mk (p := fun (q' : ℚ) ↦ x < (↑q' : ℝ)) (↑r : ℚ) ⋯) : ℚ) = f a (↑r : ℚ)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
rw : ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x
⊢ ContinuousWithinAt (stieltjesFunctionAux f a) (Ici x) x

Tactic:
rw [← continuousWithinAt_Ioi_iff_Ici]

Premises used: continuousWithinAt_Ioi_iff_Ici
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (sInf (stieltjesFunctionAux f a '' Ioi x)))

Tactic:
Monotone.tendsto_nhdsGT (monotone_stieltjesFunctionAux hf a) x

Premises used: ProbabilityTheory.IsMeasurableRatCDF.monotone_stieltjesFunctionAux, Monotone.tendsto_nhdsGT
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
a₁ :
  ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x ↔
    Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (sInf (stieltjesFunctionAux f a '' Ioi x)))
⊢ ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x

Tactic:
convert! Monotone.tendsto_nhdsGT (monotone_stieltjesFunctionAux hf a) x

Premises used: ProbabilityTheory.IsMeasurableRatCDF.monotone_stieltjesFunctionAux, Monotone.tendsto_nhdsGT
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
a₁ :
  ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x ↔
    Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (⨅ (a_1 : (↑(Ioi x) : Type)), stieltjesFunctionAux f a (↑a_1 : ℝ)))
⊢ ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x ↔
    Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (sInf (stieltjesFunctionAux f a '' Ioi x)))

Tactic:
rw [sInf_image']

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

Tactic:
Real.iInf_Ioi_eq_iInf_rat_gt x ?_ (monotone_stieltjesFunctionAux hf a)

Premises used: Real.iInf_Ioi_eq_iInf_rat_gt, ProbabilityTheory.IsMeasurableRatCDF.monotone_stieltjesFunctionAux
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
refine : BddBelow (stieltjesFunctionAux f a '' Ioi x)
⊢ Eq (α := ℝ) (⨅ (r : (↑(Ioi x) : Type)), stieltjesFunctionAux f a (↑r : ℝ))
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), stieltjesFunctionAux f a (↑(↑r : ℚ) : ℝ))

Tactic:
refine Real.iInf_Ioi_eq_iInf_rat_gt x ?_ (monotone_stieltjesFunctionAux hf a)

Premises used: Real.iInf_Ioi_eq_iInf_rat_gt, ProbabilityTheory.IsMeasurableRatCDF.monotone_stieltjesFunctionAux
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ BddBelow (stieltjesFunctionAux f a '' Ioi x)

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 : ℝ
refine : ∀ z ∈ stieltjesFunctionAux f a '' Ioi x, 0 ≤ z
⊢ BddBelow (stieltjesFunctionAux f a '' Ioi x)

Tactic:
refine ⟨0, fun z ↦ ?_⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x u : ℝ
⊢ 0 ≤ stieltjesFunctionAux f a u

Tactic:
stieltjesFunctionAux_nonneg hf a u

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x u : ℝ
⊢ 0 ≤ stieltjesFunctionAux f a u

Tactic:
exact stieltjesFunctionAux_nonneg hf a u

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

Tactic:
have h' : ⨅ r : Ioi x, stieltjesFunctionAux f a r
      = ⨅ r : { r' : ℚ // x < r' }, stieltjesFunctionAux f a r := by
    refine Real.iInf_Ioi_eq_iInf_rat_gt x ?_ (monotone_stieltjesFunctionAux hf a)
    refine ⟨0, fun z ↦ ?_⟩
    rintro ⟨u, -, rfl⟩
    exact stieltjesFunctionAux_nonneg hf a u
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
h' :
  Eq (α := ℝ) (⨅ (r : (↑(Ioi x) : Type)), stieltjesFunctionAux f a (↑r : ℝ))
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), stieltjesFunctionAux f a (↑(↑r : ℚ) : ℝ))
e_s : ∀ (r : { r' : ℚ // x < (↑r' : ℝ) }), stieltjesFunctionAux f a (↑(↑r : ℚ) : ℝ) = f a (↑r : ℚ)
⊢ Eq (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), stieltjesFunctionAux f a (↑(↑r : ℚ) : ℝ))
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ))

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

Tactic:
stieltjesFunctionAux_eq hf a r

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_eq, Subtype.val
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
h' :
  Eq (α := ℝ) (⨅ (r : (↑(Ioi x) : Type)), stieltjesFunctionAux f a (↑r : ℝ))
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), stieltjesFunctionAux f a (↑(↑r : ℚ) : ℝ))
r : { r' : ℚ // x < (↑r' : ℝ) }
⊢ stieltjesFunctionAux f a (↑(↑r : ℚ) : ℝ) = f a (↑r : ℚ)

Tactic:
exact stieltjesFunctionAux_eq hf a r

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_eq, Subtype.val
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
h' :
  Eq (α := ℝ) (⨅ (r : (↑(Ioi x) : Type)), stieltjesFunctionAux f a (↑r : ℝ))
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), stieltjesFunctionAux f a (↑(↑r : ℚ) : ℝ))
⊢ Eq (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), stieltjesFunctionAux f a (↑(↑r : ℚ) : ℝ))
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ))

Tactic:
have h'' :
    ⨅ r : { r' : ℚ // x < r' }, stieltjesFunctionAux f a r =
      ⨅ r : { r' : ℚ // x < r' }, f a r := by
    congr with r
    exact stieltjesFunctionAux_eq hf a r
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
h' :
  Eq (α := ℝ) (⨅ (r : (↑(Ioi x) : Type)), stieltjesFunctionAux f a (↑r : ℝ))
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), stieltjesFunctionAux f a (↑(↑r : ℚ) : ℝ))
h'' :
  Eq (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), stieltjesFunctionAux f a (↑(↑r : ℚ) : ℝ))
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ))
a₁ :
  Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (stieltjesFunctionAux f a x)) ↔
    Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)))
⊢ ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x ↔
    Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (⨅ (a_1 : (↑(Ioi x) : Type)), stieltjesFunctionAux f a (↑a_1 : ℝ)))

Tactic:
rw [h', h'', ContinuousWithinAt]

Premises used: ContinuousWithinAt
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
h' :
  Eq (α := ℝ) (⨅ (r : (↑(Ioi x) : Type)), stieltjesFunctionAux f a (↑r : ℝ))
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), stieltjesFunctionAux f a (↑(↑r : ℚ) : ℝ))
h'' :
  Eq (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), stieltjesFunctionAux f a (↑(↑r : ℚ) : ℝ))
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ))
a₁ : stieltjesFunctionAux f a x = ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)
⊢ Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (stieltjesFunctionAux f a x)) ↔
    Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)))

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

Tactic:
rw [stieltjesFunctionAux_def]

Premises used: ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_def