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 : ℝ)}
a : (↑I : Type)
h_monotone :
  ∀ (s : X),
    Monotone (β := ℝ) fun (x : (↑I : Type)) ↦
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) s)
        (Icc 0 x)
e : X × (↑I : Type)
h :
  (∃ (a_1 : ℝ) (h : 0 ≤ a_1 ∧ a_1 ≤ 1),
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_1 ⋯)) <
          (↑e.2 : ℝ) ∧
        a < Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_1 ⋯) →
    ∃ (i : ℚ),
      (↑a : ℝ) < (↑i : ℝ) ∧
        ∃ (x : 0 ≤ i ∧ LE.le (α := ℝ) (↑i : ℝ) 1),
          Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
              ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑i : ℝ) ⋯)) <
            (↑e.2 : ℝ)
⊢ (∃ (a_1 : ℝ) (h : 0 ≤ a_1 ∧ a_1 ≤ 1),
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_1 ⋯)) <
          (↑e.2 : ℝ) ∧
        a < Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_1 ⋯) ↔
    ∃ (i : ℚ),
      (↑a : ℝ) < (↑i : ℝ) ∧
        ∃ (x : 0 ≤ i ∧ LE.le (α := ℝ) (↑i : ℝ) 1),
          Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
              ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑i : ℝ) ⋯)) <
            (↑e.2 : ℝ)
have h₁ : (∃ (i : ℚ),
    (↑a : ℝ) < (↑i : ℝ) ∧
      ∃ (x : 0 ≤ i ∧ LE.le (α := ℝ) (↑i : ℝ) 1),
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑i : ℝ) sorry)) <
          (↑e.2 : ℝ)) →
  ∃ (a_2 : ℝ) (h : 0 ≤ a_2 ∧ a_2 ≤ 1),
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) e.1)
          (Icc 0 (Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_2 sorry)) <
        (↑e.2 : ℝ) ∧
      a < Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_2 sorry
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 : ℝ)}
a : (↑I : Type)
h_monotone :
  ∀ (s : X),
    Monotone (β := ℝ) fun (x : (↑I : Type)) ↦
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) s)
        (Icc 0 x)
e : X × (↑I : Type)
y : ℝ
hyI : 0 ≤ y ∧ y ≤ 1
y_mem :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) e.1)
      (Icc 0 (Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) y ⋯)) <
    (↑e.2 : ℝ)
hy : (↑a : ℝ) < y
⊢ ∃ (i : ℚ),
    (↑a : ℝ) < (↑i : ℝ) ∧
      ∃ (x : 0 ≤ i ∧ LE.le (α := ℝ) (↑i : ℝ) 1),
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑i : ℝ) ⋯)) <
          (↑e.2 : ℝ)
have h : ∀ (q : ℚ) (hqa : (↑a : ℝ) < (↑q : ℝ)) (hqy : (↑q : ℝ) < y),
  ∃ (i : ℚ),
    (↑a : ℝ) < (↑i : ℝ) ∧
      ∃ (x : 0 ≤ i ∧ LE.le (α := ℝ) (↑i : ℝ) 1),
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑i : ℝ) sorry)) <
          (↑e.2 : ℝ)
Tactic: obtain ⟨q, hqa, hqy⟩ := exists_rat_btwn 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 : ℝ)}
a : (↑I : Type)
h_monotone :
  ∀ (s : X),
    Monotone (β := ℝ) fun (x : (↑I : Type)) ↦
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) s)
        (Icc 0 x)
e : X × (↑I : Type)
y : ℝ
hyI : 0 ≤ y ∧ y ≤ 1
y_mem :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) e.1)
      (Icc 0 (Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) y ⋯)) <
    (↑e.2 : ℝ)
hy : (↑a : ℝ) < y
q : ℚ
hqa : (↑a : ℝ) < (↑q : ℝ)
hqy : (↑q : ℝ) < y
⊢ ∃ (i : ℚ),
    (↑a : ℝ) < (↑i : ℝ) ∧
      ∃ (x : 0 ≤ i ∧ LE.le (α := ℝ) (↑i : ℝ) 1),
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑i : ℝ) ⋯)) <
          (↑e.2 : ℝ)
have h : 0 ≤ q
Tactic: refine ⟨q, hqa, ⟨?_, hqy.le.trans hyI.2⟩, lt_of_lt_of_le' y_mem (h_monotone e.1 hqy.le)⟩
-- 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 : ℝ)}
a : (↑I : Type)
h_monotone :
  ∀ (s : X),
    Monotone (β := ℝ) fun (x : (↑I : Type)) ↦
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) s)
        (Icc 0 x)
e : X × (↑I : Type)
he :
  ∃ (i : ℚ),
    (↑a : ℝ) < (↑i : ℝ) ∧
      ∃ (x : 0 ≤ i ∧ LE.le (α := ℝ) (↑i : ℝ) 1),
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑i : ℝ) ⋯)) <
          (↑e.2 : ℝ)
⊢ ∃ (a_1 : ℝ) (h : 0 ≤ a_1 ∧ a_1 ≤ 1),
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) e.1)
          (Icc 0 (Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_1 ⋯)) <
        (↑e.2 : ℝ) ∧
      a < Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_1 ⋯
have h : ∀ (q : ℚ) (hqa : (↑a : ℝ) < (↑q : ℝ)) (hqI : 0 ≤ q ∧ LE.le (α := ℝ) (↑q : ℝ) 1)
  (h :
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) e.1)
        (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑q : ℝ) sorry)) <
      (↑e.2 : ℝ)),
  ∃ (a_1 : ℝ) (h : 0 ≤ a_1 ∧ a_1 ≤ 1),
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) e.1)
          (Icc 0 (Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_1 sorry)) <
        (↑e.2 : ℝ) ∧
      a < Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_1 sorry
Tactic: obtain ⟨q, hqa, hqI, h⟩ := he
Cleared hypotheses: he
-- 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 : ℝ)}
a : (↑I : Type)
h_monotone :
  ∀ (s : X),
    Monotone (β := ℝ) fun (x : (↑I : Type)) ↦
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) s)
        (Icc 0 x)
e : X × (↑I : Type)
q : ℚ
hqa : (↑a : ℝ) < (↑q : ℝ)
hqI : 0 ≤ q ∧ LE.le (α := ℝ) (↑q : ℝ) 1
h :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) e.1)
      (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑q : ℝ) ⋯)) <
    (↑e.2 : ℝ)
⊢ ∃ (a_1 : ℝ) (h : 0 ≤ a_1 ∧ a_1 ≤ 1),
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) e.1)
          (Icc 0 (Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_1 ⋯)) <
        (↑e.2 : ℝ) ∧
      a < Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_1 ⋯
have h₁ : a < Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) (↑q : ℝ) sorry
Tactic: refine ⟨q, ⟨by simp [hqI.1], hqI.2⟩, 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 : ℝ)}
a : (↑I : Type)
h_monotone :
  ∀ (s : X),
    Monotone (β := ℝ) fun (x : (↑I : Type)) ↦
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) s)
        (Icc 0 x)
⊢ MeasurableSet.{u_1} (α := X × (↑I : Type)) {x : X × (↑I : Type) | a < f x.1 x.2}
have sSup_eq_iUnion_rat : Eq.{u_1 + 1} (α := Set (X × (↑I : Type))) {x : X × (↑I : Type) | a < f x.1 x.2}
  (⋃ (q : ℚ),
    ⋃ (hqI : (↑q : ℝ) ∈ I),
      ⋃ (_ : (↑a : ℝ) < (↑q : ℝ)),
        {e : X × (↑I : Type) |
          Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
              ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑q : ℝ) hqI)) <
            (↑e.2 : ℝ)})
Tactic: have sSup_eq_iUnion_rat : {x : X × I | a < f x.1 x.2} =
        ⋃ (q : ℚ) (hqI : ↑q ∈ I) (_ : a < (q : ℝ)), {e | (κ e.1).real (Icc 0 ⟨q, hqI⟩) < e.2} := by
      ext e
      simp_all only [lt_sSup_iff, mem_setOf_eq, Subtype.exists, mem_Icc, Rat.cast_nonneg,
        mem_iUnion, exists_prop, exists_and_left, f]
      constructor
      · rintro ⟨y, hyI, y_mem, (hy : a.1 < y)⟩
        obtain ⟨q, hqa, hqy⟩ := exists_rat_btwn hy
        refine ⟨q, hqa, ⟨?_, hqy.le.trans hyI.2⟩, lt_of_lt_of_le' y_mem (h_monotone e.1 hqy.le)⟩
        simp [← Rat.cast_nonneg (K := ℝ), a.2.1.trans hqa.le]
      · intro he
        obtain ⟨q, hqa, hqI, h⟩ := he
        refine ⟨q, ⟨by simp [hqI.1], hqI.2⟩, h, ?_⟩
        change a.1 < q
        simp [hqa]
-- 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 : ℝ)}
a : (↑I : Type)
h_monotone :
  ∀ (s : X),
    Monotone (β := ℝ) fun (x : (↑I : Type)) ↦
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) s)
        (Icc 0 x)
sSup_eq_iUnion_rat :
  Eq.{u_1 + 1} (α := Set (X × (↑I : Type))) {x : X × (↑I : Type) | a < f x.1 x.2}
    (⋃ (q : ℚ),
      ⋃ (hqI : (↑q : ℝ) ∈ I),
        ⋃ (_ : (↑a : ℝ) < (↑q : ℝ)),
          {e : X × (↑I : Type) |
            Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
                ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑q : ℝ) hqI)) <
              (↑e.2 : ℝ)})
⊢ MeasurableSet.{u_1} (α := X × (↑I : Type)) {x : X × (↑I : Type) | a < f x.1 x.2}
have rw : MeasurableSet.{u_1} (α := X × (↑I : Type))
  (⋃ (q : ℚ),
    ⋃ (hqI : (↑q : ℝ) ∈ I),
      ⋃ (_ : (↑a : ℝ) < (↑q : ℝ)),
        {e : X × (↑I : Type) |
          Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
              ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑q : ℝ) hqI)) <
            (↑e.2 : ℝ)})
Tactic: rw [sSup_eq_iUnion_rat]
-- 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 : ℝ)}
a : (↑I : Type)
h_monotone :
  ∀ (s : X),
    Monotone (β := ℝ) fun (x : (↑I : Type)) ↦
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) s)
        (Icc 0 x)
sSup_eq_iUnion_rat :
  Eq.{u_1 + 1} (α := Set (X × (↑I : Type))) {x : X × (↑I : Type) | a < f x.1 x.2}
    (⋃ (q : ℚ),
      ⋃ (hqI : (↑q : ℝ) ∈ I),
        ⋃ (_ : (↑a : ℝ) < (↑q : ℝ)),
          {e : X × (↑I : Type) |
            Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
                ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑q : ℝ) hqI)) <
              (↑e.2 : ℝ)})
⊢ MeasurableSet.{u_1} (α := X × (↑I : Type))
    (⋃ (q : ℚ),
      ⋃ (hqI : (↑q : ℝ) ∈ I),
        ⋃ (_ : (↑a : ℝ) < (↑q : ℝ)),
          {e : X × (↑I : Type) |
            Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
                ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑q : ℝ) hqI)) <
              (↑e.2 : ℝ)})
have refine : ∀ (b : ℚ) (bI : (↑b : ℝ) ∈ I),
  (↑a : ℝ) < (↑b : ℝ) →
    MeasurableSet.{u_1} (α := X × (↑I : Type))
      {e : X × (↑I : Type) |
        Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
            ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑b : ℝ) bI)) <
          (↑e.2 : ℝ)}
Tactic: refine MeasurableSet.iUnion (fun b ↦ MeasurableSet.iUnion
      (fun bI ↦ MeasurableSet.iUnion (fun _ ↦ ?_)))
-- 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 : ℝ)}
a : (↑I : Type)
h_monotone :
  ∀ (s : X),
    Monotone (β := ℝ) fun (x : (↑I : Type)) ↦
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) s)
        (Icc 0 x)
sSup_eq_iUnion_rat :
  Eq.{u_1 + 1} (α := Set (X × (↑I : Type))) {x : X × (↑I : Type) | a < f x.1 x.2}
    (⋃ (q : ℚ),
      ⋃ (hqI : (↑q : ℝ) ∈ I),
        ⋃ (_ : (↑a : ℝ) < (↑q : ℝ)),
          {e : X × (↑I : Type) |
            Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
                ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑q : ℝ) hqI)) <
              (↑e.2 : ℝ)})
b : ℚ
bI : (↑b : ℝ) ∈ I
h : (↑a : ℝ) < (↑b : ℝ)
⊢ MeasurableSet.{u_1} (α := X × (↑I : Type))
    {e : X × (↑I : Type) |
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
          ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑b : ℝ) bI)) <
        (↑e.2 : ℝ)}
have refine : Measurable (β := ℝ) fun (e : X × (↑I : Type)) ↦
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) e.1)
    (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑b : ℝ) bI))
Tactic: refine measurableSet_lt ?_ measurable_snd.subtype_val
-- 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 : ℝ)}
a : (↑I : Type)
h_monotone :
  ∀ (s : X),
    Monotone (β := ℝ) fun (x : (↑I : Type)) ↦
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) s)
        (Icc 0 x)
sSup_eq_iUnion_rat :
  Eq.{u_1 + 1} (α := Set (X × (↑I : Type))) {x : X × (↑I : Type) | a < f x.1 x.2}
    (⋃ (q : ℚ),
      ⋃ (hqI : (↑q : ℝ) ∈ I),
        ⋃ (_ : (↑a : ℝ) < (↑q : ℝ)),
          {e : X × (↑I : Type) |
            Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I))
                ((κ : (a : X) → Measure (↑I : Type)) e.1) (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑q : ℝ) hqI)) <
              (↑e.2 : ℝ)})
b : ℚ
bI : (↑b : ℝ) ∈ I
h : (↑a : ℝ) < (↑b : ℝ)
⊢ Measurable (β := ℝ) fun (e : X × (↑I : Type)) ↦
    ENNReal.toReal
      ((((κ : (a : X) → Measure (↑I : Type)) e.1 : Measure (↑I : Type)) : (a : Set (↑I : Type)) → ℝ≥0∞)
        (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑b : ℝ) bI)))
have hκ : Measurable (β := ℝ≥0∞) fun (a : X) ↦
  (((κ : (a : X) → Measure (↑I : Type)) a : Measure (↑I : Type)) : (a : Set (↑I : Type)) → ℝ≥0∞)
    (Icc 0 (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ I) (↑b : ℝ) bI))
Tactic: have hκ := κ.measurable_coe (s := Icc 0 ⟨b, bI⟩) measurableSet_Icc
-- 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 : ℝ)}
⊢ ∃ (f : X → (↑I : Type) → (↑I : Type)),
    Measurable (uncurry f) ∧
      ∀ (a : X), Eq (α := Measure (↑I : Type)) (Measure.map (f a) volume) ((κ : (a : X) → Measure (↑I : Type)) a)
have measurable_f : Measurable (uncurry f)
Tactic: have measurable_f : Measurable (uncurry f) := by
    refine measurable_of_Ioi fun a ↦ ?_
    simp only [preimage, uncurry, mem_Ioi]
    have h_monotone s : Monotone (fun x ↦ (κ s).real (Icc 0 x)) :=
      fun x y hxy ↦ measureReal_mono (by gcongr)
    have sSup_eq_iUnion_rat : {x : X × I | a < f x.1 x.2} =
        ⋃ (q : ℚ) (hqI : ↑q ∈ I) (_ : a < (q : ℝ)), {e | (κ e.1).real (Icc 0 ⟨q, hqI⟩) < e.2} := by
      ext e
      simp_all only [lt_sSup_iff, mem_setOf_eq, Subtype.exists, mem_Icc, Rat.cast_nonneg,
        mem_iUnion, exists_prop, exists_and_left, f]
      constructor
      · rintro ⟨y, hyI, y_mem, (hy : a.1 < y)⟩
        obtain ⟨q, hqa, hqy⟩ := exists_rat_btwn hy
        refine ⟨q, hqa, ⟨?_, hqy.le.trans hyI.2⟩, lt_of_lt_of_le' y_mem (h_monotone e.1 hqy.le)⟩
        simp [← Rat.cast_nonneg (K := ℝ), a.2.1.trans hqa.le]
      · intro he
        obtain ⟨q, hqa, hqI, h⟩ := he
        refine ⟨q, ⟨by simp [hqI.1], hqI.2⟩, h, ?_⟩
        change a.1 < q
        simp [hqa]
    rw [sSup_eq_iUnion_rat]
    refine MeasurableSet.iUnion (fun b ↦ MeasurableSet.iUnion
      (fun bI ↦ MeasurableSet.iUnion (fun _ ↦ ?_)))
    refine measurableSet_lt ?_ measurable_snd.subtype_val
    simp_rw [measureReal_def]
    have hκ := κ.measurable_coe (s := Icc 0 ⟨b, bI⟩) measurableSet_Icc
    fun_prop
-- 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)
⊢ ∃ (f : X → (↑I : Type) → (↑I : Type)),
    Measurable (uncurry f) ∧
      ∀ (a : X), Eq (α := Measure (↑I : Type)) (Measure.map (f a) volume) ((κ : (a : X) → Measure (↑I : Type)) a)
have refine : ∀ (a : X) (x : (↑I : Type)),
  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∞)
Tactic: refine ⟨f, measurable_f, fun a ↦ (volume.map (f a)).ext_of_Iic (κ a) fun 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 x = Icc 0 x
have h : ∀ (x_1 : (↑I : Type)), x_1 ∈ Iic x ↔ x_1 ∈ Icc 0 x
Tactic: ext
-- 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)
⊢ 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 Iic_to_Icc : Iic x = Icc 0 x
Tactic: have Iic_to_Icc : Iic x = Icc 0 x := by ext; simp
-- 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
⊢ 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 κ_in_I : Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
    (Icc 0 x) ∈
  I
Tactic: have κ_in_I : ((κ a).real (Icc 0 x)) ∈ I := ⟨measureReal_nonneg, measureReal_le_one⟩