awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) 1
have neg : LE.le (α := ℝ) (if (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) (t + 1) sorry) : ℚ) < 0 then 0 else 1) 1
Tactic: refine (ciInf_le h_bdd ⟨t + 1, lt_add_one t⟩).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
⊢ LE.le (α := ℝ) (if (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) (t + 1) ⋯) : ℚ) < 0 then 0 else 1) 1
have pos : (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) (t + 1) sorry) : ℚ) < 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
pos : (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) (t + 1) ⋯) : ℚ) < 0 → LE.le (α := ℝ) 0 1
⊢ LE.le (α := ℝ) (if (↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) (t + 1) ⋯) : ℚ) < 0 then 0 else 1) 1
have neg : ¬(↑(Subtype.mk (p := fun (x : ℚ) ↦ x ∈ Ioi t) (t + 1) sorry) : ℚ) < 0 → LE.le (α := ℝ) 1 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
⊢ LE.le (α := ℝ) 1 (⨅ (r : (↑(Ioi t) : Type)), if (↑r : ℚ) < 0 then 0 else 1)
have neg : ∀ (x : (↑(Ioi t) : Type)), LE.le (α := ℝ) 1 (if (↑x : ℚ) < 0 then 0 else 1)
Tactic: refine 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
x : (↑(Ioi t) : Type)
⊢ LE.le (α := ℝ) 1 (if (↑x : ℚ) < 0 then 0 else 1)
have neg : ¬(↑x : ℚ) < 0
Tactic: rw [if_neg]
-- 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)
⊢ ¬(↑x : ℚ) < 0
have neg : ∀ (h : 0 ≤ t) (x : (↑(Ioi t) : Type)), 0 ≤ (↑x : ℚ)
Tactic: rw [not_lt] at h ⊢
Cleared hypotheses: h, x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
a : α
h : IsRatStieltjesPoint f a
q : ℚ
⊢ toRatCDF f a q = f a q
have rw : (if IsRatStieltjesPoint f a then f a else defaultRatCDF) q = f a q
Tactic: rw [toRatCDF, if_pos h]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
⊢ toRatCDF f a q = f a q
have rw₁ : f a q = f a q
Tactic: rw [toRatCDF, if_pos h]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ (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
have rw : (if IsRatStieltjesPoint f 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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ stieltjesFunctionAux f a = fun (t : ℝ) ↦ ⨅ (r : { r' : ℚ // t < (↑r' : ℝ) }), f a (↑r : ℚ)
have h : ∀ (t : ℝ), stieltjesFunctionAux f a t = ⨅ (r : { r' : ℚ // t < (↑r' : ℝ) }), f a (↑r : ℚ)
Tactic: ext t
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
⊢ stieltjesFunctionAux f a (↑r : ℝ) = f a r
have rw : Eq (α := ℝ) (⨅ (q : { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) }), f a (↑q : ℚ))
  (⨅ (r_1 : (↑(Ioi r) : Type)), f a (↑r_1 : ℚ))
Tactic: rw [← hf.iInf_rat_gt_eq a r, IsMeasurableRatCDF.stieltjesFunctionAux]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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 : ℚ))
have refine_1 : { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) } ≃ (↑(Ioi r) : Type)
Tactic: refine Equiv.iInf_congr ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℚ
refine_1 : { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) } ≃ (↑(Ioi r) : Type)
⊢ Eq (α := ℝ) (⨅ (q : { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) }), f a (↑q : ℚ))
    (⨅ (r_1 : (↑(Ioi r) : Type)), f a (↑r_1 : ℚ))
have 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 : ℚ) sorry,
                invFun := fun (t : (↑(Ioi r) : Type)) ↦
                  Subtype.mk (p := fun (q' : ℚ) ↦ LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ)) (↑t : ℚ) sorry,
                left_inv := sorry, right_inv := sorry : { q' : ℚ // LT.lt (α := ℝ) (↑r : ℝ) (↑q' : ℝ) } ≃ (↑(Ioi r) : Type) } :
              (a : { q' : ℚ // (↑r : ℝ) < (↑q' : ℝ) }) → (↑(Ioi r) : Type))
            x) :
        ℚ) =
    f a (↑x : ℚ)
Tactic: refine Equiv.iInf_congr ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
⊢ Nonempty { r' : ℚ // r < (↑r' : ℝ) }
have obtain : ∀ (r_1 : ℚ) (hrx : r < (↑r_1 : ℝ)), Nonempty { r' : ℚ // r < (↑r' : ℝ) }
Tactic: obtain ⟨r, hrx⟩ := exists_rat_gt r
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (hypothesis)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
⊢ 0 ≤ stieltjesFunctionAux f a r
have this : Nonempty { r' : ℚ // r < (↑r' : ℝ) }
Tactic: have : Nonempty { r' : ℚ // r < ↑r' } := by
    obtain ⟨r, hrx⟩ := exists_rat_gt r
    exact ⟨⟨r, hrx⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
r : ℝ
this : Nonempty { r' : ℚ // r < (↑r' : ℝ) }
⊢ 0 ≤ stieltjesFunctionAux f a r
have rw : LE.le (α := ℝ) 0 (⨅ (q : { q' : ℚ // r < (↑q' : ℝ) }), f a (↑q : ℚ))
Tactic: rw [IsMeasurableRatCDF.stieltjesFunctionAux_def]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
⊢ Nonempty { r' : ℚ // y < (↑r' : ℝ) }
have obtain : ∀ (r : ℚ) (hrx : y < (↑r : ℝ)), Nonempty { r' : ℚ // y < (↑r' : ℝ) }
Tactic: obtain ⟨r, hrx⟩ := exists_rat_gt y
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (hypothesis)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
⊢ stieltjesFunctionAux f a x ≤ stieltjesFunctionAux f a y
have this : Nonempty { r' : ℚ // y < (↑r' : ℝ) }
Tactic: have : Nonempty { r' : ℚ // y < ↑r' } := by
    obtain ⟨r, hrx⟩ := exists_rat_gt y
    exact ⟨⟨r, hrx⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
this : Nonempty { r' : ℚ // y < (↑r' : ℝ) }
⊢ stieltjesFunctionAux f a x ≤ stieltjesFunctionAux f a y
have simp_rw : LE.le (α := ℝ) (⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f a (↑q : ℚ)) (⨅ (q : { q' : ℚ // y < (↑q' : ℝ) }), f a (↑q : ℚ))
Tactic: simp_rw [IsMeasurableRatCDF.stieltjesFunctionAux_def]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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 : ℚ))
have refine_1 : ∀ (r : { q' : ℚ // y < (↑q' : ℝ) }), BddBelow (α := ℝ) (range fun (q : { q' : ℚ // x < (↑q' : ℝ) }) ↦ f a (↑q : ℚ))
Tactic: refine le_ciInf fun r ↦ (ciInf_le ?_ ?_).trans_eq ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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 : ℚ))
⊢ LE.le (α := ℝ) (⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f a (↑q : ℚ)) (⨅ (q : { q' : ℚ // y < (↑q' : ℝ) }), f a (↑q : ℚ))
have refine_2 : (r : { q' : ℚ // y < (↑q' : ℝ) }) → { q' : ℚ // x < (↑q' : ℝ) }
Tactic: refine le_ciInf fun r ↦ (ciInf_le ?_ ?_).trans_eq ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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' : ℝ) }
⊢ LE.le (α := ℝ) (⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f a (↑q : ℚ)) (⨅ (q : { q' : ℚ // y < (↑q' : ℝ) }), f a (↑q : ℚ))
have refine_3 : ∀ (r : { q' : ℚ // y < (↑q' : ℝ) }),
  f a (↑(Subtype.mk (p := fun (q' : ℚ) ↦ x < (↑q' : ℝ)) (↑r : ℚ) sorry) : ℚ) = f a (↑r : ℚ)
Tactic: refine le_ciInf fun r ↦ (ciInf_le ?_ ?_).trans_eq ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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 : ℚ))
have refine_1 : ∀ (z : ℝ), Membership.mem (γ := Set ℝ) (range fun (q : { q' : ℚ // x < (↑q' : ℝ) }) ↦ f a (↑q : ℚ)) z → 0 ≤ z
Tactic: refine ⟨0, fun z ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ ContinuousWithinAt (stieltjesFunctionAux f a) (Ici x) x
have rw : ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x
Tactic: rw [← continuousWithinAt_Ioi_iff_Ici]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x
have a₁ : ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x ↔
  Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (sInf (stieltjesFunctionAux f a '' Ioi x)))
Tactic: convert! Monotone.tendsto_nhdsGT (monotone_stieltjesFunctionAux hf a) x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x ↔
    Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (sInf (stieltjesFunctionAux f a '' Ioi x)))
have a₁ : ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x ↔
  Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (⨅ (a_1 : (↑(Ioi x) : Type)), stieltjesFunctionAux f a (↑a_1 : ℝ)))
Tactic: rw [sInf_image']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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 : ℚ) : ℝ))
have refine : BddBelow (stieltjesFunctionAux f a '' Ioi x)
Tactic: refine Real.iInf_Ioi_eq_iInf_rat_gt x ?_ (monotone_stieltjesFunctionAux hf a)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ BddBelow (stieltjesFunctionAux f a '' Ioi x)
have refine : ∀ z ∈ stieltjesFunctionAux f a '' Ioi x, 0 ≤ z
Tactic: refine ⟨0, fun z ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (hypothesis)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x ↔
    Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (⨅ (a_1 : (↑(Ioi x) : Type)), stieltjesFunctionAux f a (↑a_1 : ℝ)))
have h' : 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
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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 : ℚ))
have e_s : ∀ (r : { r' : ℚ // x < (↑r' : ℝ) }), stieltjesFunctionAux f a (↑(↑r : ℚ) : ℝ) = f a (↑r : ℚ)
Tactic: congr with r
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (hypothesis)
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 : ℚ) : ℝ))
⊢ ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x ↔
    Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (⨅ (a_1 : (↑(Ioi x) : Type)), stieltjesFunctionAux f a (↑a_1 : ℝ)))
have h'' : 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
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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 : ℚ))
⊢ ContinuousWithinAt (stieltjesFunctionAux f a) (Ioi x) x ↔
    Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (⨅ (a_1 : (↑(Ioi x) : Type)), stieltjesFunctionAux f a (↑a_1 : ℝ)))
have a₁ : Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (stieltjesFunctionAux f a x)) ↔
  Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)))
Tactic: rw [h', h'', ContinuousWithinAt]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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 : ℚ))
⊢ Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (stieltjesFunctionAux f a x)) ↔
    Tendsto (stieltjesFunctionAux f a) (𝓝[>] x) (𝓝 (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)))
have a₁ : stieltjesFunctionAux f a x = ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)
Tactic: congr!
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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 : ℚ))
⊢ stieltjesFunctionAux f a x = ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)
have a₁ : Eq (α := ℝ) (⨅ (q : { q' : ℚ // x < (↑q' : ℝ) }), f a (↑q : ℚ)) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ))
Tactic: rw [stieltjesFunctionAux_def]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x ≤ 1
have obtain : ∀ (r : ℚ) (hrx : x < (↑r : ℝ)), (↑(hf.stieltjesFunction a) : ℝ → ℝ) x ≤ 1
Tactic: obtain ⟨r, hrx⟩ := exists_rat_gt x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < (↑r : ℝ)
⊢ (↑(hf.stieltjesFunction a) : ℝ → ℝ) x ≤ 1
have rw : LE.le (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ)) 1
Tactic: rw [← StieltjesFunction.iInf_rat_gt_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < (↑r : ℝ)
⊢ LE.le (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), (↑(hf.stieltjesFunction a) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ)) 1
have simp_rw : LE.le (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)) 1
Tactic: simp_rw [IsMeasurableRatCDF.stieltjesFunction_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
have refine_1 : BddBelow (α := ℝ) (range fun (r : { r' : ℚ // x < (↑r' : ℝ) }) ↦ f a (↑r : ℚ))
Tactic: refine ciInf_le_of_le ?_ ?_ (hf.le_one _ _)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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 : ℚ))
⊢ LE.le (α := ℝ) (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }), f a (↑r : ℚ)) 1
have refine_2 : { r' : ℚ // x < (↑r' : ℝ) }
Tactic: refine ciInf_le_of_le ?_ ?_ (hf.le_one _ _)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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 : ℚ))
have refine_1 : ∀ (z : ℝ), Membership.mem (γ := Set ℝ) (range fun (r : { r' : ℚ // x < (↑r' : ℝ) }) ↦ f a (↑r : ℚ)) z → 0 ≤ z
Tactic: refine ⟨0, fun z ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (hypothesis)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ Tendsto (↑(hf.stieltjesFunction a) : ℝ → ℝ) atBot (𝓝 0)
have h_exists : ∀ (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)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
have rw : ∀ (b : ℚ), ∃ (i : ℝ), ∀ a ≤ i, qs a ≤ b
Tactic: rw [tendsto_atBot_atBot]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
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
have refine : ∀ (q : ℚ) (y : ℝ) (hy : y ≤ HSub.hSub (α := ℝ) (↑q : ℝ) 1), qs y ≤ q
Tactic: refine fun q ↦ ⟨q - 1, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (hypothesis)
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 ≤ q
have h_le : (↑(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)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (hypothesis)
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
⊢ qs y ≤ q
have h_le₁ : LE.le (α := ℝ) (↑(qs y) : ℝ) (↑q : ℝ)
Tactic: rw [sub_add_cancel] at h_le
Cleared hypotheses: h_le
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (hypothesis)
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 (↑(hf.stieltjesFunction a) : ℝ → ℝ) atBot (𝓝 0)
have hqs_tendsto : 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