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) ρ
s : Set α
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × Ω)) → ℝ≥0∞) (Prod.map id f ⁻¹' Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((ρ : (a : Set (α × Ω)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
h₁ : Measurable (α := α × Ω) (Prod.map id f)
h₂ : MeasurableSet (α := α × ℝ) (Prod.fst ⁻¹' s)
h₃ h₄ : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((ρ'.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [hρ'def, Measure.fst_apply, Measure.fst_apply, Measure.map_apply]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.fst_apply
-- 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) ρ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × Ω)) → ℝ≥0∞) (Prod.map id f ⁻¹' Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((ρ : (a : Set (α × Ω)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)

Tactic:
rfl

Premises used: Set.Mem, setOf, Prod.map, Set.preimage, 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) ρ
s : Set α
hs : MeasurableSet s
⊢ Measurable (α := α × Ω) (Prod.map id f)

Tactic:
Measurable.prod measurable_fst <| hf.measurable.comp measurable_snd

Premises used: Measurable.comp, measurable_snd, MeasurableEmbedding.measurable, Measurable.prod, measurable_fst
-- 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) ρ
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (α := α × ℝ) (Prod.fst ⁻¹' s)

Tactic:
measurable_fst hs

Premises used: measurable_fst
-- 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) ρ
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
hs
-- 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) ρ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × Ω)) → ℝ≥0∞) (Prod.map id f ⁻¹' Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((ρ : (a : Set (α × Ω)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)

Tactic:
exacts [rfl, Measurable.prod measurable_fst <| hf.measurable.comp measurable_snd,
      measurable_fst hs, hs, hs]

Premises used: Measurable.comp, measurable_snd, MeasurableEmbedding.measurable, Measurable.prod, measurable_fst, 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) ρ
⊢ ρ'.fst = ρ.fst

Tactic:
have hρ' : ρ'.fst = ρ.fst := by
    ext s hs
    rw [hρ'def, Measure.fst_apply, Measure.fst_apply, Measure.map_apply]
    exacts [rfl, Measurable.prod measurable_fst <| hf.measurable.comp measurable_snd,
      measurable_fst hs, hs, hs]
-- 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
rw :
  ∀ᵐ (x : α) ∂ρ'.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)

Tactic:
rw [← hρ']
-- 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
⊢ ∀ᵐ (x : α) ∂ρ'.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)

Tactic:
eq_condKernel_of_measure_eq_compProd_real (Kernel.map κ f) ?_

Premises used: ProbabilityTheory.Kernel.map, ProbabilityTheory.eq_condKernel_of_measure_eq_compProd_real
-- 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
refine : ρ' = ρ'.fst ⊗ₘ κ.map f
⊢ ∀ᵐ (x : α) ∂ρ'.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)

Tactic:
refine eq_condKernel_of_measure_eq_compProd_real (Kernel.map κ f) ?_

Premises used: ProbabilityTheory.Kernel.map, ProbabilityTheory.eq_condKernel_of_measure_eq_compProd_real
-- 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 :
  ∀ (s : Set (α × ℝ)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((ρ' : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
      (((ρ'.fst ⊗ₘ κ.map f : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ρ' = ρ'.fst ⊗ₘ κ.map f

Tactic:
ext s hs
-- 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
s : Set (α × ℝ)
hs : MeasurableSet s
rw : (((Measure.map (Prod.map id f) (ρ.fst ⊗ₘ κ) : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
| ((ρ' : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [hρ'def, hκ]
-- 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
s : Set (α × ℝ)
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((Measure.map (Prod.map id f) (ρ.fst ⊗ₘ κ) : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
    (((ρ'.fst ⊗ₘ κ.map f : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ' : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
    (((ρ'.fst ⊗ₘ κ.map f : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
conv_lhs => rw [hρ'def, hκ]
-- 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
s : Set (α × ℝ)
hs : MeasurableSet s
h :
  ∫⁻ (a : α),
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a ⁻¹' Prod.map id (embeddingReal Ω) ⁻¹' s) ∂ρ.fst =
    ∫⁻ (a : α),
      ((((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂ρ.fst
⊢ Eq (α := ℝ≥0∞) (((Measure.map (Prod.map id f) (ρ.fst ⊗ₘ κ) : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
    (((ρ'.fst ⊗ₘ κ.map f : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Measure.map_apply (measurable_id.prodMap hf.measurable) hs, hρ',
      Measure.compProd_apply hs, Measure.compProd_apply (measurable_id.prodMap hf.measurable hs)]

Premises used: MeasureTheory.Measure.map_apply, measurable_id, MeasureTheory.Measure.compProd_apply, 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
s : Set (α × ℝ)
hs : MeasurableSet s
h :
  ∀ (a : α),
    Eq (α := ℝ≥0∞)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (Prod.mk a ⁻¹' Prod.map id (embeddingReal Ω) ⁻¹' s) :
        ℝ≥0∞)
      (((((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)
⊢ ∫⁻ (a : α),
      (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a ⁻¹' Prod.map id (embeddingReal Ω) ⁻¹' s) ∂ρ.fst =
    ∫⁻ (a : α),
      ((((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂ρ.fst

Tactic:
congr with a
-- 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
s : Set (α × ℝ)
hs : MeasurableSet s
a : α
h :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a ⁻¹' Prod.map id (embeddingReal Ω) ⁻¹' s) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (embeddingReal Ω ⁻¹' Prod.mk a ⁻¹' s) : ℝ≥0∞)
h₁ : MeasurableSet (Prod.mk a ⁻¹' s)
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a ⁻¹' Prod.map id (embeddingReal Ω) ⁻¹' s) :
      ℝ≥0∞)
    (((((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) a : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (Prod.mk a ⁻¹' s) : ℝ≥0∞)

Tactic:
rw [Kernel.map_apply' _ hf.measurable]

Premises used: ProbabilityTheory.Kernel.map_apply', 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
s : Set (α × ℝ)
hs : MeasurableSet s
a : α
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a ⁻¹' Prod.map id (embeddingReal Ω) ⁻¹' s) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (embeddingReal Ω ⁻¹' Prod.mk a ⁻¹' s) : ℝ≥0∞)

Tactic:
rfl

Premises used: Set.Mem, setOf, MeasureTheory.embeddingReal, Prod.map, Set.preimage, Classical.choose, 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
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
s : Set (α × ℝ)
hs : MeasurableSet s
a : α
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (Prod.mk a ⁻¹' Prod.map id (embeddingReal Ω) ⁻¹' s) :
      ℝ≥0∞)
    ((((κ : (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
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)

Tactic:
have hρ'' : ∀ᵐ x ∂ρ.fst, Kernel.map κ f x = ρ'.condKernel x := by
    rw [← hρ']
    refine eq_condKernel_of_measure_eq_compProd_real (Kernel.map κ f) ?_
    ext s hs
    conv_lhs => rw [hρ'def, hκ]
    rw [Measure.map_apply (measurable_id.prodMap hf.measurable) hs, hρ',
      Measure.compProd_apply hs, Measure.compProd_apply (measurable_id.prodMap hf.measurable hs)]
    congr with a
    rw [Kernel.map_apply' _ hf.measurable]
    exacts [rfl, measurable_prodMk_left hs]
-- 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 ℝ)
this :
  ∀ᵐ (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∞)
h :
  ∀ (x : α)
    (hx :
      Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
        ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ))
    (h :
      ∀ (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∞)),
    Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) x : Measure Ω)
      ((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω)
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) x : Measure Ω)
      ((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω)

Tactic:
filter_upwards [hρ'', this] with x hx h
-- 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 ℝ)
this :
  ∀ᵐ (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∞)
x : α
hx :
  Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
    ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
h :
  ∀ (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∞)
⊢ Eq (α := Measure ℝ) (Measure.map (embeddingReal Ω) ((κ : (a : α) → Measure Ω) x))
    ((ρ'.condKernel : (a : α) → Measure ℝ) x)

Tactic:
rw [Kernel.map_apply _ hf.measurable] at hx

Premises used: ProbabilityTheory.Kernel.map_apply, 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 ℝ)
this :
  ∀ᵐ (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∞)
x : α
hx :
  Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
    ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
h :
  ∀ (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∞)
hx₁ :
  Eq (α := Measure ℝ) (Measure.map (embeddingReal Ω) ((κ : (a : α) → Measure Ω) x))
    ((ρ'.condKernel : (a : α) → Measure ℝ) x)
⊢ ∀ (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∞)

Tactic:
rw [Kernel.map_apply _ hf.measurable] at hx

Premises used: ProbabilityTheory.Kernel.map_apply, MeasurableEmbedding.measurable