awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    ∀ (s : Set ℝ),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) ((((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
          ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have suffices : Eq (α := Measure (α × ℝ)) (Measure.map (Prod.map id f) ρ) (ρ.fst ⊗ₘ ρ.condKernel.map f)
Tactic: suffices ρ.map (Prod.map id f) = (ρ.fst ⊗ₘ (Kernel.map ρ.condKernel f)) by
    rw [← hρ'] at this
    have heq := eq_condKernel_of_measure_eq_compProd_real _ this
    rw [hρ'] at heq
    filter_upwards [heq] with x hx s hs
    rw [← hx, Kernel.map_apply _ hf.measurable, Measure.map_apply hf.measurable hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
⊢ Eq (α := Measure (α × ℝ)) (Measure.map (Prod.map id f) ρ) (ρ.fst ⊗ₘ ρ.condKernel.map f)
have h : ∀ (s : Set (α × ℝ)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((Measure.map (Prod.map id f) ρ : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
    (((ρ.fst ⊗ₘ ρ.condKernel.map f : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
s : Set (α × ℝ)
hs : MeasurableSet s
| (((Measure.map (Prod.map id f) ρ : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
have rw : (((Measure.map (Prod.map id f) (ρ.fst ⊗ₘ ρ.condKernel) : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← ρ.disintegrate ρ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
s : Set (α × ℝ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((Measure.map (Prod.map id f) ρ : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
    (((ρ.fst ⊗ₘ ρ.condKernel.map f : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  (((Measure.map (Prod.map id f) (ρ.fst ⊗ₘ ρ.condKernel) : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
  (((ρ.fst ⊗ₘ ρ.condKernel.map f : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: conv_lhs => rw [← ρ.disintegrate ρ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
s : Set (α × ℝ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (Prod.map id f) (ρ.fst ⊗ₘ ρ.condKernel) : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
    (((ρ.fst ⊗ₘ ρ.condKernel.map f : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (a : α),
    (((ρ.condKernel : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
      (Prod.mk a ⁻¹' Prod.map id (embeddingReal Ω) ⁻¹' s) ∂ρ.fst =
  ∫⁻ (a : α),
    ((((ρ.condKernel.map f : Kernel α ℝ) : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
      (Prod.mk a ⁻¹' s) ∂ρ.fst
Tactic: rw [Measure.compProd_apply hs, Measure.map_apply (measurable_id.prodMap hf.measurable) hs,
    Measure.compProd_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
s : Set (α × ℝ)
hs : MeasurableSet s
h :
  ∫⁻ (a : α),
      (((ρ.condKernel : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a ⁻¹' Prod.map id (embeddingReal Ω) ⁻¹' s) ∂ρ.fst =
    ∫⁻ (a : α),
      ((((ρ.condKernel.map f : Kernel α ℝ) : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk a ⁻¹' s) ∂ρ.fst
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (Prod.map id f) (ρ.fst ⊗ₘ ρ.condKernel) : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
    (((ρ.fst ⊗ₘ ρ.condKernel.map f : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : MeasurableSet (Prod.map id (embeddingReal Ω) ⁻¹' s)
Tactic: rw [Measure.compProd_apply hs, Measure.map_apply (measurable_id.prodMap hf.measurable) hs,
    Measure.compProd_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
s : Set (α × ℝ)
hs : MeasurableSet s
⊢ ∫⁻ (a : α),
      (((ρ.condKernel : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a ⁻¹' Prod.map id (embeddingReal Ω) ⁻¹' s) ∂ρ.fst =
    ∫⁻ (a : α),
      ((((ρ.condKernel.map f : Kernel α ℝ) : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk a ⁻¹' s) ∂ρ.fst
have h : ∀ (a : α),
  Eq (α := ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a ⁻¹' Prod.map id (embeddingReal Ω) ⁻¹' s) :
      ℝ≥0∞)
    (((((ρ.condKernel.map f : Kernel α ℝ) : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk a ⁻¹' s) :
      ℝ≥0∞)
Tactic: congr with a
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
s : Set (α × ℝ)
hs : MeasurableSet s
a : α
⊢ Eq (α := ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a ⁻¹' Prod.map id (embeddingReal Ω) ⁻¹' s) :
      ℝ≥0∞)
    (((((ρ.condKernel.map f : Kernel α ℝ) : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk a ⁻¹' s) :
      ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  ((((ρ.condKernel : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
      (Prod.mk a ⁻¹' Prod.map id (embeddingReal Ω) ⁻¹' s) :
    ℝ≥0∞)
  ((((ρ.condKernel : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (embeddingReal Ω ⁻¹' Prod.mk a ⁻¹' s) :
    ℝ≥0∞)
Tactic: rw [Kernel.map_apply' _ hf.measurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
s : Set (α × ℝ)
hs : MeasurableSet s
a : α
h :
  Eq (α := ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a ⁻¹' Prod.map id (embeddingReal Ω) ⁻¹' s) :
      ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (embeddingReal Ω ⁻¹' Prod.mk a ⁻¹' s) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a ⁻¹' Prod.map id (embeddingReal Ω) ⁻¹' s) :
      ℝ≥0∞)
    (((((ρ.condKernel.map f : Kernel α ℝ) : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk a ⁻¹' s) :
      ℝ≥0∞)
have h₁ : MeasurableSet (Prod.mk a ⁻¹' s)
Tactic: rw [Kernel.map_apply' _ hf.measurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
μ : Measure α
inst_3 : IsFiniteMeasure μ
κ : Kernel α Ω
inst_4 : IsMarkovKernel κ
this :
  EventuallyEq.{u_1, u_3} (β := Measure Ω) (ae (μ ⊗ₘ κ).fst) (⇑κ : (a : α) → Measure Ω)
    (⇑(μ ⊗ₘ κ).condKernel : (a : α) → Measure Ω)
⊢ EventuallyEq.{u_1, u_3} (β := Measure Ω) (ae μ) (⇑(μ ⊗ₘ κ).condKernel : (a : α) → Measure Ω)
    (⇑κ : (a : α) → Measure Ω)
have symm : EventuallyEq.{u_1, u_3} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑(μ ⊗ₘ κ).condKernel : (a : α) → Measure Ω)
Tactic: symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
μ : Measure α
inst_3 : IsFiniteMeasure μ
κ : Kernel α Ω
inst_4 : IsMarkovKernel κ
this :
  EventuallyEq.{u_1, u_3} (β := Measure Ω) (ae (μ ⊗ₘ κ).fst) (⇑κ : (a : α) → Measure Ω)
    (⇑(μ ⊗ₘ κ).condKernel : (a : α) → Measure Ω)
⊢ EventuallyEq.{u_1, u_3} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω)
    (⇑(μ ⊗ₘ κ).condKernel : (a : α) → Measure Ω)
have rwa : ∀
  (this :
    EventuallyEq.{u_1, u_3} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω)
      (⇑(μ ⊗ₘ κ).condKernel : (a : α) → Measure Ω)),
  EventuallyEq.{u_1, u_3} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω)
    (⇑(μ ⊗ₘ κ).condKernel : (a : α) → Measure Ω)
Tactic: rwa [Measure.fst_compProd] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
μ : Measure α
inst_3 : IsFiniteMeasure μ
κ : Kernel α Ω
inst_4 : IsMarkovKernel κ
⊢ EventuallyEq.{u_1, u_3} (β := Measure Ω) (ae μ) (⇑(μ ⊗ₘ κ).condKernel : (a : α) → Measure Ω)
    (⇑κ : (a : α) → Measure Ω)
have suffices : EventuallyEq.{u_1, u_3} (β := Measure Ω) (ae (μ ⊗ₘ κ).fst) (⇑κ : (a : α) → Measure Ω)
  (⇑(μ ⊗ₘ κ).condKernel : (a : α) → Measure Ω)
Tactic: suffices κ =ᵐ[(μ ⊗ₘ κ).fst] (μ ⊗ₘ κ).condKernel by symm; rwa [Measure.fst_compProd] at this
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
μ : Measure α
inst_3 : IsFiniteMeasure μ
κ : Kernel α Ω
inst_4 : IsMarkovKernel κ
⊢ EventuallyEq.{u_1, u_3} (β := Measure Ω) (ae (μ ⊗ₘ κ).fst) (⇑κ : (a : α) → Measure Ω)
    (⇑(μ ⊗ₘ κ).condKernel : (a : α) → Measure Ω)
have refine : μ ⊗ₘ κ = (μ ⊗ₘ κ).fst ⊗ₘ κ
Tactic: refine eq_condKernel_of_measure_eq_compProd _ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
μ : Measure α
inst_3 : IsFiniteMeasure μ
κ : Kernel α Ω
inst_4 : IsMarkovKernel κ
⊢ μ ⊗ₘ κ = (μ ⊗ₘ κ).fst ⊗ₘ κ
have rw : μ ⊗ₘ κ = μ ⊗ₘ κ
Tactic: rw [Measure.fst_compProd]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst_4 : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
⊢ (ρ : (a : α) → Measure (β × Ω)) a =
    Measure.fst.{u_2, u_3} (β := Ω) ((ρ : (a : α) → Measure (β × Ω)) a) ⊗ₘ κ.comap (fun (b : β) ↦ (a, b)) ⋯
have h : ∀ (s : Set (β × Ω)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((ρ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.fst.{u_2, u_3} (β := Ω) ((ρ : (a : α) → Measure (β × Ω)) a) ⊗ₘ κ.comap (fun (b : β) ↦ (a, b)) sorry :
          (a : Set (β × Ω)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst_4 : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
s : Set (β × Ω)
hs : MeasurableSet s
| ((((ρ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ((((ρ.fst ⊗ₖ κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← hκ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst_4 : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
s : Set (β × Ω)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((ρ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.fst.{u_2, u_3} (β := Ω) ((ρ : (a : α) → Measure (β × Ω)) a) ⊗ₘ κ.comap (fun (b : β) ↦ (a, b)) ⋯ :
          (a : Set (β × Ω)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((((ρ.fst ⊗ₖ κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
  ((Measure.fst.{u_2, u_3} (β := Ω) ((ρ : (a : α) → Measure (β × Ω)) a) ⊗ₘ κ.comap (fun (b : β) ↦ (a, b)) sorry :
        (a : Set (β × Ω)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
Tactic: conv_lhs => rw [← hκ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst_4 : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
s : Set (β × Ω)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((ρ.fst ⊗ₖ κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
    ((Measure.fst.{u_2, u_3} (β := Ω) ((ρ : (a : α) → Measure (β × Ω)) a) ⊗ₘ κ.comap (fun (b : β) ↦ (a, b)) ⋯ :
          (a : Set (β × Ω)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h : ∫⁻ (b : β),
    (((κ : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂(ρ.fst : (a : α) → Measure β) a =
  ∫⁻ (a_1 : β),
    (((κ.comap (fun (b : β) ↦ (a, b)) sorry : (a : β) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
      (Prod.mk a_1 ⁻¹' s) ∂Measure.fst.{u_2, u_3} (β := Ω) ((ρ : (a : α) → Measure (β × Ω)) a)
Tactic: rw [Measure.compProd_apply hs, Kernel.compProd_apply hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (hypothesis)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst_4 : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) ((ρ.fst : (a : α) → Measure β) a : Measure β))
    (fun (b : β) ↦ (κ : (a : α × β) → Measure Ω) (a, b))
    (⇑(Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a)) : (a : β) → Measure Ω)
have this : (ρ : (a : α) → Measure (β × Ω)) a =
  Measure.fst.{u_2, u_3} (β := Ω) ((ρ : (a : α) → Measure (β × Ω)) a) ⊗ₘ κ.comap (fun (b : β) ↦ (a, b)) sorry
Tactic: have : ρ a = (ρ a).fst ⊗ₘ Kernel.comap κ (fun b ↦ (a, b)) measurable_prodMk_left := by
    ext s hs
    conv_lhs => rw [← hκ]
    rw [Measure.compProd_apply hs, Kernel.compProd_apply hs]
    rfl
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (hypothesis)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst_4 : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
this :
  (ρ : (a : α) → Measure (β × Ω)) a =
    Measure.fst.{u_2, u_3} (β := Ω) ((ρ : (a : α) → Measure (β × Ω)) a) ⊗ₘ κ.comap (fun (b : β) ↦ (a, b)) ⋯
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) ((ρ.fst : (a : α) → Measure β) a : Measure β))
    (fun (b : β) ↦ (κ : (a : α × β) → Measure Ω) (a, b))
    (⇑(Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a)) : (a : β) → Measure Ω)
have h : ∀ᵐ (x : β) ∂Measure.fst.{u_2, u_3} (β := Ω) ((ρ : (a : α) → Measure (β × Ω)) a),
  Eq.{u_3 + 1} (α := Measure Ω) ((κ.comap (fun (b : β) ↦ (a, b)) sorry : (a : β) → Measure Ω) x : Measure Ω)
    ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a) : (a : β) → Measure Ω) x : Measure Ω)
Tactic: have h := eq_condKernel_of_measure_eq_compProd _ this
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst_4 : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
this :
  (ρ : (a : α) → Measure (β × Ω)) a =
    Measure.fst.{u_2, u_3} (β := Ω) ((ρ : (a : α) → Measure (β × Ω)) a) ⊗ₘ κ.comap (fun (b : β) ↦ (a, b)) ⋯
h :
  ∀ᵐ (x : β) ∂Measure.fst.{u_2, u_3} (β := Ω) ((ρ : (a : α) → Measure (β × Ω)) a),
    Eq.{u_3 + 1} (α := Measure Ω) ((κ.comap (fun (b : β) ↦ (a, b)) ⋯ : (a : β) → Measure Ω) x : Measure Ω)
      ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a) : (a : β) → Measure Ω) x : Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω)
    (ae (F := Measure β) (Measure.map (α := β × Ω) Prod.fst ((ρ : (a : α) → Measure (β × Ω)) a)))
    (fun (b : β) ↦ (κ : (a : α × β) → Measure Ω) (a, b))
    (⇑(Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a)) : (a : β) → Measure Ω)
have h₁ : ∀ (b : β)
  (hb :
    Eq.{u_3 + 1} (α := Measure Ω) ((κ.comap (fun (b : β) ↦ (a, b)) sorry : (a : β) → Measure Ω) b : Measure Ω)
      ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a) : (a : β) → Measure Ω) b : Measure Ω)),
  Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a, b) : Measure Ω)
    ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a) : (a : β) → Measure Ω) b : Measure Ω)
Tactic: filter_upwards [h] with b hb
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Kernel α (β × Ω)
inst_3 : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst_4 : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
this :
  (ρ : (a : α) → Measure (β × Ω)) a =
    Measure.fst.{u_2, u_3} (β := Ω) ((ρ : (a : α) → Measure (β × Ω)) a) ⊗ₘ κ.comap (fun (b : β) ↦ (a, b)) ⋯
h :
  ∀ᵐ (x : β) ∂Measure.fst.{u_2, u_3} (β := Ω) ((ρ : (a : α) → Measure (β × Ω)) a),
    Eq.{u_3 + 1} (α := Measure Ω) ((κ.comap (fun (b : β) ↦ (a, b)) ⋯ : (a : β) → Measure Ω) x : Measure Ω)
      ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a) : (a : β) → Measure Ω) x : Measure Ω)
b : β
hb :
  Eq.{u_3 + 1} (α := Measure Ω) ((κ.comap (fun (b : β) ↦ (a, b)) ⋯ : (a : β) → Measure Ω) b : Measure Ω)
    ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a) : (a : β) → Measure Ω) b : Measure Ω)
⊢ Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a, b) : Measure Ω)
    ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a) : (a : β) → Measure Ω) b : Measure Ω)
have h₁ : Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a, b) : Measure Ω)
  ((κ.comap (fun (b : β) ↦ (a, b)) sorry : (a : β) → Measure Ω) b : Measure Ω)
Tactic: rw [← hb, Kernel.comap_apply]