awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 Ω')

Tactic:
simp [Measure.map_of_not_aemeasurable hX, Filter.EventuallyEq]

Premises used: Filter.EventuallyEq, MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 μ
⊢ AEMeasurable (f ∘ Y) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 μ
pos :
  Eq (α := Measure (β × Ω')) (Measure.map (fun (x : α) ↦ (X x, (f ∘ Y) x)) μ)
    (Measure.map X μ ⊗ₘ Kernel.map (mβ := inst) (condDistrib Y X μ) 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 Ω')

Tactic:
refine condDistrib_ae_eq_of_measure_eq_compProd X (by fun_prop) ?_

Premises used: ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 μ
⊢ AEMeasurable (α := β × Ω) (_m := Prod.instMeasurableSpace) (Prod.map id f) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 μ
⊢ AEMeasurable (β := β × Ω) (fun (x : α) ↦ (X x, Y x)) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 μ
rw :
  Eq (α := Measure (β × Ω')) (Measure.map (fun (x : α) ↦ (X x, (f ∘ Y) x)) μ)
    (Measure.map (Prod.map id f ∘ fun (x : α) ↦ (X x, Y 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)) μ))

Tactic:
rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]

Premises used: AEMeasurable.map_map_of_aemeasurable
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 ∘ fun (x : α) ↦ (X x, Y x)) μ)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 μ
rw 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)) μ))
⊢ 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:
rw [compProd_map_condDistrib hY]

Premises used: ProbabilityTheory.compProd_map_condDistrib
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 μ
rw 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 μ))
⊢ 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:
rw [Measure.compProd_map hf]

Premises used: MeasureTheory.Measure.compProd_map
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 μ))
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)
⊢ Eq (α := Measure (β × Ω')) (Measure.map (fun (x : α) ↦ (X x, (f ∘ 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]

Premises used: ProbabilityTheory.Kernel.map, Function.comp, ProbabilityTheory.condDistrib, id, Prod.mk, Prod.map, MeasureTheory.Measure.map, MeasureTheory.Measure.compProd
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 Ω)
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 Ω)
⊢ 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 μ

Premises used: AEMeasurable
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 Ω)

Tactic:
simp [Measure.map_of_not_aemeasurable hX, Filter.EventuallyEq]

Premises used: Filter.EventuallyEq, MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 μ
⊢ AEMeasurable (f ∘ X) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 μ
pos : Measure.map (fun (x : α) ↦ (X x, (f ∘ X) x)) μ = Measure.map X μ ⊗ₘ Kernel.deterministic f hf
⊢ 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:
refine condDistrib_ae_eq_of_measure_eq_compProd X (by fun_prop) ?_

Premises used: ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 μ
⊢ AEMeasurable (β := β × Ω) (_m := mβ) (fun (a : β) ↦ (a, f a)) (Measure.map X μ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 μ
pos :
  Eq (α := Measure (β × Ω)) (Measure.map (fun (x : α) ↦ (X x, (f ∘ X) x)) μ)
    (Measure.map ((fun (a : β) ↦ (a, f a)) ∘ X) μ)
⊢ Measure.map (fun (x : α) ↦ (X x, (f ∘ X) x)) μ = Measure.map X μ ⊗ₘ Kernel.deterministic f hf

Tactic:
rw [Measure.compProd_deterministic, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX]

Premises used: MeasureTheory.Measure.compProd_deterministic, AEMeasurable.map_map_of_aemeasurable
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 μ
⊢ Eq (α := Measure (β × Ω)) (Measure.map (fun (x : α) ↦ (X x, (f ∘ X) x)) μ)
    (Measure.map ((fun (a : β) ↦ (a, f a)) ∘ X) μ)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
α : Type u_1
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
Y : α → Ω
⊢ (ae (F := Measure Ω) (Measure.map Y μ)).EventuallyEq (β := Measure Ω) (⇑(condDistrib Y Y μ) : (a : Ω) → Measure Ω)
    (⇑Kernel.id : (a : Ω) → Measure Ω)

Tactic:
simpa using condDistrib_comp_self Y measurable_id

Premises used: measurable_id, ProbabilityTheory.condDistrib_comp_self
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst_4 : IsFiniteMeasure μ
X_1 : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
f : β × Ω → F
X : α → β
c : Ω
⊢ Measurable.{u_2, u_3} (β := Ω) fun (x : β) ↦ c

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 : Ω
⊢ Eq (α := α → Ω) (fun (x : α) ↦ c) ((fun (x : β) ↦ c) ∘ X)

Tactic:
have : (fun _ : α ↦ c) = (fun _ : β ↦ c) ∘ X := rfl
-- Module: Mathlib.Probability.Kernel.CondDistrib
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)
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) ⋯) : (a : β) → Measure Ω)
⊢ 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 Ω)

Tactic:
rw [this]
-- Module: Mathlib.Probability.Kernel.CondDistrib
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)
h :
  ∀ (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 Ω)
⊢ 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 Ω)

Tactic:
filter_upwards [condDistrib_comp_self X (measurable_const (a := c))] with b hb

Premises used: ProbabilityTheory.condDistrib_comp_self, measurable_const
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 Ω)
h h₁ :
  Eq.{u_3 + 1} (α := Measure Ω) ((Kernel.deterministic (fun (x : β) ↦ c) ⋯ : (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 Ω)

Tactic:
rw [hb]
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 ν
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 Ω)
⊢ 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 Ω)

Tactic:
rw [← AEMeasurable.map_map_of_aemeasurable hX hf]

Premises used: AEMeasurable.map_map_of_aemeasurable
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 Ω)

Tactic:
condDistrib_ae_eq_of_measure_eq_compProd (μ := ν.map f) X hY ?_

Premises used: ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 ν
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) ν)
⊢ 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:
refine condDistrib_ae_eq_of_measure_eq_compProd (μ := ν.map f) X hY ?_

Premises used: ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd
-- Module: Mathlib.Probability.Kernel.CondDistrib
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α
funProp₁ : MeasurableEmbedding.{u_1, u_3} (β := Ω) fun (a0 : α) ↦ Y a0
⊢ AEMeasurable (Y ∘ f) ν

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 (β := β × Ω) (_m := mα) (fun (x : α) ↦ (X x, Y x)) (Measure.map f ν)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 ν
rw :
  Eq (α := Measure (β × Ω)) (Measure.map ((fun (x : α) ↦ (X x, Y x)) ∘ f) ν)
    (Measure.map (fun (a : γ) ↦ ((X ∘ f) a, (Y ∘ f) a)) ν)
⊢ 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:
rw [AEMeasurable.map_map_of_aemeasurable hX hf, compProd_map_condDistrib (by fun_prop),
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) hf]

Premises used: ProbabilityTheory.compProd_map_condDistrib, AEMeasurable.map_map_of_aemeasurable
-- Module: Mathlib.Probability.Kernel.CondDistrib
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)) ∘ f) ν)
    (Measure.map (fun (a : γ) ↦ ((X ∘ f) a, (Y ∘ f) a)) ν)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst_4 : IsProbabilityMeasure ν
pos :
  ∀ (hX : AEMeasurable X μ),
    EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
      (⇑(condDistrib (fun (ω : α × γ) ↦ Y ω.1) (fun (ω : α × γ) ↦ X ω.1) (μ.prod ν)) : (a : β) → Measure Ω)
      (⇑(condDistrib Y X μ) : (a : β) → Measure Ω)
neg :
  ∀ (hX : ¬AEMeasurable X μ),
    EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
      (⇑(condDistrib (fun (ω : α × γ) ↦ Y ω.1) (fun (ω : α × γ) ↦ X ω.1) (μ.prod ν)) : (a : β) → Measure Ω)
      (⇑(condDistrib Y X μ) : (a : β) → Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib (fun (ω : α × γ) ↦ Y ω.1) (fun (ω : α × γ) ↦ X ω.1) (μ.prod ν)) : (a : β) → Measure Ω)
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω)

Tactic:
by_cases hX : AEMeasurable X μ

Premises used: AEMeasurable