awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
this : Prod.map id e ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ = ∅
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞)
        (Prod.map id e ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) ∅) 0
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞)
        (Prod.map id e ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have suffices : Prod.map id e ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ = ∅
Tactic: suffices Prod.map id e ⁻¹' (univ ×ˢ range e)ᶜ = ∅ by rw [this]; simp
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
⊢ Prod.map id e ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ = ∅
have h : ∀ (x : β × Ω), x ∈ Prod.map id e ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ ↔ Membership.mem (γ := Set (β × Ω)) ∅ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (hypothesis)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
⊢ ∀ᵐ (t : β) ∂((κ'.fst : (a : α) → Measure β) a : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a, t)
have h_compProd : Eq (α := ℝ≥0∞)
  ((((κ' : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set β) univ (range e))ᶜ :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: have h_compProd : κ' a (univ ×ˢ range e)ᶜ = 0 := by
      unfold κ'
      rw [map_apply' _ (by fun_prop)]
      swap; · exact (MeasurableSet.univ.prod he.measurableSet_range).compl
      suffices Prod.map id e ⁻¹' (univ ×ˢ range e)ᶜ = ∅ by rw [this]; simp
      ext x
      simp
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd :
  Eq (α := ℝ≥0∞)
    ((((κ' : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (α := Set β) univ (range e))ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ ∀ᵐ (t : β) ∂((κ'.fst : (a : α) → Measure β) a : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a, t)
have rw : ∀
  (h_compProd :
    (ae (F := Measure β) ((κ'.fst : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
      (fun (b : β) ↦
        (((η : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ))
      0),
  ∀ᵐ (t : β) ∂((κ'.fst : (a : α) → Measure β) a : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a, t)
Tactic: rw [← hη', compProd_null] at h_compProd
Cleared hypotheses: h_compProd
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd :
  Eq (α := ℝ≥0∞)
    ((((κ' : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (α := Set β) univ (range e))ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
rw :
  ∀
    (h_compProd :
      (ae (F := Measure β) ((κ'.fst : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
        (fun (b : β) ↦
          (((η : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
            (Prod.mk b ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ))
        0),
    ∀ᵐ (t : β) ∂((κ'.fst : (a : α) → Measure β) a : Measure β),
      Membership.mem (γ := Set (α × β))
        {p : α × β |
          Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
            (0 : ℝ≥0∞)}
        (a, t)
⊢ ∀ᵐ (t : β) ∂((κ'.fst : (a : α) → Measure β) a : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a, t)
have hs : ∀
  (h_compProd :
    Eq (α := ℝ≥0∞)
      ((((κ'.fst ⊗ₖ η : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
          (SProd.sprod (α := Set β) univ (range e))ᶜ :
        ℝ≥0∞)
      (0 : ℝ≥0∞)),
  MeasurableSet (SProd.sprod (α := Set β) univ (range e))ᶜ
Tactic: rw [← hη', compProd_null] at h_compProd
Cleared hypotheses: h_compProd
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (hypothesis)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_compProd :
  (ae (F := Measure β) ((κ'.fst : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦
      (((η : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' (SProd.sprod (α := Set β) univ (range e))ᶜ))
    0
⊢ ∀ᵐ (t : β) ∂((κ'.fst : (a : α) → Measure β) a : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a, t)
have h_compProd₁ : (ae (F := Measure β) ((κ'.fst : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
  (fun (b : β) ↦ (((η : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ) 0
Tactic: simp only [preimage_compl, mem_univ, mk_preimage_prod_right] at h_compProd
Cleared hypotheses: h_compProd
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (hypothesis)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
⊢ (ae (F := Measure β) ((κ.fst : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦
      (((borelMarkovFromReal Ω η : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk b ⁻¹' t))
    fun (b : β) ↦
    (((η.comapRight he : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk b ⁻¹' t)
have h_ae : ∀ᵐ (t : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
  Membership.mem (γ := Set (α × β))
    {p : α × β |
      Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
        (0 : ℝ≥0∞)}
    (a, t)
Tactic: have h_ae : ∀ᵐ t ∂(fst κ a), (a, t) ∈ {p : α × β | η p (range e)ᶜ = 0} := by
    rw [← h_fst]
    have h_compProd : κ' a (univ ×ˢ range e)ᶜ = 0 := by
      unfold κ'
      rw [map_apply' _ (by fun_prop)]
      swap; · exact (MeasurableSet.univ.prod he.measurableSet_range).compl
      suffices Prod.map id e ⁻¹' (univ ×ˢ range e)ᶜ = ∅ by rw [this]; simp
      ext x
      simp
    rw [← hη', compProd_null] at h_compProd
    swap; · exact (MeasurableSet.univ.prod he.measurableSet_range).compl
    simp only [preimage_compl, mem_univ, mk_preimage_prod_right] at h_compProd
    exact h_compProd
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_ae :
  ∀ᵐ (t : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a, t)
⊢ (ae (F := Measure β) ((κ.fst : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : β) ↦
      (((borelMarkovFromReal Ω η : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk b ⁻¹' t))
    fun (b : β) ↦
    (((η.comapRight he : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk b ⁻¹' t)
have h : ∀ (a_1 : β)
  (ha :
    Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) (a, a_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
      (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞)
    ((((borelMarkovFromReal Ω η : (a : α × β) → Measure Ω) (a, a_1) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a_1 ⁻¹' t) :
      ℝ≥0∞)
    ((((η.comapRight he : (a : α × β) → Measure Ω) (a, a_1) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk a_1 ⁻¹' t) :
      ℝ≥0∞)
Tactic: filter_upwards [h_ae] with a ha
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a_1 : α
t : Set (β × Ω)
ht : MeasurableSet t
h_ae :
  ∀ᵐ (t : β) ∂((κ.fst : (a : α) → Measure β) a_1 : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a_1, t)
a : β
ha :
  Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((borelMarkovFromReal Ω η : (a : α × β) → Measure Ω) (a_1, a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a ⁻¹' t) :
      ℝ≥0∞)
    ((((η.comapRight he : (a : α × β) → Measure Ω) (a_1, a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
have h : 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_1, a) :
          Measure ℝ) :
        (a : Set ℝ) → ℝ≥0∞)
      (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
    ℝ≥0∞)
  ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
    ℝ≥0∞)
Tactic: rw [borelMarkovFromReal, comapRight_apply', comapRight_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a_1 : α
t : Set (β × Ω)
ht : MeasurableSet t
h_ae :
  ∀ᵐ (t : β) ∂((κ.fst : (a : α) → Measure β) a_1 : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a_1, t)
a : β
ha :
  Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
h :
  Eq (α := ℝ≥0∞)
    ((((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 Ω))) ⋯)
                    ⋯) :
                (a : α × β) → Measure ℝ)
              (a_1, a) :
            Measure ℝ) :
          (a : Set ℝ) → ℝ≥0∞)
        (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((borelMarkovFromReal Ω η : (a : α × β) → Measure Ω) (a_1, a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a ⁻¹' t) :
      ℝ≥0∞)
    ((((η.comapRight he : (a : α × β) → Measure Ω) (a_1, a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (Prod.mk a ⁻¹' t) : ℝ≥0∞)
have h₁ : MeasurableSet (Prod.mk a ⁻¹' t)
Tactic: rw [borelMarkovFromReal, comapRight_apply', comapRight_apply']
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a_1 : α
t : Set (β × Ω)
ht : MeasurableSet t
h_ae :
  ∀ᵐ (t : β) ∂((κ.fst : (a : α) → Measure β) a_1 : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a_1, t)
a : β
ha :
  Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((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 Ω))) ⋯)
                    ⋯) :
                (a : α × β) → Measure ℝ)
              (a_1, a) :
            Measure ℝ) :
          (a : Set ℝ) → ℝ≥0∞)
        (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
      ℝ≥0∞)
have h : Membership.mem (γ := Set (α × β))
  (preimage (β := ℝ≥0∞)
    (fun (a : α × β) ↦ (((η : (a : α × β) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
    {0})
  (a_1, a)
Tactic: rw [piecewise_apply, if_pos]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.StandardBorel (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
inst_1 : Nonempty Ω
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst_3 : IsSFiniteKernel η
hη :
  fst (mγ := Real.measurableSpace) (κ.map (Prod.map id (embeddingReal Ω))) ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := ⋯
κ' : Kernel.{u_1, u_2} α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (α := β × Ω) (Prod.map id e)
h_fst : κ'.fst = κ.fst
a_1 : α
t : Set (β × Ω)
ht : MeasurableSet t
h_ae :
  ∀ᵐ (t : β) ∂((κ.fst : (a : α) → Measure β) a_1 : Measure β),
    Membership.mem (γ := Set (α × β))
      {p : α × β |
        Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
          (0 : ℝ≥0∞)}
      (a_1, t)
a : β
ha :
  Eq (α := ℝ≥0∞) ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range e)ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((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 Ω))) ⋯)
                    ⋯) :
                (a : α × β) → Measure ℝ)
              (a_1, a) :
            Measure ℝ) :
          (a : Set ℝ) → ℝ≥0∞)
        (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
      ℝ≥0∞)
    ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
      ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  (((if
              Membership.mem (γ := Set (α × β))
                (preimage (β := ℝ≥0∞)
                  (fun (a : α × β) ↦
                    (((η : (a : α × β) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (range (embeddingReal Ω))ᶜ)
                  {0})
                (a_1, a) then
            (η : (a : α × β) → Measure ℝ) (a_1, a)
          else
            ((deterministic (fun (x : α × β) ↦ Exists.choose (p := Membership.mem (range (embeddingReal Ω))) sorry) sorry :
                  Kernel (α × β) ℝ) :
                (a : α × β) → Measure ℝ)
              (a_1, a) :
          Measure ℝ) :
        (a : Set ℝ) → ℝ≥0∞)
      (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
    ℝ≥0∞)
  ((((η : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' Prod.mk a ⁻¹' t) :
    ℝ≥0∞)
Tactic: classical
  rw [piecewise_apply, if_pos]
  exact ha