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 : ℝ)}
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)
⊢ 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]
-- 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 : ℝ)}
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 : ℝ)})
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 : ℝ)})
⊢ MeasurableSet.{u_1} (α := X × (↑I : Type)) {x : X × (↑I : Type) | a < f x.1 x.2}

Tactic:
rw [sSup_eq_iUnion_rat]
-- 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 : ℝ)}
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 : ℝ)})

Tactic:
MeasurableSet.iUnion (fun b ↦ MeasurableSet.iUnion
      (fun bI ↦ MeasurableSet.iUnion (fun _ ↦ ?_)))

Premises used: MeasurableSet.iUnion
-- 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 : ℝ)}
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 : ℝ)})
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 : ℝ)}
⊢ 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:
refine MeasurableSet.iUnion (fun b ↦ MeasurableSet.iUnion
      (fun bI ↦ MeasurableSet.iUnion (fun _ ↦ ?_)))

Premises used: MeasurableSet.iUnion
-- 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 : ℝ)}
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 : ℝ)}

Tactic:
measurableSet_lt ?_ measurable_snd.subtype_val

Premises used: setOf, Measurable.subtype_val, measurable_snd, measurableSet_lt
-- 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 : ℝ)}
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 : ℝ)
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))
⊢ 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_lt ?_ measurable_snd.subtype_val

Premises used: Measurable.subtype_val, measurable_snd, measurableSet_lt
-- 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 : ℝ)}
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 (β := ℝ≥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
-- 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 : ℝ)}
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 : ℝ)
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))
⊢ 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)))

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 (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
-- 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)
⊢ ∃ (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)

Tactic:
⟨f, measurable_f, fun a ↦ (volume.map (f a)).ext_of_Iic (κ a) fun x ↦ ?_⟩

Premises used: MeasureTheory.Measure.ext_of_Iic, MeasureTheory.MeasureSpace.volume, MeasureTheory.Measure.map, And.intro, Exists.intro, 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)
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∞)
⊢ ∃ (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)

Tactic:
refine ⟨f, measurable_f, fun a ↦ (volume.map (f a)).ext_of_Iic (κ a) fun 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)
h : ∀ (x_1 : (↑I : Type)), x_1 ∈ Iic x ↔ x_1 ∈ Icc 0 x
⊢ Iic x = Icc 0 x

Tactic:
ext
-- 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 x_1 : (↑I : Type)
⊢ x_1 ∈ Iic x ↔ x_1 ∈ Icc 0 x

Tactic:
simp
-- 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 x = Icc 0 x

Tactic:
have Iic_to_Icc : Iic x = Icc 0 x := by ext; simp
-- 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
⊢ 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⟩
-- 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
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∞)
⊢ 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:
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⟩]

Premises used: unitInterval.volume_Iic, MeasureTheory.Measure.map_apply, MeasureTheory.ofReal_measureReal, MeasureTheory.measure_ne_top, measurableSet_Iic, Subtype.mk, Set.preimage, Measurable.of_uncurry_left, Set.mem_Iic, 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
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
⊢ 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:
congr with ξ
-- 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 →
    ξ ≤
      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
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
⊢ 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