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 μ
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)
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)
⊢ ∫⁻ (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₄ : Eq (α := ℝ≥0∞) ((Measure.map (fun (a : α) ↦ (X a, Y a)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (t ×ˢ s) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s) : ℝ≥0∞)
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)
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)
rw₄ :
  Eq (α := ℝ≥0∞) ((Measure.map (fun (a : α) ↦ (X a, Y a)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (t ×ˢ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s) : ℝ≥0∞)
⊢ ∫⁻ (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₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (X x, Y x)) ⁻¹' t ×ˢ s) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s) : ℝ≥0∞)
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)
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)
rw₄ :
  Eq (α := ℝ≥0∞) ((Measure.map (fun (a : α) ↦ (X a, Y a)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (t ×ˢ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s) : ℝ≥0∞)
rw₅ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (X x, Y x)) ⁻¹' t ×ˢ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s) : ℝ≥0∞)
⊢ ∫⁻ (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₆ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' s) : ℝ≥0∞)
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 Ω
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ∫⁻ (a : α) in t,
      ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ =
    (μ : (a : Set α) → ℝ≥0∞) (t ∩ Y ⁻¹' s)
have obtain : ∀ (t' : Set β) (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)
Tactic: obtain ⟨t', ht', rfl⟩ := ht
Cleared hypotheses: t, ht
-- 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 : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
t' : Set β
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 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t' ∩ Y ⁻¹' s) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t' ∩ Y ⁻¹' s) : ℝ≥0∞)
Tactic: rw [setLIntegral_preimage_condDistrib hX hY hs ht']
-- 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 : Measurable X
hY : Measurable Y
hs : MeasurableSet s
⊢ (ae μ).EventuallyEq (β := ℝ)
    (fun (a : α) ↦ Measure.real (m := inst) (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) s)
    μ[(Y ⁻¹' s).indicator fun (ω : α) ↦ 1 | MeasurableSpace.comap X mβ]
have refine_1 : Integrable (ε := ℝ) ((Y ⁻¹' s).indicator fun (ω : α) ↦ 1) μ
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hX.comap_le ?_ ?_ ?_ ?_
-- 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 : Measurable X
hY : Measurable Y
hs : MeasurableSet s
refine_1 : Integrable (ε := ℝ) ((Y ⁻¹' s).indicator fun (ω : α) ↦ 1) μ
⊢ (ae μ).EventuallyEq (β := ℝ)
    (fun (a : α) ↦ Measure.real (m := inst) (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) s)
    μ[(Y ⁻¹' s).indicator fun (ω : α) ↦ 1 | MeasurableSpace.comap X mβ]
have refine_2 : ∀ (s_1 : Set α),
  MeasurableSet s_1 →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
      IntegrableOn (ε := ℝ)
        (fun (a : α) ↦ Measure.real (m := inst) (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) s) s_1
        μ
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hX.comap_le ?_ ?_ ?_ ?_
-- 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 : Measurable X
hY : Measurable Y
hs : MeasurableSet s
refine_1 : Integrable (ε := ℝ) ((Y ⁻¹' s).indicator fun (ω : α) ↦ 1) μ
refine_2 :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ)
          (fun (a : α) ↦ Measure.real (m := inst) (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) s)
          s_1 μ
⊢ (ae μ).EventuallyEq (β := ℝ)
    (fun (a : α) ↦ Measure.real (m := inst) (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) s)
    μ[(Y ⁻¹' s).indicator fun (ω : α) ↦ 1 | MeasurableSpace.comap X mβ]
have refine_3 : ∀ (s_1 : Set α),
  MeasurableSet s_1 →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq (α := ℝ)
        (∫ (x : α) in s_1,
          Measure.real (m := inst) (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X x)) s ∂μ)
        (∫ (x : α) in s_1, (Y ⁻¹' s).indicator (fun (ω : α) ↦ 1) x ∂μ)
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hX.comap_le ?_ ?_ ?_ ?_
-- 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 : Measurable X
hY : Measurable Y
hs : MeasurableSet s
refine_1 : Integrable (ε := ℝ) ((Y ⁻¹' s).indicator fun (ω : α) ↦ 1) μ
refine_2 :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ)
          (fun (a : α) ↦ Measure.real (m := inst) (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) s)
          s_1 μ
refine_3 :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ)
          (∫ (x : α) in s_1,
            Measure.real (m := inst) (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X x)) s ∂μ)
          (∫ (x : α) in s_1, (Y ⁻¹' s).indicator (fun (ω : α) ↦ 1) x ∂μ)
⊢ (ae μ).EventuallyEq (β := ℝ)
    (fun (a : α) ↦ Measure.real (m := inst) (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) s)
    μ[(Y ⁻¹' s).indicator fun (ω : α) ↦ 1 | MeasurableSpace.comap X mβ]
have refine_4 : AEStronglyMeasurable (β := ℝ)
  (fun (a : α) ↦ Measure.real (m := inst) (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) s) μ
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hX.comap_le ?_ ?_ ?_ ?_
-- 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 : Measurable X
hY : Measurable Y
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ)
    (∫ (x : α) in t,
      ENNReal.toReal
        (((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) ∂μ)
    (∫ (x : α) in t, (Y ⁻¹' s).indicator (fun (ω : α) ↦ 1) x ∂μ)
have refine_3 : (∫⁻ (a : α) in t,
      ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ).toReal =
  ∫ (x : α) in t, (Y ⁻¹' s).indicator (fun (ω : α) ↦ 1) x ∂μ
Tactic: rw [integral_toReal ((measurable_condDistrib hs).mono hX.comap_le le_rfl).aemeasurable
      (Eventually.of_forall fun ω => measure_lt_top (condDistrib Y X μ (X ω)) _),
      integral_indicator_const _ (hY hs), measureReal_restrict_apply (hY hs), smul_eq_mul, mul_one,
      inter_comm, setLIntegral_condDistrib_of_measurableSet hX hY.aemeasurable hs ht,
      measureReal_def]
-- 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 : Measurable X
hY : Measurable Y
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_3 :
  (∫⁻ (a : α) in t,
        ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          s ∂μ).toReal =
    ∫ (x : α) in t, (Y ⁻¹' s).indicator (fun (ω : α) ↦ 1) x ∂μ
⊢ Eq (α := ℝ)
    (∫ (x : α) in t,
      ENNReal.toReal
        (((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) ∂μ)
    (∫ (x : α) in t, (Y ⁻¹' s).indicator (fun (ω : α) ↦ 1) x ∂μ)
have refine_3₁ : (∫⁻ (a : α) in t,
      ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ).toReal =
  HSMul.hSMul (β := ℝ) ((μ.restrict t).real (Y ⁻¹' s)) 1
Tactic: rw [integral_toReal ((measurable_condDistrib hs).mono hX.comap_le le_rfl).aemeasurable
      (Eventually.of_forall fun ω => measure_lt_top (condDistrib Y X μ (X ω)) _),
      integral_indicator_const _ (hY hs), measureReal_restrict_apply (hY hs), smul_eq_mul, mul_one,
      inter_comm, setLIntegral_condDistrib_of_measurableSet hX hY.aemeasurable hs ht,
      measureReal_def]
-- 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 : Measurable X
hY : Measurable Y
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_3 :
  (∫⁻ (a : α) in t,
        ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          s ∂μ).toReal =
    ∫ (x : α) in t, (Y ⁻¹' s).indicator (fun (ω : α) ↦ 1) x ∂μ
refine_3₁ :
  (∫⁻ (a : α) in t,
        ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          s ∂μ).toReal =
    HSMul.hSMul (β := ℝ) ((μ.restrict t).real (Y ⁻¹' s)) 1
⊢ Eq (α := ℝ)
    (∫ (x : α) in t,
      ENNReal.toReal
        (((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) ∂μ)
    (∫ (x : α) in t, (Y ⁻¹' s).indicator (fun (ω : α) ↦ 1) x ∂μ)
have refine_3₂ : (∫⁻ (a : α) in t,
      ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ).toReal =
  HSMul.hSMul (β := ℝ) (μ.real (Y ⁻¹' s ∩ t)) 1
Tactic: rw [integral_toReal ((measurable_condDistrib hs).mono hX.comap_le le_rfl).aemeasurable
      (Eventually.of_forall fun ω => measure_lt_top (condDistrib Y X μ (X ω)) _),
      integral_indicator_const _ (hY hs), measureReal_restrict_apply (hY hs), smul_eq_mul, mul_one,
      inter_comm, setLIntegral_condDistrib_of_measurableSet hX hY.aemeasurable hs ht,
      measureReal_def]
-- 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 : Measurable X
hY : Measurable Y
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_3 :
  (∫⁻ (a : α) in t,
        ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          s ∂μ).toReal =
    ∫ (x : α) in t, (Y ⁻¹' s).indicator (fun (ω : α) ↦ 1) x ∂μ
refine_3₁ :
  (∫⁻ (a : α) in t,
        ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          s ∂μ).toReal =
    HSMul.hSMul (β := ℝ) ((μ.restrict t).real (Y ⁻¹' s)) 1
refine_3₂ :
  (∫⁻ (a : α) in t,
        ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          s ∂μ).toReal =
    HSMul.hSMul (β := ℝ) (μ.real (Y ⁻¹' s ∩ t)) 1
⊢ Eq (α := ℝ)
    (∫ (x : α) in t,
      ENNReal.toReal
        (((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) ∂μ)
    (∫ (x : α) in t, (Y ⁻¹' s).indicator (fun (ω : α) ↦ 1) x ∂μ)
have refine_3₃ : (∫⁻ (a : α) in t,
      ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ).toReal =
  μ.real (Y ⁻¹' s ∩ t) * 1
Tactic: rw [integral_toReal ((measurable_condDistrib hs).mono hX.comap_le le_rfl).aemeasurable
      (Eventually.of_forall fun ω => measure_lt_top (condDistrib Y X μ (X ω)) _),
      integral_indicator_const _ (hY hs), measureReal_restrict_apply (hY hs), smul_eq_mul, mul_one,
      inter_comm, setLIntegral_condDistrib_of_measurableSet hX hY.aemeasurable hs ht,
      measureReal_def]
-- 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 : Measurable X
hY : Measurable Y
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_3 :
  (∫⁻ (a : α) in t,
        ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          s ∂μ).toReal =
    ∫ (x : α) in t, (Y ⁻¹' s).indicator (fun (ω : α) ↦ 1) x ∂μ
refine_3₁ :
  (∫⁻ (a : α) in t,
        ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          s ∂μ).toReal =
    HSMul.hSMul (β := ℝ) ((μ.restrict t).real (Y ⁻¹' s)) 1
refine_3₂ :
  (∫⁻ (a : α) in t,
        ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          s ∂μ).toReal =
    HSMul.hSMul (β := ℝ) (μ.real (Y ⁻¹' s ∩ t)) 1
refine_3₃ :
  (∫⁻ (a : α) in t,
        ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          s ∂μ).toReal =
    μ.real (Y ⁻¹' s ∩ t) * 1
⊢ Eq (α := ℝ)
    (∫ (x : α) in t,
      ENNReal.toReal
        (((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) ∂μ)
    (∫ (x : α) in t, (Y ⁻¹' s).indicator (fun (ω : α) ↦ 1) x ∂μ)
have refine_3₄ : (∫⁻ (a : α) in t,
      ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ).toReal =
  μ.real (Y ⁻¹' s ∩ t)
Tactic: rw [integral_toReal ((measurable_condDistrib hs).mono hX.comap_le le_rfl).aemeasurable
      (Eventually.of_forall fun ω => measure_lt_top (condDistrib Y X μ (X ω)) _),
      integral_indicator_const _ (hY hs), measureReal_restrict_apply (hY hs), smul_eq_mul, mul_one,
      inter_comm, setLIntegral_condDistrib_of_measurableSet hX hY.aemeasurable hs ht,
      measureReal_def]
-- 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 : Measurable X
hY : Measurable Y
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_3 :
  (∫⁻ (a : α) in t,
        ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          s ∂μ).toReal =
    ∫ (x : α) in t, (Y ⁻¹' s).indicator (fun (ω : α) ↦ 1) x ∂μ
refine_3₁ :
  (∫⁻ (a : α) in t,
        ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          s ∂μ).toReal =
    HSMul.hSMul (β := ℝ) ((μ.restrict t).real (Y ⁻¹' s)) 1
refine_3₂ :
  (∫⁻ (a : α) in t,
        ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          s ∂μ).toReal =
    HSMul.hSMul (β := ℝ) (μ.real (Y ⁻¹' s ∩ t)) 1
refine_3₃ :
  (∫⁻ (a : α) in t,
        ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          s ∂μ).toReal =
    μ.real (Y ⁻¹' s ∩ t) * 1
refine_3₄ :
  (∫⁻ (a : α) in t,
        ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          s ∂μ).toReal =
    μ.real (Y ⁻¹' s ∩ t)
⊢ Eq (α := ℝ)
    (∫ (x : α) in t,
      ENNReal.toReal
        (((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) ∂μ)
    (∫ (x : α) in t, (Y ⁻¹' s).indicator (fun (ω : α) ↦ 1) x ∂μ)
have refine_3₅ : (∫⁻ (a : α) in t,
      ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ).toReal =
  μ.real (t ∩ Y ⁻¹' s)
Tactic: rw [integral_toReal ((measurable_condDistrib hs).mono hX.comap_le le_rfl).aemeasurable
      (Eventually.of_forall fun ω => measure_lt_top (condDistrib Y X μ (X ω)) _),
      integral_indicator_const _ (hY hs), measureReal_restrict_apply (hY hs), smul_eq_mul, mul_one,
      inter_comm, setLIntegral_condDistrib_of_measurableSet hX hY.aemeasurable hs ht,
      measureReal_def]