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ξ :
  (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)
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
⊢ f a ξ ≤ x

Tactic:
simp only [sSup_le_iff, f]

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)
hξ :
  (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)
c : (↑I : Type)
hc :
  Membership.mem (γ := Set (↑I : Type))
    {x : (↑I : Type) |
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
          (Icc 0 x) <
        (↑ξ : ℝ)}
    c
h : ∀ (h : x < c), False
⊢ c ≤ x

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ξ :
  (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)
c : (↑I : Type)
hc :
  Membership.mem (γ := Set (↑I : Type))
    {x : (↑I : Type) |
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
          (Icc 0 x) <
        (↑ξ : ℝ)}
    c
h : x < c
⊢ ¬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 c)

Tactic:
have h_lt : ¬ (κ a).real (Icc 0 x) ≤ (κ a).real (Icc 0 c) := not_le.mpr (lt_of_le_of_lt' hξ hc)
-- 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ξ :
  (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)
c : (↑I : Type)
hc :
  Membership.mem (γ := Set (↑I : Type))
    {x : (↑I : Type) |
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
          (Icc 0 x) <
        (↑ξ : ℝ)}
    c
h : x < c
h_lt :
  ¬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 c)
⊢ False

Tactic:
h_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 : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ :
  (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)
c : (↑I : Type)
hc :
  Membership.mem (γ := Set (↑I : Type))
    {x : (↑I : Type) |
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
          (Icc 0 x) <
        (↑ξ : ℝ)}
    c
h : x < c
h_lt :
  ¬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 c)
h₁ :
  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 c)
⊢ False

Tactic:
refine h_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 : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ :
  (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)
c : (↑I : Type)
hc :
  Membership.mem (γ := Set (↑I : Type))
    {x : (↑I : Type) |
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
          (Icc 0 x) <
        (↑ξ : ℝ)}
    c
h : x < c
h_lt :
  ¬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 c)
h₁ :
  autoParam
    (Ne (α := ℝ≥0∞)
      ((((κ : (a : X) → Measure (↑I : Type)) a : Measure (↑I : Type)) : (a : Set (↑I : Type)) → ℝ≥0∞) (Icc 0 c) : ℝ≥0∞)
      (∞ : ℝ≥0∞))
    measureReal_mono._auto_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 c)

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 : ℝ)}
measurable_f : Measurable (uncurry f)
a : X
x : (↑I : Type)
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I :
  Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x) ∈
    I
ξ : (↑I : Type)
hξ :
  (↑ξ : ℝ) ≤
    Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
      (Icc 0 x)
c : (↑I : Type)
hc :
  Membership.mem (γ := Set (↑I : Type))
    {x : (↑I : Type) |
      Measure.real (m := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) ((κ : (a : X) → Measure (↑I : Type)) a)
          (Icc 0 x) <
        (↑ξ : ℝ)}
    c
h : x < c
h_lt :
  ¬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 c)
⊢ autoParam
    (Ne (α := ℝ≥0∞)
      ((((κ : (a : X) → Measure (↑I : Type)) a : Measure (↑I : Type)) : (a : Set (↑I : Type)) → ℝ≥0∞) (Icc 0 c) : ℝ≥0∞)
      (∞ : ℝ≥0∞))
    measureReal_mono._auto_1

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Representation
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
⊢ MeasurableEmbedding (sigmoid ∘ embeddingReal Y)

Tactic:
have hg := measurableEmbedding_sigmoid_comp_embeddingReal Y
-- Module: Mathlib.Probability.Kernel.Representation
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
⊢ IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)

Tactic:
have hκg : IsMarkovKernel (κ.map g) := IsMarkovKernel.map κ hg.measurable
-- Module: Mathlib.Probability.Kernel.Representation
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)
⊢ Measurable hg.invFun

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Representation
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)
rw : κ = κ.map (hg.invFun ∘ sigmoid ∘ embeddingReal Y)
rw₁ : κ = κ.map id
rw₂ rw₃ : κ = κ
⊢ κ = map (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g) hg.invFun

Tactic:
rw [← map_comp_right _ hg.measurable (by fun_prop), LeftInverse.id hg.leftInverse_invFun,
      map_id]

Premises used: ProbabilityTheory.Kernel.map_comp_right, Function.LeftInverse.id, MeasurableEmbedding.measurable, MeasurableEmbedding.leftInverse_invFun, ProbabilityTheory.Kernel.map_id
-- Module: Mathlib.Probability.Kernel.Representation
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)
⊢ κ = map (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g) hg.invFun

Tactic:
have hg'κ : κ = (κ.map g).map hg.invFun := by
    rw [← map_comp_right _ hg.measurable (by fun_prop), LeftInverse.id hg.leftInverse_invFun,
      map_id]
-- Module: Mathlib.Probability.Kernel.Representation
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)
hg'κ : κ = map (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g) hg.invFun
obtain :
  ∀ (f' : X → (↑I : Type) → (↑I : Type)) (hf' : Measurable (uncurry f'))
    (hf'κ :
      ∀ (a : X),
        Eq (α := Measure (↑I : Type)) (Measure.map (f' a) volume)
          (((κ.map g : Kernel X (↑I : Type)) : (a : X) → Measure (↑I : Type)) a)),
    ∃ (f : X → (↑I : Type) → Y),
      Measurable (uncurry f) ∧ ∀ (a : X), Eq (α := Measure Y) (Measure.map (f a) volume) ((κ : (a : X) → Measure Y) a)
⊢ ∃ (f : X → (↑I : Type) → Y),
    Measurable (uncurry f) ∧ ∀ (a : X), Eq (α := Measure Y) (Measure.map (f a) volume) ((κ : (a : X) → Measure Y) a)

Tactic:
obtain ⟨f', hf', hf'κ⟩ := (κ.map g).exists_measurable_map_eq_unitInterval_aux

Premises used: _private.0.ProbabilityTheory.Kernel.exists_measurable_map_eq_unitInterval_aux, ProbabilityTheory.Kernel.map
-- Module: Mathlib.Probability.Kernel.Representation
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)
hg'κ : κ = map (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g) hg.invFun
f' : X → (↑I : Type) → (↑I : Type)
hf' : Measurable (uncurry f')
hf'κ :
  ∀ (a : X),
    Eq (α := Measure (↑I : Type)) (Measure.map (f' a) volume)
      (((κ.map g : Kernel X (↑I : Type)) : (a : X) → Measure (↑I : Type)) a)
⊢ Measurable.{u_1, u_2} (α := X × (↑I : Type)) (β := Y) (uncurry fun (a : X) (u : (↑I : Type)) ↦ hg.invFun (f' a u))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Representation
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)
hg'κ : κ = map (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g) hg.invFun
f' : X → (↑I : Type) → (↑I : Type)
hf' : Measurable (uncurry f')
hf'κ :
  ∀ (a : X),
    Eq (α := Measure (↑I : Type)) (Measure.map (f' a) volume)
      (((κ.map g : Kernel X (↑I : Type)) : (a : X) → Measure (↑I : Type)) a)
refine :
  ∀ (a : X),
    Eq.{u_2 + 1} (α := Measure Y)
      (Measure.map (α := (↑I : Type)) ((fun (a : X) (u : (↑I : Type)) ↦ hg.invFun (f' a u)) a) volume)
      ((κ : (a : X) → Measure Y) a)
⊢ ∃ (f : X → (↑I : Type) → Y),
    Measurable (uncurry f) ∧ ∀ (a : X), Eq (α := Measure Y) (Measure.map (f a) volume) ((κ : (a : X) → Measure Y) a)

Tactic:
refine ⟨fun a u ↦ hg.invFun (f' a u), by fun_prop, fun a ↦ ?_⟩
-- Module: Mathlib.Probability.Kernel.Representation
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)
hg'κ : κ = map (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g) hg.invFun
f' : X → (↑I : Type) → (↑I : Type)
hf' : Measurable (uncurry f')
hf'κ :
  ∀ (a : X),
    Eq (α := Measure (↑I : Type)) (Measure.map (f' a) volume)
      (((κ.map g : Kernel X (↑I : Type)) : (a : X) → Measure (↑I : Type)) a)
a : X
⊢ Measurable hg.invFun

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Representation
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)
hg'κ : κ = map (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g) hg.invFun
f' : X → (↑I : Type) → (↑I : Type)
hf' : Measurable (uncurry f')
hf'κ :
  ∀ (a : X),
    Eq (α := Measure (↑I : Type)) (Measure.map (f' a) volume)
      (((κ.map g : Kernel X (↑I : Type)) : (a : X) → Measure (↑I : Type)) a)
a : X
⊢ Measurable (f' a)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Representation
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)
hg'κ : κ = map (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g) hg.invFun
f' : X → (↑I : Type) → (↑I : Type)
hf' : Measurable (uncurry f')
hf'κ :
  ∀ (a : X),
    Eq (α := Measure (↑I : Type)) (Measure.map (f' a) volume)
      (((κ.map g : Kernel X (↑I : Type)) : (a : X) → Measure (↑I : Type)) a)
a : X
rw :
  Eq (α := Measure Y) (Measure.map (α := (↑I : Type)) ((fun (a : X) (u : (↑I : Type)) ↦ hg.invFun (f' a u)) a) volume)
    (Measure.map (hg.invFun ∘ f' a) volume)
⊢ Eq.{u_2 + 1} (α := Measure Y)
    (Measure.map (α := (↑I : Type)) ((fun (a : X) (u : (↑I : Type)) ↦ hg.invFun (f' a u)) a) volume)
    ((κ : (a : X) → Measure Y) a)

Tactic:
rw [hg'κ, map_apply _ (by fun_prop), ← hf'κ, Measure.map_map (by fun_prop) (by fun_prop)]

Premises used: ProbabilityTheory.Kernel.map_apply, MeasureTheory.Measure.map_map
-- Module: Mathlib.Probability.Kernel.Representation
Goal:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
κ : Kernel X Y
inst_2 : IsMarkovKernel κ
g : Y → (↑I : Type) := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g)
hg'κ : κ = map (mβ := Subtype.instMeasurableSpace (p := fun (x : ℝ) ↦ x ∈ I)) (κ.map g) hg.invFun
f' : X → (↑I : Type) → (↑I : Type)
hf' : Measurable (uncurry f')
hf'κ :
  ∀ (a : X),
    Eq (α := Measure (↑I : Type)) (Measure.map (f' a) volume)
      (((κ.map g : Kernel X (↑I : Type)) : (a : X) → Measure (↑I : Type)) a)
a : X
⊢ Eq (α := Measure Y) (Measure.map (α := (↑I : Type)) ((fun (a : X) (u : (↑I : Type)) ↦ hg.invFun (f' a u)) a) volume)
    (Measure.map (hg.invFun ∘ f' a) volume)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Representation
Goal:
Y : Type u_2
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
μ : Measure Y
inst_2 : IsProbabilityMeasure μ
obtain :
  ∀ (f : Unit → (↑I : Type) → Y) (hf_meas : Measurable (uncurry f))
    (hf_map : ∀ (a : Unit), Eq (α := Measure Y) (map (f a) volume) ((Kernel.const Unit μ : (a : Unit) → Measure Y) a)),
    ∃ (f : (↑I : Type) → Y), Measurable f ∧ map f volume = μ
⊢ ∃ (f : (↑I : Type) → Y), Measurable f ∧ map f volume = μ

Tactic:
obtain ⟨f, hf_meas, hf_map⟩ := Kernel.exists_measurable_map_eq_unitInterval (Kernel.const Unit μ)

Premises used: ProbabilityTheory.Kernel.exists_measurable_map_eq_unitInterval, Unit, ProbabilityTheory.Kernel.const
-- Module: Mathlib.Probability.Kernel.Representation
Goal:
Y : Type u_2
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
μ : Measure Y
inst_2 : IsProbabilityMeasure μ
f : Unit → (↑I : Type) → Y
hf_meas : Measurable (uncurry f)
hf_map : ∀ (a : Unit), Eq (α := Measure Y) (map (f a) volume) ((Kernel.const Unit μ : (a : Unit) → Measure Y) a)
⊢ Eq (α := Measure Y) (map (f ()) volume) ((Kernel.const Unit μ : (a : Unit) → Measure Y) ())

Tactic:
specialize hf_map ()

Premises used: Unit.unit
-- Module: Mathlib.Probability.Kernel.Representation
Goal:
Y : Type u_2
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
μ : Measure Y
inst_2 : IsProbabilityMeasure μ
f : Unit → (↑I : Type) → Y
hf_meas : Measurable (uncurry f)
hf_map : Eq (α := Measure Y) (map (f ()) volume) ((Kernel.const Unit μ : (a : Unit) → Measure Y) ())
⊢ Measurable (f ())

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.Representation
Goal:
Y : Type u_2
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
μ : Measure Y
inst_2 : IsProbabilityMeasure μ
f : Unit → (↑I : Type) → Y
hf_meas : Measurable (uncurry f)
hf_map : Eq (α := Measure Y) (map (f ()) volume) ((Kernel.const Unit μ : (a : Unit) → Measure Y) ())
⊢ map (f ()) volume = μ

Tactic:
simpa
-- Module: Mathlib.Probability.Kernel.Representation
Goal:
Y : Type u_2
inst : Nonempty Y
mY : MeasurableSpace Y
inst_1 : StandardBorelSpace Y
μ : Measure Y
inst_2 : IsProbabilityMeasure μ
f : Unit → (↑I : Type) → Y
hf_meas : Measurable (uncurry f)
hf_map : Eq (α := Measure Y) (map (f ()) volume) ((Kernel.const Unit μ : (a : Unit) → Measure Y) ())
⊢ ∃ (f : (↑I : Type) → Y), Measurable f ∧ map f volume = μ

Tactic:
exact ⟨f (), by fun_prop, by simpa⟩
-- Module: Mathlib.Probability.Kernel.SetIntegral
Goal:
X : Type u_1
Y : Type u_2
E : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
κ : Kernel X Y
μ : Measure X
f : X → Y → E
s : Set X
hs : MeasurableSet s
simp_rw :
  Eq.{u_3 + 1} (α := E)
    (∫ (x : X), @integral _ _ _ _ mY ((κ : (a : X) → Measure Y) x) fun (y : Y) ↦ s.indicator (fun (x : X) ↦ f x y) x ∂μ)
    (∫ (x : X), s.indicator (fun (x : X) ↦ @integral _ _ _ _ mY ((κ : (a : X) → Measure Y) x) fun (y : Y) ↦ f x y) x ∂μ)
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (x : X), @integral _ _ _ _ mY ((κ : (a : X) → Measure Y) x) fun (y : Y) ↦ s.indicator (fun (x : X) ↦ f x y) x ∂μ)
    (∫ (x : X) in s, @integral _ _ _ _ mY ((κ : (a : X) → Measure Y) x) fun (y : Y) ↦ f x y ∂μ)

Tactic:
simp_rw [← integral_indicator hs, Kernel.integral_indicator₂]

Premises used: MeasureTheory.integral_indicator, ProbabilityTheory.Kernel.integral_indicator₂
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel α β
f_1 : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
⊢ Measurable.{u_1, u_2} (β := Measure β) fun (a : α) ↦ Measure.withDensity ((κ : (a : α) → Measure β) a) (f a)

Tactic:
Measure.measurable_of_measurable_coe _ fun s hs => ?_

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe