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 ℝ)
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 ℝ) (Measure.map (embeddingReal Ω) ((κ : (a : α) → Measure Ω) x))
    ((ρ'.condKernel : (a : α) → Measure ℝ) x)
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∞)
h₁ :
  ∀ (s : Set Ω) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) x : Measure Ω)
    ((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω)

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
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 ℝ) (Measure.map (embeddingReal Ω) ((κ : (a : α) → Measure Ω) x))
    ((ρ'.condKernel : (a : α) → Measure ℝ) x)
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∞)
s : Set Ω
hs : MeasurableSet s
h₁ :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (embeddingReal Ω ⁻¹' embeddingReal Ω '' s) : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (embeddingReal Ω ⁻¹' embeddingReal Ω '' s) :
      ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞)
    ((Measure.map (embeddingReal Ω) ((κ : (a : α) → Measure Ω) x) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s) : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (embeddingReal Ω ⁻¹' embeddingReal Ω '' s) :
      ℝ≥0∞)
h₃ :
  Eq (α := ℝ≥0∞)
    ((((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (embeddingReal Ω '' s) : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (embeddingReal Ω ⁻¹' embeddingReal Ω '' s) :
      ℝ≥0∞)
h₄ h₅ :
  Eq (α := ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' embeddingReal Ω '' s) : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (embeddingReal Ω ⁻¹' embeddingReal Ω '' s) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← Set.preimage_image_eq s hf.injective,
      ← Measure.map_apply hf.measurable <| hf.measurableSet_image.2 hs, hx,
      h _ <| hf.measurableSet_image.2 hs]

Premises used: Iff.mpr, MeasurableEmbedding.measurableSet_image, MeasureTheory.Measure.map_apply, MeasurableEmbedding.injective, Set.preimage_image_eq, 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 ℝ)
suffices :
  ∀ᵐ (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 : α) ∂ρ.fst,
    Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) x : Measure Ω)
      ((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω)

Tactic:
suffices ∀ᵐ x ∂ρ.fst, ∀ s, MeasurableSet s → ρ'.condKernel x s = ρ.condKernel x (f ⁻¹' s) by
    filter_upwards [hρ'', this] with x hx h
    rw [Kernel.map_apply _ hf.measurable] at hx
    ext s hs
    rw [← Set.preimage_image_eq s hf.injective,
      ← Measure.map_apply hf.measurable <| hf.measurableSet_image.2 hs, hx,
      h _ <| hf.measurableSet_image.2 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 : Eq (α := Measure (α × ℝ)) (Measure.map (Prod.map id f) ρ) (ρ.fst ⊗ₘ ρ.condKernel.map f)
⊢ Eq (α := Measure (α × ℝ)) (Measure.map (Prod.map id f) ρ) (ρ'.fst ⊗ₘ ρ.condKernel.map f)

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

Tactic:
have heq := eq_condKernel_of_measure_eq_compProd_real _ 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 : 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 : Eq (α := Measure (α × ℝ)) (Measure.map (Prod.map id f) ρ) (ρ'.fst ⊗ₘ ρ.condKernel.map f)
heq :
  ∀ᵐ (x : α) ∂Measure.fst (Measure.map (Prod.map id f) ρ),
    Eq (α := Measure ℝ) (((ρ.condKernel.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      (((Measure.condKernel (Measure.map (Prod.map id f) ρ) : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((ρ.condKernel.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      (((Measure.condKernel (Measure.map (Prod.map id f) ρ) : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)

Tactic:
rw [hρ'] at heq
-- 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 : Eq (α := Measure (α × ℝ)) (Measure.map (Prod.map id f) ρ) (ρ'.fst ⊗ₘ ρ.condKernel.map f)
heq :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((ρ.condKernel.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      (((Measure.condKernel (Measure.map (Prod.map id f) ρ) : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
h :
  ∀ (x : α)
    (hx :
      Eq (α := Measure ℝ) (((ρ.condKernel.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
        (((Measure.condKernel (Measure.map (Prod.map id f) ρ) : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ))
    (s : Set ℝ) (hs : 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 : α) ∂ρ.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∞)

Tactic:
filter_upwards [heq] with x hx 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
hρ'' :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
this : Eq (α := Measure (α × ℝ)) (Measure.map (Prod.map id f) ρ) (ρ'.fst ⊗ₘ ρ.condKernel.map f)
heq :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((ρ.condKernel.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      (((Measure.condKernel (Measure.map (Prod.map id f) ρ) : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
x : α
hx :
  Eq (α := Measure ℝ) (((ρ.condKernel.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
    (((Measure.condKernel (Measure.map (Prod.map id f) ρ) : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
s : Set ℝ
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    (((((ρ.condKernel.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.map (embeddingReal Ω) ((ρ.condKernel : (a : α) → Measure Ω) x) : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
h₂ h₃ :
  Eq (α := ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (embeddingReal Ω ⁻¹' s) : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
⊢ 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 [← hx, Kernel.map_apply _ hf.measurable, Measure.map_apply hf.measurable hs]

Premises used: ProbabilityTheory.Kernel.map_apply, MeasureTheory.Measure.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 ℝ)
suffices : Eq (α := Measure (α × ℝ)) (Measure.map (Prod.map id f) ρ) (ρ.fst ⊗ₘ ρ.condKernel.map f)
⊢ ∀ᵐ (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∞)

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

Tactic:
rw [← ρ.disintegrate ρ.condKernel]

Premises used: MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate
-- 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
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∞)
⊢ 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:
conv_lhs => rw [← ρ.disintegrate ρ.condKernel]

Premises used: MeasureTheory.Measure.condKernel, MeasureTheory.Measure.disintegrate
-- 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
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
h₁ : MeasurableSet (Prod.map id (embeddingReal Ω) ⁻¹' 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∞)

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

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
hρ'' :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
s : Set (α × ℝ)
hs : MeasurableSet s
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∞)
⊢ ∫⁻ (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:
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
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∞)
h₁ : MeasurableSet (Prod.mk a ⁻¹' s)
⊢ 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:
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
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:
rfl

Premises used: Set.Mem, setOf, MeasureTheory.embeddingReal, Prod.map, Set.preimage, Classical.choose, rfl