awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
⊢ Eq (α := ℝ≥0∞) ((Measure.map (f a) volume : (a : Set (↑I : Type)) → ℝ≥0∞) (Iic x) : ℝ≥0∞)
    ((((κ : (a : X) → Measure (↑I : Type)) a : Measure (↑I : Type)) : (a : Set (↑I : Type)) → ℝ≥0∞) (Iic x) : ℝ≥0∞)
have simp_rw : Eq (α := ℝ≥0∞) ((volume : (a : Set (↑I : Type)) → ℝ≥0∞) {x_1 : (↑I : Type) | f a x_1 ≤ x} : ℝ≥0∞)
  ((volume : (a : Set (↑I : Type)) → ℝ≥0∞)
      (Iic
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
          (Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) a) (Icc 0 x))
          κ_in_I)) :
    ℝ≥0∞)
Tactic: simp_rw [volume.map_apply measurable_f.of_uncurry_left measurableSet_Iic, preimage,
    mem_Iic, Iic_to_Icc, ← ofReal_measureReal (measure_ne_top (κ a) _), ← volume_Iic ⟨_, κ_in_I⟩]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set (↑I : Type)) → ℝ≥0∞) {x_1 : (↑I : Type) | f a x_1 ≤ x} : ℝ≥0∞)
    ((volume : (a : Set (↑I : Type)) → ℝ≥0∞)
        (Iic
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
            (Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
              ((κ : (a : X) → Measure (↑I : Type)) a) (Icc 0 x))
            κ_in_I)) :
      ℝ≥0∞)
have h : ∀ (ξ : (↑I : Type)),
  f a ξ ≤ x ↔
    ξ ≤
      Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
        (Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
          ((κ : (a : X) → Measure (↑I : Type)) a) (Icc 0 x))
        κ_in_I
Tactic: congr with ξ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
⊢ f a ξ ≤ x ↔
    ξ ≤
      Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
        (Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
          ((κ : (a : X) → Measure (↑I : Type)) a) (Icc 0 x))
        κ_in_I
have h : f a ξ ≤ x →
  ξ ≤
    Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
      (Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
        ((κ : (a : X) → Measure (↑I : Type)) a) (Icc 0 x))
      κ_in_I
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
h :
  f a ξ ≤ x →
    ξ ≤
      Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
        (Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
          ((κ : (a : X) → Measure (↑I : Type)) a) (Icc 0 x))
        κ_in_I
⊢ f a ξ ≤ x ↔
    ξ ≤
      Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
        (Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
          ((κ : (a : X) → Measure (↑I : Type)) a) (Icc 0 x))
        κ_in_I
have h₁ : ξ ≤
    Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
      (Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
        ((κ : (a : X) → Measure (↑I : Type)) a) (Icc 0 x))
      κ_in_I →
  f a ξ ≤ x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ : f a ξ ≤ x
⊢ ξ ≤
    Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I)
      (Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
        ((κ : (a : X) → Measure (↑I : Type)) a) (Icc 0 x))
      κ_in_I
have h : (↑ξ : ℝ) ≤
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
    (Icc 0 x)
Tactic: change ξ ≤ (κ a).real (Icc 0 x)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ : f a ξ ≤ x
⊢ (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)
have pos : ∀ (hx : x = 1),
  (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)
Tactic: by_cases hx : x = 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ : f a ξ ≤ x
pos :
  ∀ (hx : x = 1),
    (↑ξ : ℝ) ≤
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
        (Icc 0 x)
⊢ (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)
have neg : ∀ (hx : ¬x = 1),
  (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)
Tactic: by_cases hx : x = 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ : f a ξ ≤ x
hx : ¬x = 1
g : (y : (↑I : Type)) → ℝ :=
  fun (y : (↑I : Type)) ↦
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 y)
⊢ (𝓝[>] x).NeBot
have refine : ∃ (b : (↑I : Type)), x < b
Tactic: refine nhdsGT_neBot_of_exists_gt ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ : f a ξ ≤ x
hx : ¬x = 1
g : (y : (↑I : Type)) → ℝ :=
  fun (y : (↑I : Type)) ↦
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 y)
⊢ ∃ (b : (↑I : Type)), x < b
have h : x < 1
Tactic: use 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ : f a ξ ≤ x
hx : ¬x = 1
g : (y : (↑I : Type)) → ℝ :=
  fun (y : (↑I : Type)) ↦
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 y)
nebot : (𝓝[>] x).NeBot := ⋯
⊢ (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)
have neg : Tendsto g (𝓝[>] x)
  (𝓝
    (Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)))
Tactic: refine le_of_tendsto_of_tendsto (b := 𝓝[>] x) (g := g) continuousWithinAt_const ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ : f a ξ ≤ x
hx : ¬x = 1
g : (y : (↑I : Type)) → ℝ :=
  fun (y : (↑I : Type)) ↦
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 y)
nebot : (𝓝[>] x).NeBot := ⋯
neg :
  Tendsto g (𝓝[>] x)
    (𝓝
      (Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
        ((κ : (a : X) → Measure (↑I : Type)) a) (Icc 0 x)))
⊢ (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)
have neg₁ : (fun (x : (↑I : Type)) ↦ (↑ξ : ℝ)) ≤ᶠ[𝓝[>] x] g
Tactic: refine le_of_tendsto_of_tendsto (b := 𝓝[>] x) (g := g) continuousWithinAt_const ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ : f a ξ ≤ x
hx : ¬x = 1
g : (y : (↑I : Type)) → ℝ :=
  fun (y : (↑I : Type)) ↦
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 y)
nebot : (𝓝[>] x).NeBot := ⋯
h : StieltjesFunction ℝ :=
  cdf
    (Measure.map (α := { x : ℝ // x ∈ I }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I))
      ((κ : (a : X) → Measure (↑I : Type)) a))
⊢ Tendsto g (𝓝[>] x)
    (𝓝
      (Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
        ((κ : (a : X) → Measure (↑I : Type)) a) (Icc 0 x)))
have h_continuousWithinAt : ContinuousWithinAt (↑h : ℝ → ℝ) (Ioi (↑x : ℝ)) (↑x : ℝ)
Tactic: have h_continuousWithinAt := continuousWithinAt_Ioi_iff_Ici.mpr (h.right_continuous x)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ : f a ξ ≤ x
hx : ¬x = 1
g : (y : (↑I : Type)) → ℝ :=
  fun (y : (↑I : Type)) ↦
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 y)
nebot : (𝓝[>] x).NeBot := ⋯
h : StieltjesFunction ℝ :=
  cdf
    (Measure.map (α := { x : ℝ // x ∈ I }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I))
      ((κ : (a : X) → Measure (↑I : Type)) a))
h_continuousWithinAt : ContinuousWithinAt (↑h : ℝ → ℝ) (Ioi (↑x : ℝ)) (↑x : ℝ)
⊢ Tendsto g (𝓝[>] x)
    (𝓝
      (Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
        ((κ : (a : X) → Measure (↑I : Type)) a) (Icc 0 x)))
have neg : Tendsto
  (fun (y : (↑I : Type)) ↦
    (↑(cdf
            (Measure.map (α := { x : ℝ // x ∈ I }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I))
              ((κ : (a : X) → Measure (↑I : Type)) a))) :
        ℝ → ℝ)
      (↑y : ℝ))
  (𝓝[>] x)
  (𝓝
    ((↑(cdf
            (Measure.map (α := { x : ℝ // x ∈ I }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I))
              ((κ : (a : X) → Measure (↑I : Type)) a))) :
        ℝ → ℝ)
      (↑x : ℝ)))
Tactic: simp_rw [g, ← unitInterval.cdf_eq_real (κ a)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ : f a ξ ≤ x
hx : ¬x = 1
g : (y : (↑I : Type)) → ℝ :=
  fun (y : (↑I : Type)) ↦
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 y)
nebot : (𝓝[>] x).NeBot := ⋯
⊢ (fun (x : (↑I : Type)) ↦ (↑ξ : ℝ)) ≤ᶠ[𝓝[>] x] g
have neg : ∀ (y : (↑I : Type)) (hy : y ∈ Ioi x), (fun (x : (↑I : Type)) ↦ (↑ξ : ℝ)) y ≤ g y
Tactic: refine eventually_nhdsWithin_of_forall fun y hy ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ : f a ξ ≤ x
hx : ¬x = 1
g : (y : (↑I : Type)) → ℝ :=
  fun (y : (↑I : Type)) ↦
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 y)
nebot : (𝓝[>] x).NeBot := ⋯
y : (↑I : Type)
hy : y ∈ Ioi x
⊢ (fun (x : (↑I : Type)) ↦ (↑ξ : ℝ)) y ≤ g y
have neg : ∀ (h : g y < (↑ξ : ℝ)), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ : f a ξ ≤ x
hx : ¬x = 1
g : (y : (↑I : Type)) → ℝ :=
  fun (y : (↑I : Type)) ↦
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 y)
nebot : (𝓝[>] x).NeBot := ⋯
y : (↑I : Type)
hy : y ∈ Ioi x
h : g y < (↑ξ : ℝ)
⊢ False
have hξ₁ : ∀ (b : (↑I : Type)),
  Membership.mem (γ := Set (↑I : Type))
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) a) (Icc 0 x) <
          (↑ξ : ℝ)}
      b →
    b ≤ x
Tactic: simp only [sSup_le_iff, f] at hξ
Cleared hypotheses: hξ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (hypothesis)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hx : ¬x = 1
g : (y : (↑I : Type)) → ℝ :=
  fun (y : (↑I : Type)) ↦
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 y)
nebot : (𝓝[>] x).NeBot := ⋯
y : (↑I : Type)
hy : y ∈ Ioi x
h : g y < (↑ξ : ℝ)
hξ :
  ∀ (b : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type))
        {x : (↑I : Type) |
          Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
              ((κ : (a : X) → Measure (↑I : Type)) a) (Icc 0 x) <
            (↑ξ : ℝ)}
        b →
      b ≤ x
⊢ False
have hξ₁ : y ≤ x
Tactic: specialize hξ y h
Cleared hypotheses: hξ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ :
  (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)
⊢ f a ξ ≤ x
have h : ∀ (b : (↑I : Type)),
  Membership.mem (γ := Set (↑I : Type))
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) a) (Icc 0 x) <
          (↑ξ : ℝ)}
      b →
    b ≤ x
Tactic: simp only [sSup_le_iff, f]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Representation (goal)
Goal:
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X (↑I : Type)
inst : IsMarkovKernel κ
f : (s : X) → (t : (↑I : Type)) → (↑I : Type) :=
  fun (s : X) (t : (↑I : Type)) ↦
    sSup
      {x : (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) s) (Icc 0 x) <
          (↑t : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ :
  (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)
c : (↑I : Type)
hc :
  Membership.mem (γ := Set (↑I : Type))
    {x : (↑I : Type) |
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
          (Icc 0 x) <
        (↑ξ : ℝ)}
    c
⊢ c ≤ x
have h : ∀ (h : x < c), False
Tactic: by_contra! h