awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
⊢ (∀ᵐ (b : γ) ∂((η : (a : α) → Measure γ) a : Measure γ), κ.rnDeriv η a b = 1) ↔
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a)
        ((η : (a : α) → Measure γ) a) =ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)]
      1

Tactic:
eventually_congr ?_

Premises used: Filter.EventuallyEq, Filter.eventually_congr
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
refine :
  ∀ᵐ (x : γ) ∂((η : (a : α) → Measure γ) a : Measure γ),
    κ.rnDeriv η a x = 1 ↔ Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x = 1 x
⊢ (∀ᵐ (b : γ) ∂((η : (a : α) → Measure γ) a : Measure γ), κ.rnDeriv η a b = 1) ↔
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a)
        ((η : (a : α) → Measure γ) a) =ᶠ[ae (F := Measure γ) ((η : (a : α) → Measure γ) a : Measure γ)]
      1

Tactic:
refine eventually_congr ?_

Premises used: Filter.eventually_congr
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
h :
  ∀ (c : γ)
    (hc : κ.rnDeriv η a c = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c),
    κ.rnDeriv η a c = 1 ↔ Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c = 1 c
⊢ ∀ᵐ (x : γ) ∂((η : (a : α) → Measure γ) a : Measure γ),
    κ.rnDeriv η a x = 1 ↔ Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x = 1 x

Tactic:
filter_upwards [rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with c hc

Premises used: ProbabilityTheory.Kernel.rnDeriv_eq_rnDeriv_measure
-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
h_ac :
  Measure.AbsolutelyContinuous.{u_2} (α := γ) (_m0 := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)
c : γ
hc : κ.rnDeriv η a c = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c
h :
  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c = 1 ↔
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c = 1 c
h₁ h₂ :
  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c = 1 ↔
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c = 1
⊢ κ.rnDeriv η a c = 1 ↔ Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) c = 1 c

Tactic:
rw [hc, Pi.one_apply]

Premises used: Pi.one_apply
-- 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:
measurable_of_Ioi fun a ↦ ?_

Premises used: measurable_of_Ioi
-- 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 : ℝ)}
refine : ∀ (a : (↑I : Type)), MeasurableSet (uncurry f ⁻¹' Ioi a)
⊢ Measurable (uncurry f)

Tactic:
refine measurable_of_Ioi fun a ↦ ?_

Premises used: measurable_of_Ioi
-- 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)
simp : MeasurableSet.{u_1} (α := X × (↑I : Type)) {x : X × (↑I : Type) | a < f x.1 x.2}
⊢ MeasurableSet (uncurry f ⁻¹' Ioi a)

Tactic:
simp only [preimage, uncurry, mem_Ioi]

Premises used: Set.mem_Ioi, Set.preimage, Function.uncurry
-- 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)
s : X
x y : (↑I : Type)
hxy : x ≤ y
⊢ Icc 0 x ⊆ Icc 0 y

Tactic:
gcongr
-- 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)
⊢ ∀ (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)

Tactic:
have h_monotone s : Monotone (fun x ↦ (κ s).real (Icc 0 x)) :=
      fun x y hxy ↦ measureReal_mono (by gcongr)
-- 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)
h :
  ∀ (e : X × (↑I : Type)),
    Membership.mem (γ := Set (X × (↑I : Type))) {x : X × (↑I : Type) | a < f x.1 x.2} e ↔
      Membership.mem (γ := Set (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 : ℝ)})
        e
⊢ 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:
ext e
-- 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)
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 : ℝ)
⊢ Membership.mem (γ := Set (X × (↑I : Type))) {x : X × (↑I : Type) | a < f x.1 x.2} e ↔
    Membership.mem (γ := Set (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 : ℝ)})
      e

Tactic:
simp_all only [lt_sSup_iff, mem_setOf_eq, Subtype.exists, mem_Icc, Rat.cast_nonneg,
        mem_iUnion, exists_prop, exists_and_left, f]

Premises used: Set.mem_iUnion, Subtype.exists, exists_and_left, Set.mem_setOf_eq, exists_prop, Rat.cast_nonneg, Set.mem_Icc, lt_sSup_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 : ℝ)}
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 : ℝ)
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 : ℝ) ⋯)) <
            (↑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 ⋯)) <
          (↑e.2 : ℝ) ∧
        a < Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) a_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 : ℝ)

Tactic:
constructor
-- 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)
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
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 : ℝ) ⋯)) <
            (↑e.2 : ℝ)
⊢ ∃ (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 : ℝ)

Tactic:
obtain ⟨q, hqa, hqy⟩ := exists_rat_btwn hy

Premises used: exists_rat_btwn
-- 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)
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 : ℝ)

Tactic:
⟨q, hqa, ⟨?_, hqy.le.trans hyI.2⟩, lt_of_lt_of_le' y_mem (h_monotone e.1 hqy.le)⟩

Premises used: lt_of_lt_of_le', LT.lt.le, Prod.fst, And.right, And.intro, Exists.intro, LE.le.trans
-- 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)
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
h : 0 ≤ q
⊢ ∃ (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 : ℝ)

Tactic:
refine ⟨q, hqa, ⟨?_, hqy.le.trans hyI.2⟩, lt_of_lt_of_le' y_mem (h_monotone e.1 hqy.le)⟩
-- 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)
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
⊢ 0 ≤ q

Tactic:
simp [← Rat.cast_nonneg (K := ℝ), a.2.1.trans hqa.le]

Premises used: LT.lt.le, Rat.cast_nonneg, And.left, LE.le.trans, 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 : ℝ)}
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 : ℝ)
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 : ℝ) ⋯)) <
        (↑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 ⋯
⊢ ∃ (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 ⋯

Tactic:
obtain ⟨q, hqa, hqI, h⟩ := he
-- 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)
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 : ℝ)
⊢ LE.le (α := ℝ) 0 (↑q : ℝ)

Tactic:
simp [hqI.1]

Premises used: And.left
-- 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)
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 : ℝ)
h₁ : a < Subtype.mk (p := fun (a : ℝ) ↦ a ∈ I) (↑q : ℝ) ⋯
⊢ ∃ (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 ⋯

Tactic:
refine ⟨q, ⟨by simp [hqI.1], hqI.2⟩, 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 : ℝ)}
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 : ℝ) < (↑q : ℝ)

Tactic:
simp [hqa]