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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := β × Ω) fun (x : α) ↦ (X x, Y x)

Tactic:
Measurable.prod hX hY

Premises used: Measurable.prod
-- 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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (α := β × Ω) (Prod.fst ⁻¹' s)

Tactic:
measurable_fst hs

Premises used: measurable_fst
-- 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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β × Ω) (fun (x : α) ↦ (X x, Y x)) (Prod.fst ⁻¹' s)) : ℝ≥0∞)

Tactic:
exacts [rfl, Measurable.prod hX hY, measurable_fst hs]

Premises used: Measurable.prod, measurable_fst, 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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
⊢ Eq (α := Measure β) (Measure.map X μ) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))

Tactic:
have heq : μ.map X = (μ.map (fun x ↦ (X x, Y x))).fst := by
    ext s hs
    rw [Measure.map_apply hX hs, Measure.fst_apply hs, Measure.map_apply]
    exacts [rfl, Measurable.prod hX hY, measurable_fst hs]
-- 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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Eq (α := Measure β) (Measure.map X μ) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
rw :
  EventuallyEq.{u_2, u_3} (β := Measure Ω)
    (ae (F := Measure β) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ)))
    (⇑(Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)

Tactic:
rw [heq, condDistrib]

Premises used: ProbabilityTheory.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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Eq (α := Measure β) (Measure.map X μ) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
symm :
  EventuallyEq.{u_2, u_3} (β := Measure Ω)
    (ae (F := Measure β) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ)))
    (⇑κ : (a : β) → Measure Ω) (⇑(Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) : (a : β) → Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω)
    (ae (F := Measure β) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ)))
    (⇑(Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)

Tactic:
symm
-- 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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Eq (α := Measure β) (Measure.map X μ) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω)
    (ae (F := Measure β) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ)))
    (⇑κ : (a : β) → Measure Ω) (⇑(Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) : (a : β) → Measure Ω)

Tactic:
eq_condKernel_of_measure_eq_compProd _ ?_

Premises used: Filter.EventuallyEq, ProbabilityTheory.eq_condKernel_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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Eq (α := Measure β) (Measure.map X μ) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
refine :
  Measure.map (fun (a : α) ↦ (X a, Y a)) μ =
    Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) ⊗ₘ κ
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω)
    (ae (F := Measure β) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ)))
    (⇑κ : (a : β) → Measure Ω) (⇑(Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) : (a : β) → Measure Ω)

Tactic:
refine eq_condKernel_of_measure_eq_compProd _ ?_

Premises used: ProbabilityTheory.eq_condKernel_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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Eq (α := Measure β) (Measure.map X μ) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
⊢ Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ

Tactic:
hκ
-- 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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Eq (α := Measure β) (Measure.map X μ) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
h : Eq (α := Measure β) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) (Measure.map X μ)
⊢ Measure.map (fun (a : α) ↦ (X a, Y a)) μ =
    Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) ⊗ₘ κ

Tactic:
convert! hκ
-- 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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Eq (α := Measure β) (Measure.map X μ) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
⊢ Eq (α := Measure β) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) (Measure.map X μ)

Tactic:
heq.symm

Premises used: Eq.symm
-- 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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Eq (α := Measure β) (Measure.map X μ) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
⊢ Eq (α := Measure β) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) (Measure.map X μ)

Tactic:
exact heq.symm

Premises used: Eq.symm
-- 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 β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
pos :
  ∀ (hX : AEMeasurable X μ),
    EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
      (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
neg :
  ∀ (hX : ¬AEMeasurable X μ),
    EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
      (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (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 μ
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 μ
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (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 β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
this :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (AEMeasurable.mk X hX) μ))
    (⇑(condDistrib (AEMeasurable.mk Y hY) (AEMeasurable.mk X hX) μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
rwa :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (AEMeasurable.mk X hX) μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
rwa₁ rwa₂ rwa₃ rwa₄ :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (AEMeasurable.mk X hX) μ))
    (⇑(condDistrib (AEMeasurable.mk Y hY) (AEMeasurable.mk X hX) μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)

Tactic:
rwa [Measure.map_congr hX.ae_eq_mk, condDistrib_congr hY.ae_eq_mk hX.ae_eq_mk]

Premises used: MeasureTheory.Measure.map_congr, ProbabilityTheory.condDistrib_congr, AEMeasurable.ae_eq_mk
-- 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 β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
pos :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (AEMeasurable.mk X hX) μ))
    (⇑(condDistrib (AEMeasurable.mk Y hY) (AEMeasurable.mk X hX) μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)

Tactic:
suffices condDistrib (hY.mk Y) (hX.mk X) μ =ᵐ[μ.map (hX.mk X)] κ by
    rwa [Measure.map_congr hX.ae_eq_mk, condDistrib_congr hY.ae_eq_mk hX.ae_eq_mk]
-- 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 β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (AEMeasurable.mk X hX) μ))
    (⇑(condDistrib (AEMeasurable.mk Y hY) (AEMeasurable.mk X hX) μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)

Tactic:
condDistrib_ae_eq_of_measure_eq_compProd_of_measurable (μ := μ)
    hX.measurable_mk hY.measurable_mk ((Eq.trans ?_ hκ).trans ?_)

Premises used: ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd_of_measurable, Eq.trans, AEMeasurable.measurable_mk
-- 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 β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
pos :
  Eq (α := Measure (β × Ω)) (Measure.map (fun (x : α) ↦ (AEMeasurable.mk X hX x, AEMeasurable.mk Y hY x)) μ)
    (Measure.map (fun (x : α) ↦ (X x, Y x)) μ)
pos₁ : Measure.map X μ ⊗ₘ κ = Measure.map (AEMeasurable.mk X hX) μ ⊗ₘ κ
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (AEMeasurable.mk X hX) μ))
    (⇑(condDistrib (AEMeasurable.mk Y hY) (AEMeasurable.mk X hX) μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)

Tactic:
refine condDistrib_ae_eq_of_measure_eq_compProd_of_measurable (μ := μ)
    hX.measurable_mk hY.measurable_mk ((Eq.trans ?_ hκ).trans ?_)

Premises used: ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd_of_measurable, Eq.trans, AEMeasurable.measurable_mk
-- 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 β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
⊢ Eq (α := Measure (β × Ω)) (Measure.map (fun (x : α) ↦ (AEMeasurable.mk X hX x, AEMeasurable.mk Y hY x)) μ)
    (Measure.map (fun (x : α) ↦ (X x, Y x)) μ)

Tactic:
Measure.map_congr ?_

Premises used: MeasureTheory.Measure.map_congr
-- 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 β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
pos :
  (ae μ).EventuallyEq (β := β × Ω) (fun (x : α) ↦ (AEMeasurable.mk X hX x, AEMeasurable.mk Y hY x)) fun (x : α) ↦
    (X x, Y x)
⊢ Eq (α := Measure (β × Ω)) (Measure.map (fun (x : α) ↦ (AEMeasurable.mk X hX x, AEMeasurable.mk Y hY x)) μ)
    (Measure.map (fun (x : α) ↦ (X x, Y x)) μ)

Tactic:
refine Measure.map_congr ?_

Premises used: MeasureTheory.Measure.map_congr
-- 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 β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
a : α
haX : X a = AEMeasurable.mk X hX a
haY : Y a = AEMeasurable.mk Y hY a
rw : (AEMeasurable.mk X hX a, AEMeasurable.mk Y hY a) = (AEMeasurable.mk X hX a, Y a)
rw₁ rw₂ : (AEMeasurable.mk X hX a, AEMeasurable.mk Y hY a) = (AEMeasurable.mk X hX a, AEMeasurable.mk Y hY a)
⊢ (AEMeasurable.mk X hX a, AEMeasurable.mk Y hY a) = (X a, Y a)

Tactic:
rw [haX, haY]
-- 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 β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ X x = AEMeasurable.mk X hX x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Y x = AEMeasurable.mk Y hY x) x} x →
                Membership.mem (γ := Set α)
                  {x : α |
                    (fun (x : α) ↦
                        Eq (α := β × Ω) ((fun (x : α) ↦ (AEMeasurable.mk X hX x, AEMeasurable.mk Y hY x)) x)
                          ((fun (x : α) ↦ (X x, Y x)) x))
                      x}
                  x}
            x}
      a
h₁ h₂ :
  ∀ (a : α) (haX : X a = AEMeasurable.mk X hX a) (haY : Y a = AEMeasurable.mk Y hY a),
    (AEMeasurable.mk X hX a, AEMeasurable.mk Y hY a) = (X a, Y a)
⊢ (ae μ).EventuallyEq (β := β × Ω) (fun (x : α) ↦ (AEMeasurable.mk X hX x, AEMeasurable.mk Y hY x)) fun (x : α) ↦
    (X x, Y x)

Tactic:
filter_upwards [hX.ae_eq_mk, hY.ae_eq_mk] with a haX haY using by rw [haX, haY]

Premises used: AEMeasurable.ae_eq_mk
-- 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 β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
pos pos₁ : Measure.map (AEMeasurable.mk X hX) μ ⊗ₘ κ = Measure.map (AEMeasurable.mk X hX) μ ⊗ₘ κ
⊢ Measure.map X μ ⊗ₘ κ = Measure.map (AEMeasurable.mk X hX) μ ⊗ₘ κ

Tactic:
rw [Measure.map_congr hX.ae_eq_mk]

Premises used: MeasureTheory.Measure.map_congr, AEMeasurable.ae_eq_mk
-- 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 β
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 μ ⊗ₘ κ

Tactic:
⟨fun h ↦ ?_, condDistrib_ae_eq_of_measure_eq_compProd X hY⟩

Premises used: ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd, Iff.intro
-- 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 β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
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 μ ⊗ₘ κ
⊢ 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⟩
-- 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 β
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 μ)
rw₁ rw₂ :
  Eq (α := Measure (β × Ω)) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
⊢ Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ

Tactic:
rw [Measure.compProd_congr h.symm, compProd_map_condDistrib hY]

Premises used: ProbabilityTheory.compProd_map_condDistrib, MeasureTheory.Measure.compProd_congr, Filter.EventuallyEq.symm
-- 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
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 Ω')
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 Ω')
⊢ 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 μ

Premises used: AEMeasurable