awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t

Tactic:
exacts [(hf h).iInf_rat_gt_eq, (hg h).iInf_rat_gt_eq]

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

Tactic:
Monotone.le_of_tendsto (hf.isRatStieltjesPoint a).mono
    (hf.isRatStieltjesPoint a).tendsto_atBot_zero q

Premises used: ProbabilityTheory.IsMeasurableRatCDF.isRatStieltjesPoint, ProbabilityTheory.IsRatStieltjesPoint.mono, ProbabilityTheory.IsRatStieltjesPoint.tendsto_atBot_zero, Monotone.le_of_tendsto
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℚ → ℝ
hf : IsMeasurableRatCDF f
a : α
q : ℚ
⊢ f a q ≤ 1

Tactic:
Monotone.ge_of_tendsto (hf.isRatStieltjesPoint a).mono
    (hf.isRatStieltjesPoint a).tendsto_atTop_one q

Premises used: Monotone.ge_of_tendsto, ProbabilityTheory.IsMeasurableRatCDF.isRatStieltjesPoint, ProbabilityTheory.IsRatStieltjesPoint.mono, ProbabilityTheory.IsRatStieltjesPoint.tendsto_atTop_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℚ → ℝ
hf : IsMeasurableRatCDF f
a : α
⊢ Tendsto (f a) atTop (𝓝 1)

Tactic:
(hf.isRatStieltjesPoint a).tendsto_atTop_one

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

Tactic:
(hf.isRatStieltjesPoint a).tendsto_atBot_zero

Premises used: ProbabilityTheory.IsMeasurableRatCDF.isRatStieltjesPoint, ProbabilityTheory.IsRatStieltjesPoint.tendsto_atBot_zero
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → ℚ → ℝ
hf : IsMeasurableRatCDF f
a : α
q : ℚ
⊢ ⨅ (r : (↑(Ioi q) : Type)), f a (↑r : ℚ) = f a q

Tactic:
(hf.isRatStieltjesPoint a).iInf_rat_gt_eq q

Premises used: ProbabilityTheory.IsMeasurableRatCDF.isRatStieltjesPoint, ProbabilityTheory.IsRatStieltjesPoint.iInf_rat_gt_eq
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
x y : ℚ
hxy : x ≤ y
pos : ∀ (h_1 : x < 0) (h_2 : y < 0), LE.le (α := ℝ) 0 0
neg : ∀ (h_1 : x < 0) (h_2 : ¬y < 0), LE.le (α := ℝ) 0 1
pos₁ : ∀ (h_1 : ¬x < 0) (h_2 : y < 0), LE.le (α := ℝ) 1 0
neg₁ : ∀ (h_1 : ¬x < 0) (h_2 : ¬y < 0), LE.le (α := ℝ) 1 1
⊢ LE.le (α := ℝ) (if x < 0 then 0 else 1) (if y < 0 then 0 else 1)

Tactic:
split_ifs with h_1 h_2 h_2
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
x y : ℚ
hxy : x ≤ y
h_1 : x < 0
h_2 : y < 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
x y : ℚ
hxy : x ≤ y
h_1 : x < 0
h_2 : ¬y < 0
⊢ LE.le (α := ℝ) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
x y : ℚ
hxy : x ≤ y
h_1 : ¬x < 0
h_2 : y < 0
⊢ LE.le (α := ℝ) 1 0

Tactic:
absurd (hxy.trans_lt h_2) h_1

Premises used: absurd, LE.le.trans_lt
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
x y : ℚ
hxy : x ≤ y
h_1 : ¬x < 0
h_2 : ¬y < 0
⊢ LE.le (α := ℝ) 1 1

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
x y : ℚ
hxy : x ≤ y
h_1 : x < 0
h_2 : y < 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
exacts [le_rfl, zero_le_one, absurd (hxy.trans_lt h_2) h_1, le_rfl]

Premises used: le_rfl, zero_le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
q : ℚ
pos : q < 0 → LE.le (α := ℝ) 0 0
neg : ¬q < 0 → LE.le (α := ℝ) 0 1
⊢ LE.le (α := ℝ) 0 (if q < 0 then 0 else 1)

Tactic:
split_ifs
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
q : ℚ
h : q < 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
q : ℚ
h : ¬q < 0
⊢ LE.le (α := ℝ) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
q : ℚ
h : q < 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
exacts [le_rfl, zero_le_one]

Premises used: le_rfl, zero_le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
q : ℚ
pos : q < 0 → LE.le (α := ℝ) 0 1
neg : ¬q < 0 → LE.le (α := ℝ) 1 1
⊢ LE.le (α := ℝ) (if q < 0 then 0 else 1) 1

Tactic:
split_ifs
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
q : ℚ
h : q < 0
⊢ LE.le (α := ℝ) 0 1

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
q : ℚ
h : ¬q < 0
⊢ LE.le (α := ℝ) 1 1

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
⊢ Tendsto defaultRatCDF atTop (𝓝 1)

Tactic:
(tendsto_congr' ?_).mp tendsto_const_nhds

Premises used: tendsto_const_nhds, Iff.mp, Filter.tendsto_congr'
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
refine : (fun (x : ℚ) ↦ 1) =ᶠ[atTop] defaultRatCDF
⊢ Tendsto defaultRatCDF atTop (𝓝 1)

Tactic:
refine (tendsto_congr' ?_).mp tendsto_const_nhds

Premises used: tendsto_const_nhds, Iff.mp, Filter.tendsto_congr'
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
rw : ∃ (a : ℚ), ∀ b ≥ a, 1 = defaultRatCDF b
⊢ (fun (x : ℚ) ↦ 1) =ᶠ[atTop] defaultRatCDF

Tactic:
rw [EventuallyEq, eventually_atTop]

Premises used: Filter.EventuallyEq, Filter.eventually_atTop
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
⊢ ∃ (a : ℚ), ∀ b ≥ a, 1 = defaultRatCDF b

Tactic:
⟨0, fun q hq => (if_neg (not_lt.mpr hq)).symm⟩

Premises used: Iff.mpr, not_lt, Exists.intro, OfNat.ofNat, Eq.symm, if_neg
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
⊢ ∃ (a : ℚ), ∀ b ≥ a, 1 = defaultRatCDF b

Tactic:
exact ⟨0, fun q hq => (if_neg (not_lt.mpr hq)).symm⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
⊢ Tendsto defaultRatCDF atBot (𝓝 0)

Tactic:
(tendsto_congr' ?_).mp tendsto_const_nhds

Premises used: tendsto_const_nhds, Iff.mp, Filter.tendsto_congr'
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
refine : (fun (x : ℚ) ↦ 0) =ᶠ[atBot] defaultRatCDF
⊢ Tendsto defaultRatCDF atBot (𝓝 0)

Tactic:
refine (tendsto_congr' ?_).mp tendsto_const_nhds

Premises used: tendsto_const_nhds, Iff.mp, Filter.tendsto_congr'
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
rw : ∃ (a : ℚ), ∀ b ≤ a, 0 = defaultRatCDF b
⊢ (fun (x : ℚ) ↦ 0) =ᶠ[atBot] defaultRatCDF

Tactic:
rw [EventuallyEq, eventually_atBot]

Premises used: Filter.EventuallyEq, Filter.eventually_atBot
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
⊢ ∃ (a : ℚ), ∀ b ≤ a, 0 = defaultRatCDF b

Tactic:
⟨-1, fun q hq => (if_pos (hq.trans_lt ?_)).symm⟩

Premises used: if_pos, Exists.intro, OfNat.ofNat, Eq.symm, LE.le.trans_lt, Neg.neg
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
refine : ∀ (q : ℚ) (hq : q ≤ -1), LT.lt (α := ℚ) (-1) 0
⊢ ∃ (a : ℚ), ∀ b ≤ a, 0 = defaultRatCDF b

Tactic:
refine ⟨-1, fun q hq => (if_pos (hq.trans_lt ?_)).symm⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
q : ℚ
hq : q ≤ -1
linarith : LE.le (α := ℚ) 0 (-1) → -1 + HSub.hSub (α := ℚ) 0 (-1) = 0
⊢ LT.lt (α := ℚ) (-1) 0

Tactic:
linarith
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
⊢ BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)

Tactic:
⟨0, fun x hx ↦ ?_⟩

Premises used: Set.Nonempty, BddBelow, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
refine :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1) x),
    0 ≤ x
⊢ BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)

Tactic:
refine ⟨0, fun x hx ↦ ?_⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1) x
obtain :
  ∀ (y : (↑(Ioi t) : Type))
    (hx :
      Membership.mem (γ := Set ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
        ((fun (r : (↑(Ioi t) : Type)) ↦ (if (↑r : ℚ) < 0 then 0 else 1 : ℝ)) y)),
    LE.le (α := ℝ) 0 ((fun (r : (↑(Ioi t) : Type)) ↦ (if (↑r : ℚ) < 0 then 0 else 1 : ℝ)) y)
⊢ 0 ≤ x

Tactic:
obtain ⟨y, rfl⟩ := mem_range.mpr hx

Premises used: Iff.mpr, Set.mem_range, rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
y : (↑(Ioi t) : Type)
hx :
  Membership.mem (γ := Set ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
    ((fun (r : (↑(Ioi t) : Type)) ↦ (if (↑r : ℚ) < 0 then 0 else 1 : ℝ)) y)
pos : (↑y : ℚ) < 0 → LE.le (α := ℝ) 0 0
neg : ¬(↑y : ℚ) < 0 → LE.le (α := ℝ) 0 1
⊢ LE.le (α := ℝ) 0 (if (↑y : ℚ) < 0 then 0 else 1)

Tactic:
split_ifs
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
y : (↑(Ioi t) : Type)
hx :
  Membership.mem (γ := Set ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
    ((fun (r : (↑(Ioi t) : Type)) ↦ (if (↑r : ℚ) < 0 then 0 else 1 : ℝ)) y)
h : (↑y : ℚ) < 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
y : (↑(Ioi t) : Type)
hx :
  Membership.mem (γ := Set ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
    ((fun (r : (↑(Ioi t) : Type)) ↦ (if (↑r : ℚ) < 0 then 0 else 1 : ℝ)) y)
h : ¬(↑y : ℚ) < 0
⊢ LE.le (α := ℝ) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
y : (↑(Ioi t) : Type)
hx :
  Membership.mem (γ := Set ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
    ((fun (r : (↑(Ioi t) : Type)) ↦ (if (↑r : ℚ) < 0 then 0 else 1 : ℝ)) y)
h : (↑y : ℚ) < 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
exacts [le_rfl, zero_le_one]

Premises used: le_rfl, zero_le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
⊢ BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)

Tactic:
have h_bdd : BddBelow (range fun r : ↥(Ioi t) ↦ ite ((r : ℚ) < 0) (0 : ℝ) 1) := by
    refine ⟨0, fun x hx ↦ ?_⟩
    obtain ⟨y, rfl⟩ := mem_range.mpr hx
    dsimp only
    split_ifs
    exacts [le_rfl, zero_le_one]
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
pos : ∀ (h : t < 0), Eq (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 0
neg : ∀ (h : ¬t < 0), Eq (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 1
⊢ Eq (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) (if t < 0 then 0 else 1)

Tactic:
split_ifs with h
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : t < 0
⊢ Eq (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 0

Tactic:
le_antisymm ?_ (le_ciInf fun x ↦ ?_)

Premises used: le_ciInf, le_antisymm
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : t < 0
pos : LE.le (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 0
pos₁ : ∀ (x : (↑(Ioi t) : Type)), LE.le (α := ℝ) 0 (if (↑x : ℚ) < 0 then 0 else 1)
⊢ Eq (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 0

Tactic:
refine le_antisymm ?_ (le_ciInf fun x ↦ ?_)

Premises used: le_ciInf, le_antisymm
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : t < 0
linarith : t / 2 ≤ t → 2 / 2 = 1
linarith₁ : t / 2 ≤ t → HMul.hMul (α := ℚ) 1 2 = 2
linarith₂ : t / 2 ≤ t → GT.gt (α := ℚ) 2 0
linarith₃ : t / 2 ≤ t → t - 0 + (1 * t - 2 * t) = 0
⊢ t < t / 2

Tactic:
linarith
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : t < 0
linarith : 0 ≤ t / 2 → 2 / 2 = 1
linarith₁ : 0 ≤ t / 2 → HMul.hMul (α := ℚ) 1 2 = 2
linarith₂ : 0 ≤ t / 2 → GT.gt (α := ℚ) 2 0
linarith₃ : 0 ≤ t / 2 → t - 0 + (HMul.hMul (α := ℚ) 2 0 - 1 * t) = 0
⊢ t / 2 < 0

Tactic:
linarith
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : t < 0
pos :
  ∀ (q : ℚ) (htq : t < q) (hq_neg : q < 0), LE.le (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 0
⊢ LE.le (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 0

Tactic:
obtain ⟨q, htq, hq_neg⟩ : ∃ q, t < q ∧ q < 0 := ⟨t / 2, by linarith, by linarith⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : t < 0
q : ℚ
htq : t < q
hq_neg : q < 0
⊢ LE.le (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 0

Tactic:
(ciInf_le h_bdd ⟨q, htq⟩).trans ?_

Premises used: Subtype.mk, ciInf_le, LE.le.trans
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : t < 0
q : ℚ
htq : t < q
hq_neg : q < 0
pos : LE.le (α := ℝ) (if (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) q htq) : ℚ) < 0 then 0 else 1) 0
⊢ LE.le (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 0

Tactic:
refine (ciInf_le h_bdd ⟨q, htq⟩).trans ?_

Premises used: Subtype.mk, ciInf_le, LE.le.trans
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : t < 0
q : ℚ
htq : t < q
hq_neg : q < 0
pos : (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) q htq) : ℚ) < 0
⊢ LE.le (α := ℝ) (if (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) q htq) : ℚ) < 0 then 0 else 1) 0

Tactic:
rw [if_pos]

Premises used: if_pos
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : t < 0
q : ℚ
htq : t < q
hq_neg pos pos₁ pos₂ pos₃ : q < 0
⊢ (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) q htq) : ℚ) < 0

Tactic:
rwa [Subtype.coe_mk]

Premises used: Subtype.coe_mk
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : t < 0
x : (↑(Ioi t) : Type)
pos : (↑x : ℚ) < 0 → LE.le (α := ℝ) 0 0
neg : ¬(↑x : ℚ) < 0 → LE.le (α := ℝ) 0 1
⊢ LE.le (α := ℝ) 0 (if (↑x : ℚ) < 0 then 0 else 1)

Tactic:
split_ifs
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : t < 0
x : (↑(Ioi t) : Type)
h_1 : (↑x : ℚ) < 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : t < 0
x : (↑(Ioi t) : Type)
h_1 : ¬(↑x : ℚ) < 0
⊢ LE.le (α := ℝ) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : t < 0
x : (↑(Ioi t) : Type)
h_1 : (↑x : ℚ) < 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
exacts [le_rfl, zero_le_one]

Premises used: le_rfl, zero_le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : ¬t < 0
⊢ Eq (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 1

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : ¬t < 0
neg : LE.le (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 1
neg₁ : LE.le (α := ℝ) 1 (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1)
⊢ Eq (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 1

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : ¬t < 0
⊢ LE.le (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 1

Tactic:
(ciInf_le h_bdd ⟨t + 1, lt_add_one t⟩).trans ?_

Premises used: lt_add_one, Subtype.mk, HAdd.hAdd, ciInf_le, LE.le.trans, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : ¬t < 0
neg : LE.le (α := ℝ) (if (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) (t + 1) ⋯) : ℚ) < 0 then 0 else 1) 1
⊢ LE.le (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 1

Tactic:
refine (ciInf_le h_bdd ⟨t + 1, lt_add_one t⟩).trans ?_

Premises used: lt_add_one, Subtype.mk, HAdd.hAdd, ciInf_le, LE.le.trans, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : ¬t < 0
pos : (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) (t + 1) ⋯) : ℚ) < 0 → LE.le (α := ℝ) 0 1
neg : ¬(↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) (t + 1) ⋯) : ℚ) < 0 → LE.le (α := ℝ) 1 1
⊢ LE.le (α := ℝ) (if (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) (t + 1) ⋯) : ℚ) < 0 then 0 else 1) 1

Tactic:
split_ifs
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : ¬t < 0
h_1 : (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) (t + 1) ⋯) : ℚ) < 0
⊢ LE.le (α := ℝ) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : ¬t < 0
h_1 : ¬(↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) (t + 1) ⋯) : ℚ) < 0
⊢ LE.le (α := ℝ) 1 1

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : ¬t < 0
h_1 : (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) (t + 1) ⋯) : ℚ) < 0
⊢ LE.le (α := ℝ) 0 1

Tactic:
exacts [zero_le_one, le_rfl]

Premises used: le_rfl, zero_le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : ¬t < 0
⊢ LE.le (α := ℝ) 1 (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1)

Tactic:
le_ciInf fun x ↦ ?_

Premises used: le_ciInf
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : ¬t < 0
neg : ∀ (x : (↑(Ioi t) : Type)), LE.le (α := ℝ) 1 (if (↑x : ℚ) < 0 then 0 else 1)
⊢ LE.le (α := ℝ) 1 (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1)

Tactic:
refine le_ciInf fun x ↦ ?_

Premises used: le_ciInf
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : ¬t < 0
x : (↑(Ioi t) : Type)
neg : ¬(↑x : ℚ) < 0
⊢ LE.le (α := ℝ) 1 (if (↑x : ℚ) < 0 then 0 else 1)

Tactic:
rw [if_neg]

Premises used: if_neg
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : ¬t < 0
x : (↑(Ioi t) : Type)
neg : ∀ (h : 0 ≤ t) (x : (↑(Ioi t) : Type)), 0 ≤ (↑x : ℚ)
⊢ ¬(↑x : ℚ) < 0

Tactic:
rw [not_lt] at h ⊢

Premises used: not_lt
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : 0 ≤ t
x : (↑(Ioi t) : Type)
⊢ 0 ≤ (↑x : ℚ)

Tactic:
h.trans (mem_Ioi.mp x.prop).le

Premises used: Set.mem_Ioi, LT.lt.le, Subtype.prop, Iff.mp, LE.le.trans
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : 0 ≤ t
x : (↑(Ioi t) : Type)
⊢ 0 ≤ (↑x : ℚ)

Tactic:
exact h.trans (mem_Ioi.mp x.prop).le

Premises used: Set.mem_Ioi, LT.lt.le, Subtype.prop, Iff.mp, LE.le.trans
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
a : α
h : IsRatStieltjesPoint f a
q : ℚ
rw : (if IsRatStieltjesPoint f a then f a else defaultRatCDF) q = f a q
rw₁ rw₂ : f a q = f a q
⊢ toRatCDF f a q = f a q

Tactic:
rw [toRatCDF, if_pos h]

Premises used: if_pos, ProbabilityTheory.toRatCDF
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
a : α
rw rw₁ :
  (if IsRatStieltjesPoint f a then (fun (p : Unit × α) ↦ f p.2) ((), a) else defaultRatCDF) =
    if IsRatStieltjesPoint f a then f a else defaultRatCDF
⊢ (if IsRatStieltjesPoint (fun (p : Unit × α) ↦ f p.2) ((), a) then (fun (p : Unit × α) ↦ f p.2) ((), a)
    else defaultRatCDF) =
    if IsRatStieltjesPoint f a then f a else defaultRatCDF

Tactic:
rw [isRatStieltjesPoint_unit_prod_iff]

Premises used: ProbabilityTheory.isRatStieltjesPoint_unit_prod_iff
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
⊢ Measurable (toRatCDF f)

Tactic:
Measurable.ite (measurableSet_isRatStieltjesPoint hf) hf measurable_const

Premises used: Measurable.ite, ProbabilityTheory.toRatCDF, measurable_const, ProbabilityTheory.measurableSet_isRatStieltjesPoint
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
⊢ IsRatStieltjesPoint (toRatCDF f) a

Tactic:
IsRatStieltjesPoint.ite (IsRatStieltjesPoint f) id
      (fun _ ↦ isRatStieltjesPoint_defaultRatCDF a)

Premises used: id, ProbabilityTheory.isRatStieltjesPoint_defaultRatCDF, ProbabilityTheory.IsRatStieltjesPoint, ProbabilityTheory.toRatCDF, ProbabilityTheory.IsRatStieltjesPoint.ite
-- Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
a : α
⊢ IsRatStieltjesPoint (toRatCDF f) a

Tactic:
exact IsRatStieltjesPoint.ite (IsRatStieltjesPoint f) id
      (fun _ ↦ isRatStieltjesPoint_defaultRatCDF a)

Premises used: id, ProbabilityTheory.isRatStieltjesPoint_defaultRatCDF, ProbabilityTheory.IsRatStieltjesPoint, ProbabilityTheory.IsRatStieltjesPoint.ite