awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Representation
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
h :
  (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 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:
change ξ ≤ (κ a).real (Icc 0 x)

Premises used: MeasureTheory.Measure.real, Set.Icc, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Representation
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)
neg :
  ∀ (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)

Tactic:
by_cases hx : x = 1
-- Module: Mathlib.Probability.Kernel.Representation
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
⊢ (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)

Tactic:
simp [hx, ← univ_eq_Icc, ξ.2.2]

Premises used: And.right, unitInterval.univ_eq_Icc, Subtype.property
-- Module: Mathlib.Probability.Kernel.Representation
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

Tactic:
nhdsGT_neBot_of_exists_gt ?_

Premises used: nhdsGT_neBot_of_exists_gt
-- Module: Mathlib.Probability.Kernel.Representation
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)
refine : ∃ (b : (↑I : Type)), x < b
⊢ (𝓝[>] x).NeBot

Tactic:
refine nhdsGT_neBot_of_exists_gt ?_

Premises used: nhdsGT_neBot_of_exists_gt
-- Module: Mathlib.Probability.Kernel.Representation
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)
h : x < 1
⊢ ∃ (b : (↑I : Type)), x < b

Tactic:
use 1
-- Module: Mathlib.Probability.Kernel.Representation
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 < 1

Tactic:
lt_of_le_of_ne x.2.2 hx

Premises used: And.right, lt_of_le_of_ne, Subtype.property
-- Module: Mathlib.Probability.Kernel.Representation
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 < 1

Tactic:
exact lt_of_le_of_ne x.2.2 hx
-- Module: Mathlib.Probability.Kernel.Representation
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)

Tactic:
le_of_tendsto_of_tendsto (b := 𝓝[>] x) (g := g) continuousWithinAt_const ?_ ?_

Premises used: continuousWithinAt_const, le_of_tendsto_of_tendsto
-- Module: Mathlib.Probability.Kernel.Representation
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)))
neg₁ : (fun (x : (↑I : Type)) ↦ (↑ξ : ℝ)) ≤ᶠ[𝓝[>] x] g
⊢ (↑ξ : ℝ) ≤
    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 ?_ ?_

Premises used: continuousWithinAt_const, le_of_tendsto_of_tendsto
-- Module: Mathlib.Probability.Kernel.Representation
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))
⊢ ContinuousWithinAt (↑h : ℝ → ℝ) (Ioi (↑x : ℝ)) (↑x : ℝ)

Tactic:
have h_continuousWithinAt := continuousWithinAt_Ioi_iff_Ici.mpr (h.right_continuous x)
-- Module: Mathlib.Probability.Kernel.Representation
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 : ℝ)
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 : ℝ)))
⊢ Tendsto g (𝓝[>] x)
    (𝓝
      (Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
        ((κ : (a : X) → Measure (↑I : Type)) a) (Icc 0 x)))

Tactic:
simp_rw [g, ← unitInterval.cdf_eq_real (κ a)]

Premises used: ProbabilityTheory.unitInterval.cdf_eq_real, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Representation
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 : ℝ)
⊢ Continuous (X := (↑I : Type)) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Representation
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
    (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:
exact h_continuousWithinAt.comp (Continuous.continuousWithinAt (by fun_prop)) (fun y hy ↦ hy)

Premises used: ContinuousWithinAt.comp, Continuous.continuousWithinAt
-- Module: Mathlib.Probability.Kernel.Representation
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

Tactic:
eventually_nhdsWithin_of_forall fun y hy ↦ ?_

Premises used: Filter.EventuallyLE, eventually_nhdsWithin_of_forall
-- Module: Mathlib.Probability.Kernel.Representation
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 : ∀ (y : (↑I : Type)) (hy : y ∈ Ioi x), (fun (x : (↑I : Type)) ↦ (↑ξ : ℝ)) y ≤ g y
⊢ (fun (x : (↑I : Type)) ↦ (↑ξ : ℝ)) ≤ᶠ[𝓝[>] x] g

Tactic:
refine eventually_nhdsWithin_of_forall fun y hy ↦ ?_

Premises used: eventually_nhdsWithin_of_forall
-- Module: Mathlib.Probability.Kernel.Representation
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
neg : ∀ (h : g y < (↑ξ : ℝ)), False
⊢ (fun (x : (↑I : Type)) ↦ (↑ξ : ℝ)) y ≤ g y

Tactic:
by_contra! h
-- Module: Mathlib.Probability.Kernel.Representation
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 < (↑ξ : ℝ)
⊢ ∀ (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ξ

Premises used: sSup_le_iff
-- Module: Mathlib.Probability.Kernel.Representation
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
⊢ y ≤ x

Tactic:
specialize hξ y h
-- Module: Mathlib.Probability.Kernel.Representation
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ξ : y ≤ x
⊢ False

Tactic:
grind