awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst_1 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    ∀ (f : ℕ → Set ℝ),
      Pairwise (Function.onFun Disjoint f) →
        (∀ (i : ℕ), MeasurableSet (f i)) →
          (∀ (i : ℕ),
              Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i) : ℝ≥0∞)
                ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i) : ℝ≥0∞)) →
            Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
              ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
have h_union : ∀ (x : α) (f : ℕ → Set ℝ) (hdisj : Pairwise (Function.onFun Disjoint f)) (hf : ∀ (i : ℕ), MeasurableSet (f i))
  (heq :
    ∀ (i : ℕ),
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i) : ℝ≥0∞)
        ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i) : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
Tactic: refine ae_of_all _ (fun x f hdisj hf heq ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst_1 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞)
x : α
f : ℕ → Set ℝ
hdisj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
heq :
  ∀ (i : ℕ),
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i) : ℝ≥0∞)
      ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
have h_union : Eq (α := ℝ≥0∞) (∑' (i : ℕ), (((κ : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i))
  (∑' (i : ℕ), (((ρ.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (f i))
Tactic: rw [measure_iUnion hdisj hf, measure_iUnion hdisj hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (hypothesis)
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 Ω
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) x : Measure Ω)
      ((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω)
have hf : MeasurableEmbedding (embeddingReal Ω)
Tactic: have hf := measurableEmbedding_embeddingReal Ω
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (hypothesis)
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 Ω)
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) x : Measure Ω)
      ((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω)
have hρ'def : let ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ;
ρ' = Measure.map (Prod.map id f) ρ
Tactic: set ρ' : Measure (α × ℝ) := ρ.map (Prod.map id f) with hρ'def
-- 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) ρ
⊢ ρ'.fst = ρ.fst
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((ρ'.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ.fst : (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) ρ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((ρ'.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × Ω)) → ℝ≥0∞) (Prod.map id f ⁻¹' Prod.fst ⁻¹' s) : ℝ≥0∞)
  ((ρ : (a : Set (α × Ω)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
Tactic: rw [hρ'def, Measure.fst_apply, Measure.fst_apply, Measure.map_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) ρ
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∞)
⊢ Eq (α := ℝ≥0∞) ((ρ'.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Measurable (α := α × Ω) (Prod.map id f)
Tactic: rw [hρ'def, Measure.fst_apply, Measure.fst_apply, Measure.map_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) ρ
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)
⊢ Eq (α := ℝ≥0∞) ((ρ'.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : MeasurableSet (α := α × ℝ) (Prod.fst ⁻¹' s)
Tactic: rw [hρ'def, Measure.fst_apply, Measure.fst_apply, Measure.map_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (hypothesis)
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) ρ
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) x : Measure Ω)
      ((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω)
have hρ' : ρ'.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]
-- 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
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
have rw : ∀ᵐ (x : α) ∂ρ'.fst,
  Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
    ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
Tactic: rw [← hρ']
-- 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
⊢ ∀ᵐ (x : α) ∂ρ'.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
have refine : ρ' = ρ'.fst ⊗ₘ κ.map f
Tactic: refine eq_condKernel_of_measure_eq_compProd_real (Kernel.map κ f) ?_
-- 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
⊢ ρ' = ρ'.fst ⊗ₘ κ.map f
have h : ∀ (s : Set (α × ℝ)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((ρ' : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
    (((ρ'.fst ⊗ₘ κ.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
s : Set (α × ℝ)
hs : MeasurableSet s
| ((ρ' : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
have rw : (((Measure.map (Prod.map id f) (ρ.fst ⊗ₘ κ) : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [hρ'def, hκ]
-- 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
s : Set (α × ℝ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((ρ' : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
    (((ρ'.fst ⊗ₘ κ.map f : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
Tactic: conv_lhs => rw [hρ'def, hκ]
-- 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
s : Set (α × ℝ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((Measure.map (Prod.map id f) (ρ.fst ⊗ₘ κ) : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
    (((ρ'.fst ⊗ₘ κ.map f : Measure (α × ℝ)) : (a : Set (α × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
have 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
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)]
-- 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
s : Set (α × ℝ)
hs : MeasurableSet s
⊢ ∫⁻ (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
have 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∞)
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
s : Set (α × ℝ)
hs : MeasurableSet s
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∞)
have 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∞)
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
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∞)
⊢ 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∞)
have h₁ : MeasurableSet (Prod.mk a ⁻¹' s)
Tactic: rw [Kernel.map_apply' _ hf.measurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (hypothesis)
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.{u_3 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) x : Measure Ω)
      ((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω)
have hρ'' : ∀ᵐ (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]
-- 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 ℝ)
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 : α) ∂ρ.fst,
    Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) x : Measure Ω)
      ((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω)
have 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 Ω)
Tactic: filter_upwards [hρ'', this] with x hx h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (hypothesis)
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.{u_3 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) x : Measure Ω)
    ((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω)
have hx₁ : Eq (α := Measure ℝ) (Measure.map (embeddingReal Ω) ((κ : (a : α) → Measure Ω) x))
  ((ρ'.condKernel : (a : α) → Measure ℝ) x)
Tactic: rw [Kernel.map_apply _ hf.measurable] at hx
Cleared hypotheses: hx, h
-- 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 ℝ)
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∞)
⊢ Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) x : Measure Ω)
    ((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω)
have 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∞)
Tactic: ext s hs