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
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
inst_6 : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
hf_int' : Integrable.{u_4, u_1} (ε := F) (fun (a : α) ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ (Measure.restrict (Measure.map X μ) t) fun (y : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) y) fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₁ :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ
      (Measure.restrict (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) t) fun (y : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) y) fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₂ :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ
      (Measure.restrict (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) t) fun (y : β) ↦
      @integral _ _ _ _ inst ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) y)
        fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₃ :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) (SProd.sprod (β := Set Ω) t univ)) fun (x : β × Ω) ↦
      f x)
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
⊢ Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ (Measure.map X (μ.restrict (X ⁻¹' t))) fun (y : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) y) fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
have refine_2₄ : Eq.{u_4 + 1} (α := F) (∫ (x : α) in (fun (a : α) ↦ (X a, Y a)) ⁻¹' SProd.sprod (β := Set Ω) t univ, f (X x, Y x) ∂μ)
  (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
Tactic: rw [← Measure.restrict_map hX ht, ← Measure.fst_map_prodMk₀ hY, condDistrib,
      Measure.setIntegral_condKernel_univ_right ht hf_int.integrableOn,
      setIntegral_map (ht.prod MeasurableSet.univ) hf_int.1 (hX.aemeasurable.prodMk hY),
      mk_preimage_prod, preimage_univ, inter_univ]
-- 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
inst_6 : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
hf_int' : Integrable.{u_4, u_1} (ε := F) (fun (a : α) ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ (Measure.restrict (Measure.map X μ) t) fun (y : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) y) fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₁ :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ
      (Measure.restrict (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) t) fun (y : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) y) fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₂ :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ
      (Measure.restrict (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) t) fun (y : β) ↦
      @integral _ _ _ _ inst ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) y)
        fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₃ :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) (SProd.sprod (β := Set Ω) t univ)) fun (x : β × Ω) ↦
      f x)
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₄ :
  Eq.{u_4 + 1} (α := F) (∫ (x : α) in (fun (a : α) ↦ (X a, Y a)) ⁻¹' SProd.sprod (β := Set Ω) t univ, f (X x, Y x) ∂μ)
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
⊢ Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ (Measure.map X (μ.restrict (X ⁻¹' t))) fun (y : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) y) fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
have refine_2₅ : Eq.{u_4 + 1} (α := F) (∫ (x : α) in X ⁻¹' t ∩ Y ⁻¹' univ, f (X x, Y x) ∂μ) (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
Tactic: rw [← Measure.restrict_map hX ht, ← Measure.fst_map_prodMk₀ hY, condDistrib,
      Measure.setIntegral_condKernel_univ_right ht hf_int.integrableOn,
      setIntegral_map (ht.prod MeasurableSet.univ) hf_int.1 (hX.aemeasurable.prodMk hY),
      mk_preimage_prod, preimage_univ, inter_univ]
-- 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
inst_6 : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
hf_int' : Integrable.{u_4, u_1} (ε := F) (fun (a : α) ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ (Measure.restrict (Measure.map X μ) t) fun (y : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) y) fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₁ :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ
      (Measure.restrict (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) t) fun (y : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) y) fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₂ :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ
      (Measure.restrict (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) t) fun (y : β) ↦
      @integral _ _ _ _ inst ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) y)
        fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₃ :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) (SProd.sprod (β := Set Ω) t univ)) fun (x : β × Ω) ↦
      f x)
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₄ :
  Eq.{u_4 + 1} (α := F) (∫ (x : α) in (fun (a : α) ↦ (X a, Y a)) ⁻¹' SProd.sprod (β := Set Ω) t univ, f (X x, Y x) ∂μ)
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₅ :
  Eq.{u_4 + 1} (α := F) (∫ (x : α) in X ⁻¹' t ∩ Y ⁻¹' univ, f (X x, Y x) ∂μ) (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
⊢ Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ (Measure.map X (μ.restrict (X ⁻¹' t))) fun (y : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) y) fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
have refine_2₆ : Eq.{u_4 + 1} (α := F) (∫ (x : α) in X ⁻¹' t ∩ univ, f (X x, Y x) ∂μ) (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
Tactic: rw [← Measure.restrict_map hX ht, ← Measure.fst_map_prodMk₀ hY, condDistrib,
      Measure.setIntegral_condKernel_univ_right ht hf_int.integrableOn,
      setIntegral_map (ht.prod MeasurableSet.univ) hf_int.1 (hX.aemeasurable.prodMk hY),
      mk_preimage_prod, preimage_univ, inter_univ]
-- 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
inst_6 : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
hf_int' : Integrable.{u_4, u_1} (ε := F) (fun (a : α) ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ (Measure.restrict (Measure.map X μ) t) fun (y : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) y) fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₁ :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ
      (Measure.restrict (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) t) fun (y : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) y) fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₂ :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ
      (Measure.restrict (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) t) fun (y : β) ↦
      @integral _ _ _ _ inst ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) y)
        fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₃ :
  Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) (SProd.sprod (β := Set Ω) t univ)) fun (x : β × Ω) ↦
      f x)
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₄ :
  Eq.{u_4 + 1} (α := F) (∫ (x : α) in (fun (a : α) ↦ (X a, Y a)) ⁻¹' SProd.sprod (β := Set Ω) t univ, f (X x, Y x) ∂μ)
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₅ :
  Eq.{u_4 + 1} (α := F) (∫ (x : α) in X ⁻¹' t ∩ Y ⁻¹' univ, f (X x, Y x) ∂μ) (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
refine_2₆ : Eq.{u_4 + 1} (α := F) (∫ (x : α) in X ⁻¹' t ∩ univ, f (X x, Y x) ∂μ) (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
⊢ Eq.{u_4 + 1} (α := F)
    (@integral _ _ _ _ mβ (Measure.map X (μ.restrict (X ⁻¹' t))) fun (y : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) y) fun (y_1 : Ω) ↦ f (y, y_1))
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
have refine_2₇ : Eq.{u_4 + 1} (α := F) (∫ (x : α) in X ⁻¹' t, f (X x, Y x) ∂μ) (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)
Tactic: rw [← Measure.restrict_map hX ht, ← Measure.fst_map_prodMk₀ hY, condDistrib,
      Measure.setIntegral_condKernel_univ_right ht hf_int.integrableOn,
      setIntegral_map (ht.prod MeasurableSet.univ) hf_int.1 (hX.aemeasurable.prodMk hY),
      mk_preimage_prod, preimage_univ, inter_univ]
-- 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
inst_6 : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
hf_int : Integrable.{u_4, u_1} (ε := F) (fun (a : α) ↦ f (X a, Y a)) μ
⊢ @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
have rwa : Integrable (f ∘ fun (a : α) ↦ (X a, Y a)) μ
Tactic: rwa [integrable_map_measure hf (hX.aemeasurable.prodMk 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
inst_6 : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf : StronglyMeasurable f
hf_int : Integrable.{u_4, u_1} (ε := F) (fun (a : α) ↦ f (X a, Y a)) μ
⊢ @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
have rwa : Integrable (f ∘ fun (x : α) ↦ (X x, Y x)) μ
Tactic: rwa [integrable_map_measure hf.aestronglyMeasurable (hX.aemeasurable.prodMk hY)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (β := F) (m₀ := Prod.instMeasurableSpace) (fun (x : β × Ω) ↦ f x.2)
    (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
have refine : (ae (F := Measure (β × Ω)) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)).EventuallyEq (β := F) (fun (x : β × Ω) ↦ f x.2)
  fun (x : β × Ω) ↦ AEStronglyMeasurable.mk f hf x.2
Tactic: refine ⟨fun x => hf.mk f x.2, hf.stronglyMeasurable_mk.comp_measurable measurable_snd, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
⊢ (ae (F := Measure (β × Ω)) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)).EventuallyEq (β := F) (fun (x : β × Ω) ↦ f x.2)
    fun (x : β × Ω) ↦ AEStronglyMeasurable.mk f hf x.2
have suffices : Measure.QuasiMeasurePreserving (α := β × Ω) (m0 := Prod.instMeasurableSpace) Prod.snd
  (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ) μ
Tactic: suffices h : Measure.QuasiMeasurePreserving Prod.snd (μ.map fun ω ↦ (X ω, ω)) μ from
    Measure.QuasiMeasurePreserving.ae_eq h hf.ae_eq_mk
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
⊢ Measure.QuasiMeasurePreserving (α := β × Ω) (m0 := Prod.instMeasurableSpace) Prod.snd
    (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ) μ
have refine : ∀ (s : Set Ω) (hs : MeasurableSet s) (hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞)
    (((Measure.map (α := β × Ω) Prod.snd (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: refine ⟨measurable_snd, Measure.AbsolutelyContinuous.mk fun s hs hμs => ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (α := β × Ω) Prod.snd (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [Measure.map_apply measurable_snd hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have pos : ∀ (hX : AEMeasurable X μ),
  Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: by_cases hX : AEMeasurable X μ
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
pos :
  ∀ (hX : AEMeasurable X μ),
    Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have neg : ∀ (hX : ¬AEMeasurable X μ),
  Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: by_cases hX : AEMeasurable X μ
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : AEMeasurable X μ
⊢ Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have pos : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (preimage (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) (Prod.snd ⁻¹' s)) : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: rw [Measure.map_apply_of_aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : AEMeasurable X μ
pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (preimage (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) (Prod.snd ⁻¹' s)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have pos₁ : AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ
Tactic: rw [Measure.map_apply_of_aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : AEMeasurable X μ
pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (preimage (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) (Prod.snd ⁻¹' s)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
pos₁ : AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ
⊢ Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have pos₂ : MeasurableSet (α := β × Ω) (Prod.snd ⁻¹' s)
Tactic: rw [Measure.map_apply_of_aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : ¬AEMeasurable X μ
⊢ Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have neg : Eq (α := ℝ≥0∞) ((0 : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [Measure.map_of_not_aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : ¬AEMeasurable X μ
neg : Eq (α := ℝ≥0∞) ((0 : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have neg₁ : ¬AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ
Tactic: rw [Measure.map_of_not_aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : ¬AEMeasurable X μ
⊢ ¬AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ
have neg : ∀ (hX : AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ), AEMeasurable X μ
Tactic: contrapose hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
β : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
⊢ @Integrable F _ _ _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
have pos : ∀ (hX : AEMeasurable X μ),
  @Integrable F _ _ _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
Tactic: by_cases hX : AEMeasurable X μ
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
β : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
pos :
  ∀ (hX : AEMeasurable X μ),
    @Integrable F _ _ _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
⊢ @Integrable F _ _ _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
have neg : ∀ (hX : ¬AEMeasurable X μ),
  @Integrable F _ _ _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
Tactic: by_cases hX : AEMeasurable X μ
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (hypothesis)
Goal:
β : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable X μ
⊢ @Integrable F _ _ _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
have hf : AEStronglyMeasurable (β := F) (m₀ := Prod.instMeasurableSpace) (fun (x : β × Ω) ↦ f x.2)
  (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
Tactic: have hf := hf_int.1.comp_snd_map_prodMk X (mΩ := mΩ) (mβ := mβ)
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
Goal:
β : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable X μ
hf :
  AEStronglyMeasurable (β := F) (m₀ := Prod.instMeasurableSpace) (fun (x : β × Ω) ↦ f x.2)
    (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
⊢ @Integrable F _ _ _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
have pos : @HasFiniteIntegral _ F _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
Tactic: refine ⟨hf, ?_⟩