awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
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
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
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]
-- 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∞)
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∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
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]
-- 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∞)
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∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
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]
-- 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∞)
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∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    Eq.{u_3 + 1} (α := Measure Ω) ((κ : (a : α) → Measure Ω) x : Measure Ω)
      ((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω)
have 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∞)
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]
-- 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 : 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∞)
have this₁ : Eq (α := Measure (α × ℝ)) (Measure.map (Prod.map id f) ρ) (ρ'.fst ⊗ₘ ρ.condKernel.map f)
Tactic: rw [← hρ'] at this
Cleared hypotheses: this
-- 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 : 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∞)
have 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 ℝ)
Tactic: have heq := eq_condKernel_of_measure_eq_compProd_real _ this
-- 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 : 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,
    ∀ (s : Set ℝ),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) ((((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
          ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have 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 ℝ)
Tactic: rw [hρ'] at heq
Cleared hypotheses: heq
-- 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 : 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 : α) ∂ρ.fst,
    ∀ (s : Set ℝ),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) ((((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
          ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have 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∞)
Tactic: filter_upwards [heq] with x hx s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
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
⊢ Eq (α := ℝ≥0∞) ((((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have 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∞)
Tactic: rw [← hx, Kernel.map_apply _ hf.measurable, Measure.map_apply hf.measurable hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
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∞)
⊢ Eq (α := ℝ≥0∞) ((((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have 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∞)
Tactic: rw [← hx, Kernel.map_apply _ hf.measurable, Measure.map_apply hf.measurable hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Unique (goal)
Goal:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (α × Ω)
inst_3 : IsFiniteMeasure ρ
κ : Kernel α Ω
inst_4 : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' :
  ∀ᵐ (x : α) ∂ρ.fst,
    Eq (α := Measure ℝ) (((κ.map f : Kernel α ℝ) : (a : α) → Measure ℝ) x : Measure ℝ)
      ((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ)
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∞)
⊢ Eq (α := ℝ≥0∞) ((((ρ'.condKernel : (a : α) → Measure ℝ) x : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
    ((((ρ.condKernel : (a : α) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have 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∞)
Tactic: rw [← hx, Kernel.map_apply _ hf.measurable, Measure.map_apply hf.measurable hs]