awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 : α
⊢ MeasurableSet (Prod.mk a ⁻¹' s)

Tactic:
measurable_prodMk_left hs

Premises used: measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (embeddingReal Ω ⁻¹' Prod.mk a ⁻¹' s) :
      ℝ≥0∞)

Tactic:
exacts [rfl, measurable_prodMk_left hs]

Premises used: measurable_prodMk_left, rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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
⊢ MeasurableSet (Prod.map id (embeddingReal Ω) ⁻¹' s)

Tactic:
measurable_id.prodMap hf.measurable hs

Premises used: measurable_id, Measurable.prodMap, MeasurableEmbedding.measurable
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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
⊢ MeasurableSet (Prod.map id (embeddingReal Ω) ⁻¹' s)

Tactic:
exact measurable_id.prodMap hf.measurable hs

Premises used: measurable_id, Measurable.prodMap, MeasurableEmbedding.measurable
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 Ω)
symm :
  EventuallyEq.{u_1, u_3} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω)
    (⇑(μ ⊗ₘ κ).condKernel : (a : α) → Measure Ω)
⊢ EventuallyEq.{u_1, u_3} (β := Measure Ω) (ae μ) (⇑(μ ⊗ₘ κ).condKernel : (a : α) → Measure Ω)
    (⇑κ : (a : α) → Measure Ω)

Tactic:
symm
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 Ω)
rwa rwa₁ rwa₂ 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 Ω)
⊢ EventuallyEq.{u_1, u_3} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω)
    (⇑(μ ⊗ₘ κ).condKernel : (a : α) → Measure Ω)

Tactic:
rwa [Measure.fst_compProd] at this

Premises used: MeasureTheory.Measure.fst_compProd
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 κ
suffices :
  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 Ω)

Tactic:
suffices κ =ᵐ[(μ ⊗ₘ κ).fst] (μ ⊗ₘ κ).condKernel by symm; rwa [Measure.fst_compProd] at this
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 Ω)

Tactic:
eq_condKernel_of_measure_eq_compProd _ ?_

Premises used: Filter.EventuallyEq, ProbabilityTheory.eq_condKernel_of_measure_eq_compProd
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 κ
refine : μ ⊗ₘ κ = (μ ⊗ₘ κ).fst ⊗ₘ κ
⊢ EventuallyEq.{u_1, u_3} (β := Measure Ω) (ae (μ ⊗ₘ κ).fst) (⇑κ : (a : α) → Measure Ω)
    (⇑(μ ⊗ₘ κ).condKernel : (a : α) → Measure Ω)

Tactic:
refine eq_condKernel_of_measure_eq_compProd _ ?_

Premises used: ProbabilityTheory.eq_condKernel_of_measure_eq_compProd
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 κ
rw rw₁ : μ ⊗ₘ κ = μ ⊗ₘ κ
⊢ μ ⊗ₘ κ = (μ ⊗ₘ κ).fst ⊗ₘ κ

Tactic:
rw [Measure.fst_compProd]

Premises used: MeasureTheory.Measure.fst_compProd
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 : α
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)) ⋯ :
            (a : Set (β × Ω)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ (ρ : (a : α) → Measure (β × Ω)) a =
    Measure.fst.{u_2, u_3} (β := Ω) ((ρ : (a : α) → Measure (β × Ω)) a) ⊗ₘ κ.comap (fun (b : β) ↦ (a, b)) ⋯

Tactic:
ext s hs
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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
rw : ((((ρ.fst ⊗ₖ κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
| ((((ρ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← hκ]
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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
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)) ⋯ :
          (a : Set (β × Ω)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
⊢ 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∞)

Tactic:
conv_lhs => rw [← hκ]
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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
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)) ⋯ : (a : β) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a_1 ⁻¹' s) ∂Measure.fst.{u_2, u_3} (β := Ω) ((ρ : (a : α) → Measure (β × Ω)) a)
⊢ 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∞)

Tactic:
rw [Measure.compProd_apply hs, Kernel.compProd_apply hs]

Premises used: MeasureTheory.Measure.compProd_apply, ProbabilityTheory.Kernel.compProd_apply
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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
⊢ ∫⁻ (b : β),
      (((κ : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(ρ.fst : (a : α) → Measure β) a =
    ∫⁻ (a_1 : β),
      (((κ.comap (fun (b : β) ↦ (a, b)) ⋯ : (a : β) → Measure Ω) a_1 : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a_1 ⁻¹' s) ∂Measure.fst.{u_2, u_3} (β := Ω) ((ρ : (a : α) → Measure (β × Ω)) a)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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)) ⋯

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
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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)) ⋯
⊢ ∀ᵐ (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 Ω)

Tactic:
have h := eq_condKernel_of_measure_eq_compProd _ this
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 Ω)
h₁ :
  ∀ (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 Ω)
⊢ 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 Ω)

Tactic:
filter_upwards [h] with b hb
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
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 Ω)
h₁ :
  Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a, b) : Measure Ω)
    ((κ.comap (fun (b : β) ↦ (a, b)) ⋯ : (a : β) → Measure Ω) b : Measure Ω)
h₂ h₃ :
  Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a, b) : Measure Ω)
    ((κ : (a : α × β) → Measure Ω) (a, b) : Measure Ω)
⊢ Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a, b) : Measure Ω)
    ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a) : (a : β) → Measure Ω) b : Measure Ω)

Tactic:
rw [← hb, Kernel.comap_apply]

Premises used: ProbabilityTheory.Kernel.comap_apply
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel κ
a : α
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) ((κ.fst : (a : α) → Measure β) a : Measure β))
    (fun (b : β) ↦ (κ.condKernel : (a : α × β) → Measure Ω) (a, b))
    (⇑(Measure.condKernel ((κ : (a : α) → Measure (β × Ω)) a)) : (a : β) → Measure Ω)

Tactic:
Kernel.apply_eq_measure_condKernel_of_compProd_eq (κ.disintegrate _) a

Premises used: ProbabilityTheory.Kernel.apply_eq_measure_condKernel_of_compProd_eq, ProbabilityTheory.Kernel.disintegrate
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
ρ : Measure (β × Ω)
inst_4 : IsFiniteMeasure ρ
a : α
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω)
    (ae (F := Measure β) (((Kernel.fst (Kernel.const α ρ) : Kernel α β) : (a : α) → Measure β) a : Measure β))
    (fun (b : β) ↦ (Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b))
    (⇑(Measure.condKernel ((Kernel.const α ρ : (a : α) → Measure (β × Ω)) a)) : (a : β) → Measure Ω)

Tactic:
have h := Kernel.condKernel_apply_eq_condKernel (Kernel.const α ρ) a
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
ρ : Measure (β × Ω)
inst_4 : IsFiniteMeasure ρ
a : α
h :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map Prod.fst ρ))
    (fun (b : β) ↦ (Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b))
    (⇑ρ.condKernel : (a : β) → Measure Ω)
b : β
hb :
  Eq.{u_3 + 1} (α := Measure Ω) ((Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b) : Measure Ω)
    ((ρ.condKernel : (a : β) → Measure Ω) b : Measure Ω)
⊢ Eq.{u_3 + 1} (α := Measure Ω) ((Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b) : Measure Ω)
    ((ρ.condKernel : (a : β) → Measure Ω) b : Measure Ω)

Tactic:
hb
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
ρ : Measure (β × Ω)
inst_4 : IsFiniteMeasure ρ
a : α
h :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map Prod.fst ρ))
    (fun (b : β) ↦ (Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b))
    (⇑ρ.condKernel : (a : β) → Measure Ω)
h₁ :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq.{u_3 + 1} (α := Measure Ω)
                    ((fun (b : β) ↦
                          ((Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b) : Measure Ω))
                        x :
                      Measure Ω)
                    ((ρ.condKernel : (a : β) → Measure Ω) x : Measure Ω))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq.{u_3 + 1} (α := Measure Ω)
                    ((fun (b : β) ↦
                          ((Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b) : Measure Ω))
                        x :
                      Measure Ω)
                    ((ρ.condKernel : (a : β) → Measure Ω) x : Measure Ω))
                x}
            x}
      a_1
h₂ h₃ :
  ∀ (b : β)
    (hb :
      Eq.{u_3 + 1} (α := Measure Ω)
        ((Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b) : Measure Ω)
        ((ρ.condKernel : (a : β) → Measure Ω) b : Measure Ω)),
    Eq.{u_3 + 1} (α := Measure Ω) ((Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b) : Measure Ω)
      ((ρ.condKernel : (a : β) → Measure Ω) b : Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae ρ.fst)
    (fun (b : β) ↦ (Kernel.condKernel (Kernel.const α ρ) : (a : α × β) → Measure Ω) (a, b))
    (⇑ρ.condKernel : (a : β) → Measure Ω)

Tactic:
filter_upwards [h] with b hb using hb
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
ρ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst_5 : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
h :
  ∀ (a_1 : β)
    (h1 :
      Eq.{u_3 + 1} (α := Measure Ω) ((ρ.condKernel : (a : α × β) → Measure Ω) (a, a_1) : Measure Ω)
        ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a) : (a : β) → Measure Ω) a_1 : Measure Ω))
    (h2 :
      Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a, a_1) : Measure Ω)
        ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a) : (a : β) → Measure Ω) a_1 : Measure Ω)),
    Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a, a_1) : Measure Ω)
      ((ρ.condKernel : (a : α × β) → Measure Ω) (a, a_1) : Measure Ω)
⊢ ∀ᵐ (x : β) ∂((ρ.fst : (a : α) → Measure β) a : Measure β),
    Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a, x) : Measure Ω)
      ((ρ.condKernel : (a : α × β) → Measure Ω) (a, x) : Measure Ω)

Tactic:
filter_upwards [Kernel.condKernel_apply_eq_condKernel ρ a,
    Kernel.apply_eq_measure_condKernel_of_compProd_eq hκ a] with a h1 h2

Premises used: ProbabilityTheory.Kernel.apply_eq_measure_condKernel_of_compProd_eq, ProbabilityTheory.Kernel.condKernel_apply_eq_condKernel
-- Module: Mathlib.Probability.Kernel.Disintegration.Unique
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : CountableOrCountablyGenerated α β
ρ : Kernel α (β × Ω)
inst_4 : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst_5 : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a_1 : α
a : β
h1 :
  Eq.{u_3 + 1} (α := Measure Ω) ((ρ.condKernel : (a : α × β) → Measure Ω) (a_1, a) : Measure Ω)
    ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a_1) : (a : β) → Measure Ω) a : Measure Ω)
h2 h :
  Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a_1, a) : Measure Ω)
    ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a_1) : (a : β) → Measure Ω) a : Measure Ω)
h₁ h₂ :
  Eq.{u_3 + 1} (α := Measure Ω)
    ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a_1) : (a : β) → Measure Ω) a : Measure Ω)
    ((Measure.condKernel ((ρ : (a : α) → Measure (β × Ω)) a_1) : (a : β) → Measure Ω) a : Measure Ω)
⊢ Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α × β) → Measure Ω) (a_1, a) : Measure Ω)
    ((ρ.condKernel : (a : α × β) → Measure Ω) (a_1, a) : Measure Ω)

Tactic:
rw [h1, h2]