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 γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst_4 : IsProbabilityMeasure ν
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 Ω)

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 γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst_4 : IsProbabilityMeasure ν
hX : AEMeasurable X μ
⊢ AEMeasurable (_m := inferInstance) X (Measure.map Prod.fst (μ.prod ν))

Tactic:
simpa
-- 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 ν
hX : AEMeasurable X μ
⊢ AEMeasurable (_m := inferInstance) Y (Measure.map Prod.fst (μ.prod ν))

Tactic:
simpa
-- 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 ν
hX : AEMeasurable X μ
⊢ AEMeasurable Prod.fst (μ.prod ν)

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 γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst_4 : IsProbabilityMeasure ν
hX : AEMeasurable X μ
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (X ∘ Prod.fst) (μ.prod ν)))
    (⇑(@condDistrib _ _ _ _ _ _ inferInstance _ Y X (Measure.map Prod.fst (μ.prod ν)) _) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ Prod.fst) (X ∘ Prod.fst) (μ.prod ν)) : (a : β) → Measure Ω)

Tactic:
have h_map := condDistrib_map (X := X) (Y := Y) (f := Prod.fst (α := α) (β := γ))
      (ν := μ.prod ν) (mα := inferInstance) (mβ := inferInstance)
      (by simpa) (by simpa) (by 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 γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst_4 : IsProbabilityMeasure ν
hX : AEMeasurable X μ
h_map :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (X ∘ Prod.fst) (μ.prod ν)))
    (⇑(@condDistrib _ _ _ _ _ _ inferInstance _ Y X (Measure.map Prod.fst (μ.prod ν)) _) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ Prod.fst) (X ∘ Prod.fst) (μ.prod ν)) : (a : β) → Measure Ω)
⊢ AEMeasurable (_m := mα) X (Measure.map Prod.fst (μ.prod ν))

Tactic:
simpa
-- 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 ν
hX : AEMeasurable X μ
h_map :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (X ∘ Prod.fst) (μ.prod ν)))
    (⇑(@condDistrib _ _ _ _ _ _ inferInstance _ Y X (Measure.map Prod.fst (μ.prod ν)) _) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ Prod.fst) (X ∘ Prod.fst) (μ.prod ν)) : (a : β) → Measure Ω)
⊢ AEMeasurable Prod.fst (μ.prod ν)

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 γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst_4 : IsProbabilityMeasure ν
hX : AEMeasurable X μ
h_map :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (X ∘ Prod.fst) (μ.prod ν)))
    (⇑(@condDistrib _ _ _ _ _ _ inferInstance _ Y X (Measure.map Prod.fst (μ.prod ν)) _) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ Prod.fst) (X ∘ Prod.fst) (μ.prod ν)) : (a : β) → Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X (Measure.map Prod.fst (μ.prod ν))))
    (⇑(@condDistrib _ _ _ _ _ _ inferInstance _ Y X (Measure.map Prod.fst (μ.prod ν)) _) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ Prod.fst) (X ∘ Prod.fst) (μ.prod ν)) : (a : β) → Measure Ω)

Tactic:
rw [← AEMeasurable.map_map_of_aemeasurable (by simpa) (by fun_prop)] at h_map

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 γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst_4 : IsProbabilityMeasure ν
hX : AEMeasurable X μ
h_map :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X (Measure.map Prod.fst (μ.prod ν))))
    (⇑(@condDistrib _ _ _ _ _ _ inferInstance _ Y X (Measure.map Prod.fst (μ.prod ν)) _) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ Prod.fst) (X ∘ Prod.fst) (μ.prod ν)) : (a : β) → Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ Prod.fst) (X ∘ Prod.fst) (μ.prod ν)) : (a : β) → Measure Ω)

Tactic:
simp only [Measure.map_fst_prod, measure_univ, one_smul] at h_map

Premises used: MeasureTheory.Measure.map_fst_prod, MeasureTheory.IsProbabilityMeasure.measure_univ, one_smul
-- 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 ν
hX : AEMeasurable X μ
h_map :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ Prod.fst) (X ∘ Prod.fst) (μ.prod ν)) : (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:
h_map.symm

Premises used: 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 γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst_4 : IsProbabilityMeasure ν
hX : AEMeasurable X μ
h_map :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ Prod.fst) (X ∘ Prod.fst) (μ.prod ν)) : (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:
exact h_map.symm

Premises used: 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 γ
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 ω.2) (fun (ω : γ × α) ↦ X ω.2) (ν.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 ω.2) (fun (ω : γ × α) ↦ X ω.2) (ν.prod μ)) : (a : β) → Measure Ω)
      (⇑(condDistrib Y X μ) : (a : β) → Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib (fun (ω : γ × α) ↦ Y ω.2) (fun (ω : γ × α) ↦ X ω.2) (ν.prod μ)) : (a : β) → Measure Ω)
    (⇑(condDistrib Y X μ) : (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 β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst_4 : IsProbabilityMeasure ν
hX : ¬AEMeasurable X μ
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib (fun (ω : γ × α) ↦ Y ω.2) (fun (ω : γ × α) ↦ X ω.2) (ν.prod μ)) : (a : β) → Measure Ω)
    (⇑(condDistrib Y X μ) : (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 γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst_4 : IsProbabilityMeasure ν
hX : AEMeasurable X μ
⊢ AEMeasurable (_m := inferInstance) X (Measure.map Prod.snd (ν.prod μ))

Tactic:
simpa
-- 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 ν
hX : AEMeasurable X μ
⊢ AEMeasurable (_m := inferInstance) Y (Measure.map Prod.snd (ν.prod μ))

Tactic:
simpa
-- 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 ν
hX : AEMeasurable X μ
⊢ AEMeasurable Prod.snd (ν.prod μ)

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 γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst_4 : IsProbabilityMeasure ν
hX : AEMeasurable X μ
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (X ∘ Prod.snd) (ν.prod μ)))
    (⇑(@condDistrib _ _ _ _ _ _ inferInstance _ Y X (Measure.map Prod.snd (ν.prod μ)) _) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ Prod.snd) (X ∘ Prod.snd) (ν.prod μ)) : (a : β) → Measure Ω)

Tactic:
have h_map := condDistrib_map (X := X) (Y := Y) (f := Prod.snd (β := α) (α := γ))
      (ν := ν.prod μ) (mα := inferInstance) (mβ := inferInstance)
      (by simpa) (by simpa) (by 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 γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst_4 : IsProbabilityMeasure ν
hX : AEMeasurable X μ
h_map :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (X ∘ Prod.snd) (ν.prod μ)))
    (⇑(@condDistrib _ _ _ _ _ _ inferInstance _ Y X (Measure.map Prod.snd (ν.prod μ)) _) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ Prod.snd) (X ∘ Prod.snd) (ν.prod μ)) : (a : β) → Measure Ω)
⊢ AEMeasurable (_m := mα) X (Measure.map Prod.snd (ν.prod μ))

Tactic:
simpa
-- 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 ν
hX : AEMeasurable X μ
h_map :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (X ∘ Prod.snd) (ν.prod μ)))
    (⇑(@condDistrib _ _ _ _ _ _ inferInstance _ Y X (Measure.map Prod.snd (ν.prod μ)) _) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ Prod.snd) (X ∘ Prod.snd) (ν.prod μ)) : (a : β) → Measure Ω)
⊢ AEMeasurable Prod.snd (ν.prod μ)

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 γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst_4 : IsProbabilityMeasure ν
hX : AEMeasurable X μ
h_map :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (X ∘ Prod.snd) (ν.prod μ)))
    (⇑(@condDistrib _ _ _ _ _ _ inferInstance _ Y X (Measure.map Prod.snd (ν.prod μ)) _) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ Prod.snd) (X ∘ Prod.snd) (ν.prod μ)) : (a : β) → Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X (Measure.map Prod.snd (ν.prod μ))))
    (⇑(@condDistrib _ _ _ _ _ _ inferInstance _ Y X (Measure.map Prod.snd (ν.prod μ)) _) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ Prod.snd) (X ∘ Prod.snd) (ν.prod μ)) : (a : β) → Measure Ω)

Tactic:
rw [← AEMeasurable.map_map_of_aemeasurable (by simpa) (by fun_prop)] at h_map

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 γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst_4 : IsProbabilityMeasure ν
hX : AEMeasurable X μ
h_map :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X (Measure.map Prod.snd (ν.prod μ))))
    (⇑(@condDistrib _ _ _ _ _ _ inferInstance _ Y X (Measure.map Prod.snd (ν.prod μ)) _) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ Prod.snd) (X ∘ Prod.snd) (ν.prod μ)) : (a : β) → Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ Prod.snd) (X ∘ Prod.snd) (ν.prod μ)) : (a : β) → Measure Ω)

Tactic:
simp only [Measure.map_snd_prod, measure_univ, one_smul] at h_map

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, one_smul, MeasureTheory.Measure.map_snd_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 μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst_4 : IsProbabilityMeasure ν
hX : AEMeasurable X μ
h_map :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ Prod.snd) (X ∘ Prod.snd) (ν.prod μ)) : (a : β) → Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib (fun (ω : γ × α) ↦ Y ω.2) (fun (ω : γ × α) ↦ X ω.2) (ν.prod μ)) : (a : β) → Measure Ω)
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω)

Tactic:
h_map.symm

Premises used: 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 γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst_4 : IsProbabilityMeasure ν
hX : AEMeasurable X μ
h_map :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω)
    (⇑(condDistrib (Y ∘ Prod.snd) (X ∘ Prod.snd) (ν.prod μ)) : (a : β) → Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib (fun (ω : γ × α) ↦ Y ω.2) (fun (ω : γ × α) ↦ X ω.2) (ν.prod μ)) : (a : β) → Measure Ω)
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω)

Tactic:
exact h_map.symm

Premises used: 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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ Integrable (ε := ℝ)
    (fun (a : α) ↦ Measure.real (m := inst) (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) s) μ

Tactic:
integrable_toReal_of_lintegral_ne_top ?_ ?_

Premises used: MeasureTheory.Measure.real, MeasureTheory.integrable_toReal_of_lintegral_ne_top
-- 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 β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
refine_1 :
  AEMeasurable (β := ℝ≥0∞)
    (fun (a : α) ↦
      ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s)
    μ
refine_2 :
  ∫⁻ (x : α), ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ ≠
    ∞
⊢ Integrable (ε := ℝ)
    (fun (a : α) ↦ Measure.real (m := inst) (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) s) μ

Tactic:
refine integrable_toReal_of_lintegral_ne_top ?_ ?_

Premises used: MeasureTheory.integrable_toReal_of_lintegral_ne_top
-- 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 β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ AEMeasurable (β := ℝ≥0∞)
    (fun (a : α) ↦
      ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s)
    μ

Tactic:
Measurable.comp_aemeasurable (Kernel.measurable_coe _ hs) hX

Premises used: ProbabilityTheory.Kernel.measurable_coe, Measurable.comp_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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ AEMeasurable (β := ℝ≥0∞)
    (fun (a : α) ↦
      ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s)
    μ

Tactic:
exact Measurable.comp_aemeasurable (Kernel.measurable_coe _ hs) hX

Premises used: ProbabilityTheory.Kernel.measurable_coe, Measurable.comp_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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ ∫⁻ (x : α), ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ ≠
    ∞

Tactic:
ne_of_lt ?_

Premises used: ne_of_lt
-- 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 β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
refine_2 :
  ∫⁻ (x : α), ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ <
    ∞
⊢ ∫⁻ (x : α), ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ ≠
    ∞

Tactic:
refine ne_of_lt ?_

Premises used: ne_of_lt
-- 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 β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ ≤
    ∫⁻ (x : α), 1 ∂μ

Tactic:
lintegral_mono fun a => prob_le_one

Premises used: MeasureTheory.prob_le_one, MeasureTheory.lintegral_mono
-- 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 β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ ∫⁻ (x : α), 1 ∂μ = (μ : (a : Set α) → ℝ≥0∞) univ

Tactic:
lintegral_one

Premises used: MeasureTheory.lintegral_one
-- 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 β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_lt_top _ _

Premises used: MeasureTheory.measure_lt_top