awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
⊢ κ.fst ⊗ₖ κ.condKernelReal = κ
have rw : κ.fst ⊗ₖ IsCondKernelCDF.toKernel κ.condKernelCDF sorry = κ
Tactic: rw [condKernelReal, compProd_toKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel.{u_1, u_3} α (γ × ℝ)
inst_1 : IsFiniteKernel κ
rw : κ.fst ⊗ₖ IsCondKernelCDF.toKernel κ.condKernelCDF ⋯ = κ
⊢ κ.fst ⊗ₖ κ.condKernelReal = κ
have rw₁ : κ = κ
Tactic: rw [condKernelReal, compProd_toKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
κ : Kernel Unit (α × ℝ)
inst_3 : IsFiniteKernel κ
⊢ κ.fst ⊗ₖ κ.condKernelUnitReal = κ
have rw : const Unit ((κ : (a : Unit) → Measure (α × ℝ)) ()) = κ
Tactic: rw [condKernelUnitReal, compProd_toKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
κ : Kernel Unit (α × ℝ)
inst_3 : IsFiniteKernel κ
⊢ const Unit ((κ : (a : Unit) → Measure (α × ℝ)) ()) = κ
have h : ∀ (a : Unit) (s : Set (α × ℝ)),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      ((((const Unit ((κ : (a : Unit) → Measure (α × ℝ)) ()) : (a : Unit) → Measure (α × ℝ)) a : Measure (α × ℝ)) :
            (a : Set (α × ℝ)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((κ : (a : Unit) → Measure (α × ℝ)) a : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
⊢ Eq (α := Measure Ω)
    (Measure.comap (embeddingReal Ω)
      (if
          Membership.mem (γ := Set α)
            (preimage (β := ℝ≥0∞)
              (fun (a : α) ↦
                (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
              {0})
            a then
        (η : (a : α) → Measure ℝ) a
      else Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
    (if
        Eq (α := ℝ≥0∞)
          ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞) then
      Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
    else
      Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
have simp : Eq (α := Measure Ω)
  (Measure.comap (embeddingReal Ω)
    (if
        Eq (α := ℝ≥0∞)
          ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞) then
      (η : (a : α) → Measure ℝ) a
    else Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) sorry)))
  (if
      Eq (α := ℝ≥0∞)
        ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
        (0 : ℝ≥0∞) then
    Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
  else
    Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) sorry)))
Tactic: simp only [mem_preimage, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
⊢ Eq (α := Measure Ω)
    (Measure.comap (embeddingReal Ω)
      (if
          Eq (α := ℝ≥0∞)
            ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞) then
        (η : (a : α) → Measure ℝ) a
      else Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
    (if
        Eq (α := ℝ≥0∞)
          ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞) then
      Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
    else
      Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
have pos : Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞) →
  Eq (α := Measure Ω) (Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a))
    (Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
pos :
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞) →
    Eq (α := Measure Ω) (Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a))
      (Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a))
⊢ Eq (α := Measure Ω)
    (Measure.comap (embeddingReal Ω)
      (if
          Eq (α := ℝ≥0∞)
            ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞) then
        (η : (a : α) → Measure ℝ) a
      else Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
    (if
        Eq (α := ℝ≥0∞)
          ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞) then
      Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
    else
      Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)))
have neg : ¬Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞) →
  Eq (α := Measure Ω)
    (Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) sorry)))
    (Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) sorry)))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
⊢ Eq.{u_5 + 1} (α := Measure Ω) (((borelMarkovFromReal Ω η : Kernel α Ω) : (a : α) → Measure Ω) a : Measure Ω)
    (if
          Eq (α := ℝ≥0∞)
            ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞) then
        Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
      else
        Measure.comap (embeddingReal Ω)
          (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)) :
      Measure Ω)
have rw : Eq.{u_5 + 1} (α := Measure Ω)
  ((((piecewise (s :=
                preimage (β := ℝ≥0∞)
                  (fun (a : α) ↦
                    (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
                  {0})
                sorry η
                (deterministic (fun (x : α) ↦ Exists.choose (p := Membership.mem (range (embeddingReal Ω))) sorry)
                  sorry)).comapRight
            (f := embeddingReal Ω) sorry :
          Kernel α Ω) :
        (a : α) → Measure Ω)
      a :
    Measure Ω)
  (if
        Eq (α := ℝ≥0∞)
          ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞) then
      Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
    else
      Measure.comap (embeddingReal Ω)
        (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) sorry)) :
    Measure Ω)
Tactic: classical
  rw [borelMarkovFromReal, comapRight_apply, piecewise_apply, deterministic_apply]
  simp only [mem_preimage, mem_singleton_iff]
  split_ifs <;> rfl
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
rw :
  Eq.{u_5 + 1} (α := Measure Ω)
    ((((piecewise (s :=
                  preimage (β := ℝ≥0∞)
                    (fun (a : α) ↦
                      (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
                    {0})
                  ⋯ η
                  (deterministic (fun (x : α) ↦ Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)
                    ⋯)).comapRight
              (f := embeddingReal Ω) ⋯ :
            Kernel α Ω) :
          (a : α) → Measure Ω)
        a :
      Measure Ω)
    (if
          Eq (α := ℝ≥0∞)
            ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞) then
        Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
      else
        Measure.comap (embeddingReal Ω)
          (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)) :
      Measure Ω)
⊢ Eq.{u_5 + 1} (α := Measure Ω) (((borelMarkovFromReal Ω η : Kernel α Ω) : (a : α) → Measure Ω) a : Measure Ω)
    (if
          Eq (α := ℝ≥0∞)
            ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞) then
        Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
      else
        Measure.comap (embeddingReal Ω)
          (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)) :
      Measure Ω)
have rw₁ : Eq (α := Measure Ω)
  (Measure.comap (embeddingReal Ω)
    ((piecewise (s :=
          preimage (β := ℝ≥0∞)
            (fun (a : α) ↦ (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
            {0})
          sorry η (deterministic (fun (x : α) ↦ Exists.choose (p := Membership.mem (range (embeddingReal Ω))) sorry) sorry) :
        (a : α) → Measure ℝ)
      a))
  (if
      Eq (α := ℝ≥0∞)
        ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
        (0 : ℝ≥0∞) then
    Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
  else
    Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) sorry)))
Tactic: classical
  rw [borelMarkovFromReal, comapRight_apply, piecewise_apply, deterministic_apply]
  simp only [mem_preimage, mem_singleton_iff]
  split_ifs <;> rfl
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
s : Set Ω
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((((borelMarkovFromReal Ω η : Kernel α Ω) : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (if
          Eq (α := ℝ≥0∞)
            ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞) then
        (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s)
      else (embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) :
      ℝ≥0∞)
have he : MeasurableEmbedding (embeddingReal Ω)
Tactic: have he := measurableEmbedding_embeddingReal Ω
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
s : Set Ω
hs : MeasurableSet s
he : MeasurableEmbedding (embeddingReal Ω)
⊢ Eq (α := ℝ≥0∞)
    (((((borelMarkovFromReal Ω η : Kernel α Ω) : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    (if
          Eq (α := ℝ≥0∞)
            ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞) then
        (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s)
      else (embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) :
      ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  (((if
              Eq (α := ℝ≥0∞)
                ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
                (0 : ℝ≥0∞) then
            Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
          else
            Measure.comap (embeddingReal Ω)
              (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) sorry)) :
          Measure Ω) :
        (a : Set Ω) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  (if
        Eq (α := ℝ≥0∞)
          ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞) then
      (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s)
    else (embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) sorry) :
    ℝ≥0∞)
Tactic: rw [borelMarkovFromReal_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
s : Set Ω
hs : MeasurableSet s
he : MeasurableEmbedding (embeddingReal Ω)
⊢ Eq (α := ℝ≥0∞)
    (((if
                Eq (α := ℝ≥0∞)
                  ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
                  (0 : ℝ≥0∞) then
              Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
            else
              Measure.comap (embeddingReal Ω)
                (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)) :
            Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (if
          Eq (α := ℝ≥0∞)
            ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞) then
        (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s)
      else (embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) :
      ℝ≥0∞)
have pos : ∀
  (h :
    Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞)
    (((Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s) : ℝ≥0∞)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
s : Set Ω
hs : MeasurableSet s
he : MeasurableEmbedding (embeddingReal Ω)
pos :
  ∀
    (h :
      Eq (α := ℝ≥0∞)
        ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
        (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞)
      (((Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((if
                Eq (α := ℝ≥0∞)
                  ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
                  (0 : ℝ≥0∞) then
              Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a)
            else
              Measure.comap (embeddingReal Ω)
                (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)) :
            Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (if
          Eq (α := ℝ≥0∞)
            ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞) then
        (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s)
      else (embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) :
      ℝ≥0∞)
have neg : ∀
  (h :
    ¬Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
        (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞)
    (((Measure.comap (embeddingReal Ω)
              (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) sorry)) :
            Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) sorry) : ℝ≥0∞)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
s : Set Ω
hs : MeasurableSet s
he : MeasurableEmbedding (embeddingReal Ω)
h :
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.comap (embeddingReal Ω) ((η : (a : α) → Measure ℝ) a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s) : ℝ≥0∞)
have pos : Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s) : ℝ≥0∞)
  ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s) : ℝ≥0∞)
Tactic: rw [Measure.comap_apply _ he.injective he.measurableSet_image' _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
s : Set Ω
hs : MeasurableSet s
he : MeasurableEmbedding (embeddingReal Ω)
h :
  ¬Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.comap (embeddingReal Ω)
              (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)) :
            Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) : ℝ≥0∞)
have neg : Eq (α := ℝ≥0∞)
  ((Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) sorry) : (a : Set ℝ) → ℝ≥0∞)
      (embeddingReal Ω '' s) :
    ℝ≥0∞)
  ((embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) sorry) : ℝ≥0∞)
Tactic: rw [Measure.comap_apply _ he.injective he.measurableSet_image' _ hs, Measure.dirac_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst : Nonempty Ω
inst_1 : MeasurableSpace Ω
inst_2 : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
s : Set Ω
hs : MeasurableSet s
he : MeasurableEmbedding (embeddingReal Ω)
h :
  ¬Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)
neg :
  Eq (α := ℝ≥0∞)
    ((Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) : (a : Set ℝ) → ℝ≥0∞)
        (embeddingReal Ω '' s) :
      ℝ≥0∞)
    ((embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.comap (embeddingReal Ω)
              (Measure.dirac (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯)) :
            Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) : ℝ≥0∞)
have neg₁ : Eq (α := ℝ≥0∞) ((embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) sorry))
  ((embeddingReal Ω '' s).indicator 1 (Exists.choose (p := Membership.mem (range (embeddingReal Ω))) sorry))
Tactic: rw [Measure.comap_apply _ he.injective he.measurableSet_image' _ hs, Measure.dirac_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
η : Kernel α ℝ
inst_3 : IsMarkovKernel η
⊢ IsMarkovKernel (mβ := mΩ) (borelMarkovFromReal Ω η)
have refine : ∀ (a : α),
  Eq (α := ℝ≥0∞)
    ((((piecewise (s :=
                  preimage (β := ℝ≥0∞)
                    (fun (a : α) ↦
                      (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
                    {0})
                  sorry η
                  (deterministic (fun (x : α) ↦ Exists.choose (p := Membership.mem (range (embeddingReal Ω))) sorry) sorry) :
                (a : α) → Measure ℝ)
              a :
            Measure ℝ) :
          (a : Set ℝ) → ℝ≥0∞)
        (range (embeddingReal Ω)) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
Tactic: refine IsMarkovKernel.comapRight _ (measurableEmbedding_embeddingReal Ω) (fun a ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
η : Kernel α ℝ
inst_3 : IsMarkovKernel η
a : α
⊢ Eq (α := ℝ≥0∞)
    (((if
                Membership.mem (γ := Set α)
                  (preimage (β := ℝ≥0∞)
                    (fun (a : α) ↦
                      (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
                    {0})
                  a then
              (η : (a : α) → Measure ℝ) a
            else
              ((deterministic (fun (x : α) ↦ Exists.choose (p := Membership.mem (range (embeddingReal Ω))) ⋯) ⋯ :
                    Kernel α ℝ) :
                  (a : α) → Measure ℝ)
                a :
            Measure ℝ) :
          (a : Set ℝ) → ℝ≥0∞)
        (range (embeddingReal Ω)) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
have pos : ∀
  (h :
    Membership.mem (γ := Set α)
      (preimage (β := ℝ≥0∞)
        (fun (a : α) ↦ (((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ) {0})
      a),
  Eq (α := ℝ≥0∞) ((((η : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω)) : ℝ≥0∞)
    (1 : ℝ≥0∞)
Tactic: split_ifs with h