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 β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst_4 : IsProbabilityMeasure ν
⊢ 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 Ω)
have 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 Ω)
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 γ
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 Ω)
⊢ 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 Ω)
have 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 Ω)
Tactic: by_cases hX : AEMeasurable X μ
-- 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 μ
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 Ω)
have 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 Ω)
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)
-- 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 μ
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 μ))
    (⇑(condDistrib (fun (ω : α × γ) ↦ Y ω.1) (fun (ω : α × γ) ↦ X ω.1) (μ.prod ν)) : (a : β) → Measure Ω)
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω)
have 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 Ω)
Tactic: rw [← AEMeasurable.map_map_of_aemeasurable (by simpa) (by fun_prop)] at h_map
Cleared hypotheses: h_map
-- 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 μ
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 (fun (ω : α × γ) ↦ Y ω.1) (fun (ω : α × γ) ↦ X ω.1) (μ.prod ν)) : (a : β) → Measure Ω)
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω)
have 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 Ω)
Tactic: simp only [Measure.map_fst_prod, measure_univ, one_smul] at h_map
Cleared hypotheses: h_map
-- 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 γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst_4 : IsProbabilityMeasure ν
⊢ 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 Ω)
have 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 Ω)
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 γ
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 Ω)
⊢ 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 Ω)
have 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 Ω)
Tactic: by_cases hX : AEMeasurable X μ
-- 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 μ
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 Ω)
have 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 Ω)
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)
-- 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 μ
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 μ))
    (⇑(condDistrib (fun (ω : γ × α) ↦ Y ω.2) (fun (ω : γ × α) ↦ X ω.2) (ν.prod μ)) : (a : β) → Measure Ω)
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω)
have 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 Ω)
Tactic: rw [← AEMeasurable.map_map_of_aemeasurable (by simpa) (by fun_prop)] at h_map
Cleared hypotheses: h_map
-- 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 μ
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 (fun (ω : γ × α) ↦ Y ω.2) (fun (ω : γ × α) ↦ X ω.2) (ν.prod μ)) : (a : β) → Measure Ω)
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω)
have 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 Ω)
Tactic: simp only [Measure.map_snd_prod, measure_univ, one_smul] at h_map
Cleared hypotheses: h_map
-- 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 μ
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) μ
have refine_1 : AEMeasurable (β := ℝ≥0∞)
  (fun (a : α) ↦ ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s)
  μ
Tactic: refine integrable_toReal_of_lintegral_ne_top ?_ ?_
-- 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 μ
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)
    μ
⊢ Integrable (ε := ℝ)
    (fun (a : α) ↦ Measure.real (m := inst) (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) s) μ
have refine_2 : ∫⁻ (x : α), ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ ≠ ∞
Tactic: refine integrable_toReal_of_lintegral_ne_top ?_ ?_
-- 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 μ
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 ∂μ ≠
    ∞
have refine_2 : ∫⁻ (x : α), ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ < ∞
Tactic: refine ne_of_lt ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
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 : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
⊢ ∀ᵐ (b : β) ∂Measure.map X μ,
    @Integrable.{u_4, u_3} F _ _ _ inst (fun (ω : Ω) ↦ f (b, ω))
      (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) b)
have rw : ∀ᵐ (b : β) ∂Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ),
  @Integrable.{u_4, u_3} F _ _ _ inst (fun (ω : Ω) ↦ f (b, ω))
    ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) b)
Tactic: rw [condDistrib, ← Measure.fst_map_prodMk₀ (X := X) hY]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
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 : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
⊢ @Integrable ℝ _ _ _ mβ
    (fun (x : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) x) fun (y : Ω) ↦ ‖f (x, y)‖)
    (Measure.map X μ)
have rw : @Integrable ℝ _ _ _ mβ
  (fun (x : β) ↦
    @integral _ _ _ _ inst ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) x)
      fun (y : Ω) ↦ ‖f (x, y)‖)
  (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ))
Tactic: rw [condDistrib, ← Measure.fst_map_prodMk₀ (X := X) hY]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
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 : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst_5 : NormedSpace ℝ F
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
⊢ @Integrable ℝ _ _ _ mβ
    (fun (x : β) ↦
      norm.{u_4} (E := F)
        (@integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) x) fun (y : Ω) ↦ f (x, y)))
    (Measure.map X μ)
have rw : @Integrable ℝ _ _ _ mβ
  (fun (x : β) ↦
    norm.{u_4} (E := F)
      (@integral _ _ _ _ inst ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) x)
        fun (y : Ω) ↦ f (x, y)))
  (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ))
Tactic: rw [condDistrib, ← Measure.fst_map_prodMk₀ (X := 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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (a : α) in X ⁻¹' t,
      ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ =
    (μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s)
have rw : ∫⁻ (a : β),
    ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
      s ∂Measure.map X (μ.restrict (X ⁻¹' t)) =
  (μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s)
Tactic: rw [← lintegral_map (Kernel.measurable_coe _ hs) hX, condDistrib, ← Measure.restrict_map hX ht,
    ← Measure.fst_map_prodMk₀ hY, Measure.setLIntegral_condKernel_eq_measure_prod ht hs,
    Measure.map_apply_of_aemeasurable (hX.aemeasurable.prodMk hY) (ht.prod hs), mk_preimage_prod]
-- 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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
ht : MeasurableSet t
rw :
  ∫⁻ (a : β),
      ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        s ∂Measure.map X (μ.restrict (X ⁻¹' t)) =
    (μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s)
⊢ ∫⁻ (a : α) in X ⁻¹' t,
      ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ =
    (μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s)
have rw₁ : ∫⁻ (a : β),
    (((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) a : Measure Ω) :
        (a : Set Ω) → ℝ≥0∞)
      s ∂Measure.map X (μ.restrict (X ⁻¹' t)) =
  (μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s)
Tactic: rw [← lintegral_map (Kernel.measurable_coe _ hs) hX, condDistrib, ← Measure.restrict_map hX ht,
    ← Measure.fst_map_prodMk₀ hY, Measure.setLIntegral_condKernel_eq_measure_prod ht hs,
    Measure.map_apply_of_aemeasurable (hX.aemeasurable.prodMk hY) (ht.prod hs), mk_preimage_prod]
-- 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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
ht : MeasurableSet t
rw :
  ∫⁻ (a : β),
      ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        s ∂Measure.map X (μ.restrict (X ⁻¹' t)) =
    (μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s)
rw₁ :
  ∫⁻ (a : β),
      (((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) a : Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s ∂Measure.map X (μ.restrict (X ⁻¹' t)) =
    (μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s)
⊢ ∫⁻ (a : α) in X ⁻¹' t,
      ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ =
    (μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s)
have rw₂ : ∫⁻ (a : β) in t,
    (((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) a : Measure Ω) :
        (a : Set Ω) → ℝ≥0∞)
      s ∂Measure.map X μ =
  (μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s)
Tactic: rw [← lintegral_map (Kernel.measurable_coe _ hs) hX, condDistrib, ← Measure.restrict_map hX ht,
    ← Measure.fst_map_prodMk₀ hY, Measure.setLIntegral_condKernel_eq_measure_prod ht hs,
    Measure.map_apply_of_aemeasurable (hX.aemeasurable.prodMk hY) (ht.prod hs), mk_preimage_prod]
-- 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 μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
t : Set β
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
ht : MeasurableSet t
rw :
  ∫⁻ (a : β),
      ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        s ∂Measure.map X (μ.restrict (X ⁻¹' t)) =
    (μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s)
rw₁ :
  ∫⁻ (a : β),
      (((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) a : Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s ∂Measure.map X (μ.restrict (X ⁻¹' t)) =
    (μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s)
rw₂ :
  ∫⁻ (a : β) in t,
      (((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) a : Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s ∂Measure.map X μ =
    (μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s)
⊢ ∫⁻ (a : α) in X ⁻¹' t,
      ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ =
    (μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s)
have rw₃ : ∫⁻ (a : β) in t,
    (((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) a : Measure Ω) :
        (a : Set Ω) → ℝ≥0∞)
      s ∂Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) =
  (μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s)
Tactic: rw [← lintegral_map (Kernel.measurable_coe _ hs) hX, condDistrib, ← Measure.restrict_map hX ht,
    ← Measure.fst_map_prodMk₀ hY, Measure.setLIntegral_condKernel_eq_measure_prod ht hs,
    Measure.map_apply_of_aemeasurable (hX.aemeasurable.prodMk hY) (ht.prod hs), mk_preimage_prod]