awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
⊢ MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t}
have rw : MeasurableSet.{u_1} (α := α) (⋂ (i : ℚ), {x : α | ⨅ (r : (↑(Ioi i) : Type)), f x (↑r : ℚ) = f x i})
Tactic: rw [Set.setOf_forall]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : ℚ), {x : α | ⨅ (r : (↑(Ioi i) : Type)), f x (↑r : ℚ) = f x i})
have refine : ∀ (q : ℚ), MeasurableSet.{u_1} (α := α) {x : α | ⨅ (r : (↑(Ioi q) : Type)), f x (↑r : ℚ) = f x q}
Tactic: refine MeasurableSet.iInter (fun q ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (hypothesis)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
⊢ MeasurableSet.{u_1} (α := α) {a : α | IsRatStieltjesPoint f a}
have h4 : MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t}
Tactic: have h4 : MeasurableSet {a | ∀ t : ℚ, ⨅ r : Ioi t, f a r = f a t} := by
    rw [Set.setOf_forall]
    refine MeasurableSet.iInter (fun q ↦ ?_)
    exact measurableSet_eq_fun (.iInf fun _ ↦ hf.eval) hf.eval
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t}
this :
  Eq.{u_1 + 1} (α := Set α) {a : α | IsRatStieltjesPoint f a}
    ({a : α | Monotone (f a)} ∩ {a : α | Tendsto (f a) atTop (𝓝 1)} ∩ {a : α | Tendsto (f a) atBot (𝓝 0)} ∩
      {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t})
⊢ MeasurableSet.{u_1} (α := α) {a : α | IsRatStieltjesPoint f a}
have rw : MeasurableSet.{u_1} (α := α)
  ({a : α | Monotone (f a)} ∩ {a : α | Tendsto (f a) atTop (𝓝 1)} ∩ {a : α | Tendsto (f a) atBot (𝓝 0)} ∩
    {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t}
⊢ MeasurableSet.{u_1} (α := α) {a : α | IsRatStieltjesPoint f a}
have suffices : Eq.{u_1 + 1} (α := Set α) {a : α | IsRatStieltjesPoint f a}
  ({a : α | Monotone (f a)} ∩ {a : α | Tendsto (f a) atTop (𝓝 1)} ∩ {a : α | Tendsto (f a) atBot (𝓝 0)} ∩
    {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t})
Tactic: suffices {a | IsRatStieltjesPoint f a}
      = ({a | Monotone (f a)} ∩ {a | Tendsto (f a) atTop (𝓝 1)} ∩ {a | Tendsto (f a) atBot (𝓝 0)}
        ∩ {a | ∀ t : ℚ, ⨅ r : Ioi t, f a r = f a t}) by
    rw [this]
    exact (((h1.inter h2).inter h3).inter h4)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t}
⊢ Eq.{u_1 + 1} (α := Set α) {a : α | IsRatStieltjesPoint f a}
    ({a : α | Monotone (f a)} ∩ {a : α | Tendsto (f a) atTop (𝓝 1)} ∩ {a : α | Tendsto (f a) atBot (𝓝 0)} ∩
      {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t})
have h : ∀ (a : α),
  Membership.mem (γ := Set α) {a : α | IsRatStieltjesPoint f a} a ↔
    Membership.mem (γ := Set α)
      ({a : α | Monotone (f a)} ∩ {a : α | Tendsto (f a) atTop (𝓝 1)} ∩ {a : α | Tendsto (f a) atBot (𝓝 0)} ∩
        {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t})
      a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t}
a : α
⊢ IsRatStieltjesPoint f a ↔
    ((Monotone (f a) ∧ Tendsto (f a) atTop (𝓝 1)) ∧ Tendsto (f a) atBot (𝓝 0)) ∧
      ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t
have h : ∀ (h : IsRatStieltjesPoint f a),
  ((Monotone (f a) ∧ Tendsto (f a) atTop (𝓝 1)) ∧ Tendsto (f a) atBot (𝓝 0)) ∧
    ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet.{u_1} (α := α) {a : α | ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t}
a : α
h :
  ∀ (h : IsRatStieltjesPoint f a),
    ((Monotone (f a) ∧ Tendsto (f a) atTop (𝓝 1)) ∧ Tendsto (f a) atBot (𝓝 0)) ∧
      ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t
⊢ IsRatStieltjesPoint f a ↔
    ((Monotone (f a) ∧ Tendsto (f a) atTop (𝓝 1)) ∧ Tendsto (f a) atBot (𝓝 0)) ∧
      ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t
have h₁ : ∀
  (h :
    ((Monotone (f a) ∧ Tendsto (f a) atTop (𝓝 1)) ∧ Tendsto (f a) atBot (𝓝 0)) ∧
      ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t),
  IsRatStieltjesPoint f a
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
⊢ Monotone (if p a then f a else g a)
have pos : ∀ (h : p a), Monotone (f a)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
pos : ∀ (h : p a), Monotone (f a)
⊢ Monotone (if p a then f a else g a)
have neg : ∀ (h : ¬p a), Monotone (g a)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
⊢ Tendsto (if p a then f a else g a) atTop (𝓝 1)
have pos : ∀ (h : p a), Tendsto (f a) atTop (𝓝 1)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
pos : ∀ (h : p a), Tendsto (f a) atTop (𝓝 1)
⊢ Tendsto (if p a then f a else g a) atTop (𝓝 1)
have neg : ∀ (h : ¬p a), Tendsto (g a) atTop (𝓝 1)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
⊢ Tendsto (if p a then f a else g a) atBot (𝓝 0)
have pos : ∀ (h : p a), Tendsto (f a) atBot (𝓝 0)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
pos : ∀ (h : p a), Tendsto (f a) atBot (𝓝 0)
⊢ Tendsto (if p a then f a else g a) atBot (𝓝 0)
have neg : ∀ (h : ¬p a), Tendsto (g a) atBot (𝓝 0)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
⊢ ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), (if p a then f a else g a) (↑r : ℚ) = (if p a then f a else g a) t
have pos : ∀ (h : p a) (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
pos : ∀ (h : p a) (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), f a (↑r : ℚ) = f a t
⊢ ∀ (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), (if p a then f a else g a) (↑r : ℚ) = (if p a then f a else g a) t
have neg : ∀ (h : ¬p a) (t : ℚ), ⨅ (r : (↑(Ioi t) : Type)), g a (↑r : ℚ) = g a t
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
x y : ℚ
hxy : x ≤ y
⊢ LE.le (α := ℝ) (if x < 0 then 0 else 1) (if y < 0 then 0 else 1)
have pos : ∀ (h_1 : x < 0) (h_2 : y < 0), LE.le (α := ℝ) 0 0
Tactic: split_ifs with h_1 h_2 h_2
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
x y : ℚ
hxy : x ≤ y
pos : ∀ (h_1 : x < 0) (h_2 : y < 0), LE.le (α := ℝ) 0 0
⊢ LE.le (α := ℝ) (if x < 0 then 0 else 1) (if y < 0 then 0 else 1)
have neg : ∀ (h_1 : x < 0) (h_2 : ¬y < 0), LE.le (α := ℝ) 0 1
Tactic: split_ifs with h_1 h_2 h_2
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
⊢ LE.le (α := ℝ) (if x < 0 then 0 else 1) (if y < 0 then 0 else 1)
have pos₁ : ∀ (h_1 : ¬x < 0) (h_2 : y < 0), LE.le (α := ℝ) 1 0
Tactic: split_ifs with h_1 h_2 h_2
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
⊢ LE.le (α := ℝ) (if x < 0 then 0 else 1) (if y < 0 then 0 else 1)
have neg₁ : ∀ (h_1 : ¬x < 0) (h_2 : ¬y < 0), LE.le (α := ℝ) 1 1
Tactic: split_ifs with h_1 h_2 h_2
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
q : ℚ
⊢ LE.le (α := ℝ) 0 (if q < 0 then 0 else 1)
have pos : q < 0 → LE.le (α := ℝ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
q : ℚ
pos : q < 0 → LE.le (α := ℝ) 0 0
⊢ LE.le (α := ℝ) 0 (if q < 0 then 0 else 1)
have neg : ¬q < 0 → LE.le (α := ℝ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
q : ℚ
⊢ LE.le (α := ℝ) (if q < 0 then 0 else 1) 1
have pos : q < 0 → LE.le (α := ℝ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
q : ℚ
pos : q < 0 → LE.le (α := ℝ) 0 1
⊢ LE.le (α := ℝ) (if q < 0 then 0 else 1) 1
have neg : ¬q < 0 → LE.le (α := ℝ) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
⊢ Tendsto defaultRatCDF atTop (𝓝 1)
have refine : (fun (x : ℚ) ↦ 1) =ᶠ[atTop] defaultRatCDF
Tactic: refine (tendsto_congr' ?_).mp tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
⊢ (fun (x : ℚ) ↦ 1) =ᶠ[atTop] defaultRatCDF
have rw : ∃ (a : ℚ), ∀ b ≥ a, 1 = defaultRatCDF b
Tactic: rw [EventuallyEq, eventually_atTop]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
⊢ Tendsto defaultRatCDF atBot (𝓝 0)
have refine : (fun (x : ℚ) ↦ 0) =ᶠ[atBot] defaultRatCDF
Tactic: refine (tendsto_congr' ?_).mp tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
⊢ (fun (x : ℚ) ↦ 0) =ᶠ[atBot] defaultRatCDF
have rw : ∃ (a : ℚ), ∀ b ≤ a, 0 = defaultRatCDF b
Tactic: rw [EventuallyEq, eventually_atBot]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
⊢ ∃ (a : ℚ), ∀ b ≤ a, 0 = defaultRatCDF b
have refine : ∀ (q : ℚ) (hq : q ≤ -1), LT.lt (α := ℚ) (-1) 0
Tactic: refine ⟨-1, fun q hq => (if_pos (hq.trans_lt ?_)).symm⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
q : ℚ
hq : q ≤ -1
⊢ LT.lt (α := ℚ) (-1) 0
have linarith : LE.le (α := ℚ) 0 (-1) → -1 + HSub.hSub (α := ℚ) 0 (-1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
t : ℚ
⊢ BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
have refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1) x),
  0 ≤ x
Tactic: refine ⟨0, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
t : ℚ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1) x
⊢ 0 ≤ x
have 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)
Tactic: obtain ⟨y, rfl⟩ := mem_range.mpr hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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)
⊢ LE.le (α := ℝ) 0 (if (↑y : ℚ) < 0 then 0 else 1)
have pos : (↑y : ℚ) < 0 → LE.le (α := ℝ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
⊢ LE.le (α := ℝ) 0 (if (↑y : ℚ) < 0 then 0 else 1)
have neg : ¬(↑y : ℚ) < 0 → LE.le (α := ℝ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (hypothesis)
Goal:
t : ℚ
⊢ Eq (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) (if t < 0 then 0 else 1)
have h_bdd : 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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
⊢ Eq (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) (if t < 0 then 0 else 1)
have pos : ∀ (h : t < 0), Eq (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
⊢ Eq (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) (if t < 0 then 0 else 1)
have neg : ∀ (h : ¬t < 0), Eq (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
have pos : LE.le (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 0
Tactic: refine le_antisymm ?_ (le_ciInf fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
⊢ Eq (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 0
have pos₁ : ∀ (x : (↑(Ioi t) : Type)), LE.le (α := ℝ) 0 (if (↑x : ℚ) < 0 then 0 else 1)
Tactic: refine le_antisymm ?_ (le_ciInf fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : t < 0
⊢ t < t / 2
have linarith : t / 2 ≤ t → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
⊢ t < t / 2
have linarith₁ : t / 2 ≤ t → HMul.hMul (α := ℚ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
⊢ t < t / 2
have linarith₂ : t / 2 ≤ t → GT.gt (α := ℚ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
⊢ t < t / 2
have linarith₃ : t / 2 ≤ t → t - 0 + (1 * t - 2 * t) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
t : ℚ
h_bdd : BddBelow (α := ℝ) (range fun (r : (↑(Ioi t) : Type)) ↦ if (↑r : ℚ) < 0 then 0 else 1)
h : t < 0
⊢ t / 2 < 0
have linarith : 0 ≤ t / 2 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
⊢ t / 2 < 0
have linarith₁ : 0 ≤ t / 2 → HMul.hMul (α := ℚ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
⊢ t / 2 < 0
have linarith₂ : 0 ≤ t / 2 → GT.gt (α := ℚ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
⊢ t / 2 < 0
have linarith₃ : 0 ≤ t / 2 → t - 0 + (HMul.hMul (α := ℚ) 2 0 - 1 * t) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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) 0
have pos : ∀ (q : ℚ) (htq : t < q) (hq_neg : q < 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⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
have pos : LE.le (α := ℝ) (if (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) q htq) : ℚ) < 0 then 0 else 1) 0
Tactic: refine (ciInf_le h_bdd ⟨q, htq⟩).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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 (α := ℝ) (if (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) q htq) : ℚ) < 0 then 0 else 1) 0
have pos : (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) q htq) : ℚ) < 0
Tactic: rw [if_pos]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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)
⊢ LE.le (α := ℝ) 0 (if (↑x : ℚ) < 0 then 0 else 1)
have pos : (↑x : ℚ) < 0 → LE.le (α := ℝ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
⊢ LE.le (α := ℝ) 0 (if (↑x : ℚ) < 0 then 0 else 1)
have neg : ¬(↑x : ℚ) < 0 → LE.le (α := ℝ) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
have neg : LE.le (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 1
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
⊢ Eq (α := ℝ) (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1) 1
have neg₁ : LE.le (α := ℝ) 1 (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1)
Tactic: refine le_antisymm ?_ ?_