awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
⊢ Measure.map X μ ⊗ₘ κ = Measure.map (AEMeasurable.mk X hX) μ ⊗ₘ κ
have pos : Measure.map (AEMeasurable.mk X hX) μ ⊗ₘ κ = Measure.map (AEMeasurable.mk X hX) μ ⊗ₘ κ
Tactic: rw [Measure.map_congr hX.ae_eq_mk]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
      (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω) ↔
    Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
have refine : ∀
  (h :
    EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
      (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)),
  Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
Tactic: refine ⟨fun h ↦ ?_, condDistrib_ae_eq_of_measure_eq_compProd X hY⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
h :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
⊢ Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
have rw : Eq (α := Measure (β × Ω)) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ) (Measure.map X μ ⊗ₘ condDistrib Y X μ)
Tactic: rw [Measure.compProd_congr h.symm, compProd_map_condDistrib hY]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
h :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
rw : Eq (α := Measure (β × Ω)) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ) (Measure.map X μ ⊗ₘ condDistrib Y X μ)
⊢ Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
have rw₁ : Eq (α := Measure (β × Ω)) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
Tactic: rw [Measure.compProd_congr h.symm, compProd_map_condDistrib hY]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst_4 : StandardBorelSpace Ω'
inst_5 : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
⊢ EventuallyEq.{u_2, u_5} (β := Measure Ω') (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib (f ∘ Y) X μ) : (a : β) → Measure Ω')
    (⇑(Kernel.map (mβ := inst) (condDistrib Y X μ) f) : (a : β) → Measure Ω')
have pos : ∀ (hX : AEMeasurable X μ),
  EventuallyEq.{u_2, u_5} (β := Measure Ω') (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib (f ∘ Y) X μ) : (a : β) → Measure Ω')
    (⇑(Kernel.map (mβ := inst) (condDistrib Y X μ) f) : (a : β) → Measure Ω')
Tactic: by_cases hX : AEMeasurable X μ
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst_4 : StandardBorelSpace Ω'
inst_5 : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
pos :
  ∀ (hX : AEMeasurable X μ),
    EventuallyEq.{u_2, u_5} (β := Measure Ω') (ae (F := Measure β) (Measure.map X μ))
      (⇑(condDistrib (f ∘ Y) X μ) : (a : β) → Measure Ω')
      (⇑(Kernel.map (mβ := inst) (condDistrib Y X μ) f) : (a : β) → Measure Ω')
⊢ EventuallyEq.{u_2, u_5} (β := Measure Ω') (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib (f ∘ Y) X μ) : (a : β) → Measure Ω')
    (⇑(Kernel.map (mβ := inst) (condDistrib Y X μ) f) : (a : β) → Measure Ω')
have neg : ∀ (hX : ¬AEMeasurable X μ),
  EventuallyEq.{u_2, u_5} (β := Measure Ω') (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib (f ∘ Y) X μ) : (a : β) → Measure Ω')
    (⇑(Kernel.map (mβ := inst) (condDistrib Y X μ) f) : (a : β) → Measure Ω')
Tactic: by_cases hX : AEMeasurable X μ
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst_4 : StandardBorelSpace Ω'
inst_5 : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : AEMeasurable X μ
⊢ EventuallyEq.{u_2, u_5} (β := Measure Ω') (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib (f ∘ Y) X μ) : (a : β) → Measure Ω')
    (⇑(Kernel.map (mβ := inst) (condDistrib Y X μ) f) : (a : β) → Measure Ω')
have pos : Eq (α := Measure (β × Ω')) (Measure.map (fun (x : α) ↦ (X x, (f ∘ Y) x)) μ)
  (Measure.map X μ ⊗ₘ Kernel.map (mβ := inst) (condDistrib Y X μ) f)
Tactic: refine condDistrib_ae_eq_of_measure_eq_compProd X (by fun_prop) ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst_4 : StandardBorelSpace Ω'
inst_5 : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : AEMeasurable X μ
⊢ Eq (α := Measure (β × Ω')) (Measure.map (fun (x : α) ↦ (X x, (f ∘ Y) x)) μ)
    (Measure.map (Prod.map id f) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
have rw : Eq (α := Measure (β × Ω')) (Measure.map (fun (x : α) ↦ (X x, (f ∘ Y) x)) μ)
  (Measure.map (Prod.map id f ∘ fun (x : α) ↦ (X x, Y x)) μ)
Tactic: rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst_4 : StandardBorelSpace Ω'
inst_5 : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : AEMeasurable X μ
⊢ Eq (α := Measure (β × Ω')) (Measure.map (Prod.map id f) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
    (Measure.map (Prod.map id f) (Measure.map X μ ⊗ₘ condDistrib Y X μ))
have rw : Eq (α := Measure (β × Ω')) (Measure.map (Prod.map id f) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
  (Measure.map (Prod.map id f) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ))
Tactic: rw [compProd_map_condDistrib hY]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst_4 : StandardBorelSpace Ω'
inst_5 : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : AEMeasurable X μ
⊢ Eq (α := Measure (β × Ω')) (Measure.map (Prod.map id f) (Measure.map X μ ⊗ₘ condDistrib Y X μ))
    (Measure.map X μ ⊗ₘ Kernel.map (mβ := inst) (condDistrib Y X μ) f)
have rw : Eq (α := Measure (β × Ω')) (Measure.map (Prod.map id f) (Measure.map X μ ⊗ₘ condDistrib Y X μ))
  (Measure.map (Prod.map id f) (Measure.map X μ ⊗ₘ condDistrib Y X μ))
Tactic: rw [Measure.compProd_map hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst_4 : StandardBorelSpace Ω'
inst_5 : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : AEMeasurable X μ
⊢ Eq (α := Measure (β × Ω')) (Measure.map (fun (x : α) ↦ (X x, (f ∘ Y) x)) μ)
    (Measure.map X μ ⊗ₘ Kernel.map (mβ := inst) (condDistrib Y X μ) f)
have calc : Eq (α := Measure (β × Ω')) (Measure.map (fun (x : α) ↦ (X x, (f ∘ Y) x)) μ)
  (Measure.map (Prod.map id f) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
Tactic: calc μ.map (fun x ↦ (X x, (f ∘ Y) x))
  _ = (μ.map (fun x ↦ (X x, Y x))).map (Prod.map id f) := by
    rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
    simp [Function.comp_def]
  _ = (μ.map X ⊗ₘ condDistrib Y X μ).map (Prod.map id f) := by rw [compProd_map_condDistrib hY]
  _ = μ.map X ⊗ₘ (condDistrib Y X μ).map f := by rw [Measure.compProd_map hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst_4 : StandardBorelSpace Ω'
inst_5 : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : AEMeasurable X μ
calc :
  Eq (α := Measure (β × Ω')) (Measure.map (fun (x : α) ↦ (X x, (f ∘ Y) x)) μ)
    (Measure.map (Prod.map id f) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
⊢ Eq (α := Measure (β × Ω')) (Measure.map (fun (x : α) ↦ (X x, (f ∘ Y) x)) μ)
    (Measure.map X μ ⊗ₘ Kernel.map (mβ := inst) (condDistrib Y X μ) f)
have calc₁ : Eq (α := Measure (β × Ω')) (Measure.map (Prod.map id f) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
  (Measure.map (Prod.map id f) (Measure.map X μ ⊗ₘ condDistrib Y X μ))
Tactic: calc μ.map (fun x ↦ (X x, (f ∘ Y) x))
  _ = (μ.map (fun x ↦ (X x, Y x))).map (Prod.map id f) := by
    rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
    simp [Function.comp_def]
  _ = (μ.map X ⊗ₘ condDistrib Y X μ).map (Prod.map id f) := by rw [compProd_map_condDistrib hY]
  _ = μ.map X ⊗ₘ (condDistrib Y X μ).map f := by rw [Measure.compProd_map hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst_4 : StandardBorelSpace Ω'
inst_5 : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : AEMeasurable X μ
calc :
  Eq (α := Measure (β × Ω')) (Measure.map (fun (x : α) ↦ (X x, (f ∘ Y) x)) μ)
    (Measure.map (Prod.map id f) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
calc₁ :
  Eq (α := Measure (β × Ω')) (Measure.map (Prod.map id f) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
    (Measure.map (Prod.map id f) (Measure.map X μ ⊗ₘ condDistrib Y X μ))
⊢ Eq (α := Measure (β × Ω')) (Measure.map (fun (x : α) ↦ (X x, (f ∘ Y) x)) μ)
    (Measure.map X μ ⊗ₘ Kernel.map (mβ := inst) (condDistrib Y X μ) f)
have calc₂ : Eq (α := Measure (β × Ω')) (Measure.map (Prod.map id f) (Measure.map X μ ⊗ₘ condDistrib Y X μ))
  (Measure.map X μ ⊗ₘ Kernel.map (mβ := inst) (condDistrib Y X μ) f)
Tactic: calc μ.map (fun x ↦ (X x, (f ∘ Y) x))
  _ = (μ.map (fun x ↦ (X x, Y x))).map (Prod.map id f) := by
    rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
    simp [Function.comp_def]
  _ = (μ.map X ⊗ₘ condDistrib Y X μ).map (Prod.map id f) := by rw [compProd_map_condDistrib hY]
  _ = μ.map X ⊗ₘ (condDistrib Y X μ).map f := by rw [Measure.compProd_map hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
f : β → Ω
hf : Measurable f
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib (f ∘ X) X μ) : (a : β) → Measure Ω) (⇑(Kernel.deterministic f hf) : (a : β) → Measure Ω)
have pos : ∀ (hX : AEMeasurable X μ),
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib (f ∘ X) X μ) : (a : β) → Measure Ω) (⇑(Kernel.deterministic f hf) : (a : β) → Measure Ω)
Tactic: by_cases hX : AEMeasurable X μ
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
f : β → Ω
hf : Measurable f
pos :
  ∀ (hX : AEMeasurable X μ),
    EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
      (⇑(condDistrib (f ∘ X) X μ) : (a : β) → Measure Ω) (⇑(Kernel.deterministic f hf) : (a : β) → Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib (f ∘ X) X μ) : (a : β) → Measure Ω) (⇑(Kernel.deterministic f hf) : (a : β) → Measure Ω)
have neg : ∀ (hX : ¬AEMeasurable X μ),
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib (f ∘ X) X μ) : (a : β) → Measure Ω) (⇑(Kernel.deterministic f hf) : (a : β) → Measure Ω)
Tactic: by_cases hX : AEMeasurable X μ
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
f : β → Ω
hf : Measurable f
hX : AEMeasurable X μ
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib (f ∘ X) X μ) : (a : β) → Measure Ω) (⇑(Kernel.deterministic f hf) : (a : β) → Measure Ω)
have pos : Measure.map (fun (x : α) ↦ (X x, (f ∘ X) x)) μ = Measure.map X μ ⊗ₘ Kernel.deterministic f hf
Tactic: refine condDistrib_ae_eq_of_measure_eq_compProd X (by fun_prop) ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
f : β → Ω
hf : Measurable f
hX : AEMeasurable X μ
⊢ Measure.map (fun (x : α) ↦ (X x, (f ∘ X) x)) μ = Measure.map X μ ⊗ₘ Kernel.deterministic f hf
have pos : Eq (α := Measure (β × Ω)) (Measure.map (fun (x : α) ↦ (X x, (f ∘ X) x)) μ)
  (Measure.map ((fun (a : β) ↦ (a, f a)) ∘ X) μ)
Tactic: rw [Measure.compProd_deterministic, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (hypothesis)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
c : Ω
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib (fun (x : α) ↦ c) X μ) : (a : β) → Measure Ω)
    (⇑(Kernel.deterministic (fun (x : β) ↦ c) ⋯) : (a : β) → Measure Ω)
have this : Eq (α := α → Ω) (fun (x : α) ↦ c) ((fun (x : β) ↦ c) ∘ X)
Tactic: have : (fun _ : α ↦ c) = (fun _ : β ↦ c) ∘ X := rfl
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
c : Ω
this : Eq (α := α → Ω) (fun (x : α) ↦ c) ((fun (x : β) ↦ c) ∘ X)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib (fun (x : α) ↦ c) X μ) : (a : β) → Measure Ω)
    (⇑(Kernel.deterministic (fun (x : β) ↦ c) ⋯) : (a : β) → Measure Ω)
have rw : EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
  (⇑(condDistrib ((fun (x : β) ↦ c) ∘ X) X μ) : (a : β) → Measure Ω)
  (⇑(Kernel.deterministic (fun (x : β) ↦ c) sorry) : (a : β) → Measure Ω)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
c : Ω
this : Eq (α := α → Ω) (fun (x : α) ↦ c) ((fun (x : β) ↦ c) ∘ X)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib ((fun (x : β) ↦ c) ∘ X) X μ) : (a : β) → Measure Ω)
    (⇑(Kernel.deterministic (fun (x : β) ↦ c) ⋯) : (a : β) → Measure Ω)
have h : ∀ (b : β)
  (hb :
    Eq.{u_3 + 1} (α := Measure Ω) ((condDistrib ((fun (x : β) ↦ c) ∘ X) X μ : (a : β) → Measure Ω) b : Measure Ω)
      ((Kernel.deterministic (fun (x : β) ↦ c) sorry : (a : β) → Measure Ω) b : Measure Ω)),
  Eq.{u_3 + 1} (α := Measure Ω) ((condDistrib ((fun (x : β) ↦ c) ∘ X) X μ : (a : β) → Measure Ω) b : Measure Ω)
    ((Kernel.deterministic (fun (x : β) ↦ c) sorry : (a : β) → Measure Ω) b : Measure Ω)
Tactic: filter_upwards [condDistrib_comp_self X (measurable_const (a := c))] with b hb
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
c : Ω
this : Eq (α := α → Ω) (fun (x : α) ↦ c) ((fun (x : β) ↦ c) ∘ X)
b : β
hb :
  Eq.{u_3 + 1} (α := Measure Ω) ((condDistrib ((fun (x : β) ↦ c) ∘ X) X μ : (a : β) → Measure Ω) b : Measure Ω)
    ((Kernel.deterministic (fun (x : β) ↦ c) ⋯ : (a : β) → Measure Ω) b : Measure Ω)
⊢ Eq.{u_3 + 1} (α := Measure Ω) ((condDistrib ((fun (x : β) ↦ c) ∘ X) X μ : (a : β) → Measure Ω) b : Measure Ω)
    ((Kernel.deterministic (fun (x : β) ↦ c) ⋯ : (a : β) → Measure Ω) b : Measure Ω)
have h : Eq.{u_3 + 1} (α := Measure Ω) ((Kernel.deterministic (fun (x : β) ↦ c) sorry : (a : β) → Measure Ω) b : Measure Ω)
  ((Kernel.deterministic (fun (x : β) ↦ c) sorry : (a : β) → Measure Ω) b : Measure Ω)
Tactic: rw [hb]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
ν : Measure γ
inst_3 : IsFiniteMeasure ν
f : γ → α
hX : AEMeasurable (_m := mα) X (Measure.map f ν)
hY : AEMeasurable (_m := mα) Y (Measure.map f ν)
hf : AEMeasurable f ν
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (X ∘ f) ν))
    (⇑(@condDistrib _ _ _ _ _ _ mα _ Y X (Measure.map f ν) _) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ f) (X ∘ f) ν) : (a : β) → Measure Ω)
have rw : EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X (Measure.map f ν)))
  (⇑(@condDistrib _ _ _ _ _ _ mα _ Y X (Measure.map f ν) _) : (a : β) → Measure Ω)
  (⇑(condDistrib (Y ∘ f) (X ∘ f) ν) : (a : β) → Measure Ω)
Tactic: rw [← AEMeasurable.map_map_of_aemeasurable hX hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
ν : Measure γ
inst_3 : IsFiniteMeasure ν
f : γ → α
hX : AEMeasurable (_m := mα) X (Measure.map f ν)
hY : AEMeasurable (_m := mα) Y (Measure.map f ν)
hf : AEMeasurable f ν
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X (Measure.map f ν)))
    (⇑(@condDistrib _ _ _ _ _ _ mα _ Y X (Measure.map f ν) _) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ f) (X ∘ f) ν) : (a : β) → Measure Ω)
have refine : Eq (α := Measure (β × Ω)) (Measure.map (fun (x : α) ↦ (X x, Y x)) (Measure.map f ν))
  (Measure.map X (Measure.map f ν) ⊗ₘ condDistrib (Y ∘ f) (X ∘ f) ν)
Tactic: refine condDistrib_ae_eq_of_measure_eq_compProd (μ := ν.map f) X hY ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
ν : Measure γ
inst_3 : IsFiniteMeasure ν
f : γ → α
hX : AEMeasurable (_m := mα) X (Measure.map f ν)
hY : AEMeasurable (_m := mα) Y (Measure.map f ν)
hf : AEMeasurable f ν
⊢ AEMeasurable (Y ∘ f) ν
have funProp : mα ≤ mα
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
ν : Measure γ
inst_3 : IsFiniteMeasure ν
f : γ → α
hX : AEMeasurable (_m := mα) X (Measure.map f ν)
hY : AEMeasurable (_m := mα) Y (Measure.map f ν)
hf : AEMeasurable f ν
funProp : mα ≤ mα
⊢ AEMeasurable (Y ∘ f) ν
have funProp₁ : MeasurableEmbedding.{u_1, u_3} (β := Ω) fun (a0 : α) ↦ Y a0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
ν : Measure γ
inst_3 : IsFiniteMeasure ν
f : γ → α
hX : AEMeasurable (_m := mα) X (Measure.map f ν)
hY : AEMeasurable (_m := mα) Y (Measure.map f ν)
hf : AEMeasurable f ν
⊢ Eq (α := Measure (β × Ω)) (Measure.map (fun (x : α) ↦ (X x, Y x)) (Measure.map f ν))
    (Measure.map X (Measure.map f ν) ⊗ₘ condDistrib (Y ∘ f) (X ∘ f) ν)
have rw : Eq (α := Measure (β × Ω)) (Measure.map ((fun (x : α) ↦ (X x, Y x)) ∘ f) ν)
  (Measure.map (fun (a : γ) ↦ ((X ∘ f) a, (Y ∘ f) a)) ν)
Tactic: rw [AEMeasurable.map_map_of_aemeasurable hX hf, compProd_map_condDistrib (by fun_prop),
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) hf]