awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
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)
refine_3₅ :
  (∫⁻ (a : α) in t,
        ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          s ∂μ).toReal =
    μ.real (t ∩ Y ⁻¹' s)
refine_3₆ : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t ∩ Y ⁻¹' s)) = μ.real (t ∩ Y ⁻¹' s)
refine_3₇ refine_3₈ :
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t ∩ Y ⁻¹' s)) = ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t ∩ Y ⁻¹' s))
⊢ 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 ∂μ)

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]

Premises used: le_rfl, Measurable.aemeasurable, MeasureTheory.measure_lt_top, ProbabilityTheory.measurable_condDistrib, Measurable.comap_le, ProbabilityTheory.condDistrib, Filter.Eventually.of_forall, Set.inter_comm, MeasureTheory.measureReal_def, MeasureTheory.integral_indicator_const, smul_eq_mul, ProbabilityTheory.setLIntegral_condDistrib_of_measurableSet, mul_one, Measurable.mono, DFunLike.coe, MeasureTheory.measureReal_restrict_apply, MeasureTheory.integral_toReal
-- 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 : Measurable X
hY : Measurable Y
hs : MeasurableSet s
⊢ AEStronglyMeasurable (β := ℝ)
    (fun (a : α) ↦ Measure.real (m := inst) (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) s) μ

Tactic:
(measurable_condDistrib hs).ennreal_toReal.aestronglyMeasurable

Premises used: ProbabilityTheory.measurable_condDistrib, Measurable.aestronglyMeasurable, MeasureTheory.Measure.real, Measurable.ennreal_toReal
-- 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 : Measurable X
hY : Measurable Y
hs : MeasurableSet s
⊢ AEStronglyMeasurable (β := ℝ)
    (fun (a : α) ↦ Measure.real (m := inst) (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) s) μ

Tactic:
exact (measurable_condDistrib hs).ennreal_toReal.aestronglyMeasurable

Premises used: ProbabilityTheory.measurable_condDistrib, Measurable.aestronglyMeasurable, Measurable.ennreal_toReal
-- Module: Mathlib.Probability.Kernel.CondDistrib
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)) μ)
⊢ Integrable.{u_4, u_1} (ε := F) (fun (a : α) ↦ f (X a, Y a)) μ

Tactic:
have hf_int' : Integrable (fun a => f (X a, Y a)) μ :=
    (integrable_map_measure hf_int.1 (hX.aemeasurable.prodMk hY)).mp hf_int
-- Module: Mathlib.Probability.Kernel.CondDistrib
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)) μ
⊢ EventuallyEq.{u_1, u_4} (β := F) (ae μ) μ[fun (a : α) ↦ f (X a, Y a) | MeasurableSpace.comap X mβ] fun (a : α) ↦
    @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) fun (y : Ω) ↦ f (X a, y)

Tactic:
(ae_eq_condExp_of_forall_setIntegral_eq hX.comap_le hf_int' (fun s _ _ => ?_) ?_ ?_).symm

Premises used: Measurable.comap_le, MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Kernel.CondDistrib
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)) μ
refine_1 :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn.{u_1, u_4} (ε := F)
          (fun (a : α) ↦
            @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) fun (y : Ω) ↦
              f (X a, y))
          s μ
refine_2 :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_4 + 1} (α := F)
          (∫ (x : α) in s,
            @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X x)) fun (y : Ω) ↦
              f (X x, y) ∂μ)
          (∫ (x : α) in s, f (X x, Y x) ∂μ)
refine_3 :
  AEStronglyMeasurable.{u_1, u_4} (β := F)
    (fun (a : α) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) fun (y : Ω) ↦ f (X a, y))
    μ
⊢ EventuallyEq.{u_1, u_4} (β := F) (ae μ) μ[fun (a : α) ↦ f (X a, Y a) | MeasurableSpace.comap X mβ] fun (a : α) ↦
    @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) fun (y : Ω) ↦ f (X a, y)

Tactic:
refine (ae_eq_condExp_of_forall_setIntegral_eq hX.comap_le hf_int' (fun s _ _ => ?_) ?_ ?_).symm

Premises used: Measurable.comap_le, MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Kernel.CondDistrib
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)) μ
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn.{u_1, u_4} (ε := F)
    (fun (a : α) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) fun (y : Ω) ↦ f (X a, y))
    s μ

Tactic:
(hf_int.integral_condDistrib hX.aemeasurable hY).integrableOn

Premises used: Measurable.aemeasurable, MeasureTheory.Integrable.integral_condDistrib, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.Probability.Kernel.CondDistrib
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)) μ
s : Set α
h : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn.{u_1, u_4} (ε := F)
    (fun (a : α) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) fun (y : Ω) ↦ f (X a, y))
    s μ

Tactic:
exact (hf_int.integral_condDistrib hX.aemeasurable hY).integrableOn

Premises used: Measurable.aemeasurable, MeasureTheory.Integrable.integral_condDistrib, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.Probability.Kernel.CondDistrib
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.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) ∂μ)
refine_2₁ :
  AEStronglyMeasurable.{u_2, u_4} (β := F) (m₀ := mβ)
    (fun (x' : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) x') fun (y : Ω) ↦ f (x', y))
    (Measure.map X (μ.restrict (X ⁻¹' t)))
⊢ Eq.{u_4 + 1} (α := F)
    (∫ (a : α) in X ⁻¹' t,
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) fun (y : Ω) ↦
        f (X a, y) ∂μ)
    (∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ)

Tactic:
rw [← integral_map hX.aemeasurable (f := fun x' => ∫ y, f (x', y) ∂(condDistrib Y X μ) x')]

Premises used: Measurable.aemeasurable, MeasureTheory.integral_map
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 :
  AEStronglyMeasurable.{u_2, u_4} (β := F) (m₀ := mβ)
    (fun (x' : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) x') fun (y : Ω) ↦ f (x', y))
    (Measure.restrict (Measure.map X μ) t)
⊢ AEStronglyMeasurable.{u_2, u_4} (β := F) (m₀ := mβ)
    (fun (x' : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) x') fun (y : Ω) ↦ f (x', y))
    (Measure.map X (μ.restrict (X ⁻¹' t)))

Tactic:
rw [← Measure.restrict_map hX ht]

Premises used: MeasureTheory.Measure.restrict_map
-- Module: Mathlib.Probability.Kernel.CondDistrib
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∞)
⊢ AEStronglyMeasurable.{u_2, u_4} (β := F) (m₀ := mβ)
    (fun (x' : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) x') fun (y : Ω) ↦ f (x', y))
    (Measure.restrict (Measure.map X μ) t)

Tactic:
(hf_int.1.integral_condDistrib_map hY).restrict

Premises used: MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map, MeasureTheory.AEStronglyMeasurable.restrict, And.left
-- Module: Mathlib.Probability.Kernel.CondDistrib
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∞)
⊢ AEStronglyMeasurable.{u_2, u_4} (β := F) (m₀ := mβ)
    (fun (x' : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) x') fun (y : Ω) ↦ f (x', y))
    (Measure.restrict (Measure.map X μ) t)

Tactic:
exact (hf_int.1.integral_condDistrib_map hY).restrict

Premises used: MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map, MeasureTheory.AEStronglyMeasurable.restrict, And.left
-- Module: Mathlib.Probability.Kernel.CondDistrib
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)) μ
⊢ AEStronglyMeasurable.{u_1, u_4} (β := F)
    (fun (a : α) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) fun (y : Ω) ↦ f (X a, y))
    μ

Tactic:
aestronglyMeasurable_integral_condDistrib hX.aemeasurable hY hf_int.1

Premises used: Measurable.aemeasurable, ProbabilityTheory.aestronglyMeasurable_integral_condDistrib, And.left
-- Module: Mathlib.Probability.Kernel.CondDistrib
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)) μ
⊢ AEStronglyMeasurable.{u_1, u_4} (β := F)
    (fun (a : α) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) fun (y : Ω) ↦ f (X a, y))
    μ

Tactic:
exact aestronglyMeasurable_integral_condDistrib hX.aemeasurable hY hf_int.1

Premises used: Measurable.aemeasurable, ProbabilityTheory.aestronglyMeasurable_integral_condDistrib, And.left
-- Module: Mathlib.Probability.Kernel.CondDistrib
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)) μ
rwa rwa₁ rwa₂ rwa₃ : Integrable (f ∘ fun (a : α) ↦ (X a, Y a)) μ
⊢ @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)

Tactic:
rwa [integrable_map_measure hf (hX.aemeasurable.prodMk hY)]

Premises used: Measurable.aemeasurable, AEMeasurable.prodMk, MeasureTheory.integrable_map_measure
-- Module: Mathlib.Probability.Kernel.CondDistrib
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)) μ
rwa rwa₁ rwa₂ rwa₃ : Integrable (f ∘ fun (x : α) ↦ (X x, Y x)) μ
⊢ @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)

Tactic:
rwa [integrable_map_measure hf.aestronglyMeasurable (hX.aemeasurable.prodMk hY)]

Premises used: Measurable.aemeasurable, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, AEMeasurable.prodMk, MeasureTheory.integrable_map_measure
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 β
inst_5 : NormedSpace ℝ F
inst_6 : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
f : Ω → F
hf : StronglyMeasurable f
hf_int : Integrable.{u_4, u_1} (ε := F) (fun (a : α) ↦ f (Y a)) μ
⊢ EventuallyEq.{u_1, u_4} (β := F) (ae μ) μ[fun (a : α) ↦ f (Y a) | MeasurableSpace.comap X mβ] fun (a : α) ↦
    @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) fun (y : Ω) ↦ f y

Tactic:
condExp_prod_ae_eq_integral_condDistrib hX hY (hf.comp_measurable measurable_snd) hf_int

Premises used: ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib, MeasureTheory.StronglyMeasurable.comp_measurable, measurable_snd
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
X : α → β
mβ : MeasurableSpace β
Ω : Type u_5
inst_1 : NormedAddCommGroup Ω
inst_2 : NormedSpace ℝ Ω
inst_3 : CompleteSpace Ω
inst_4 : MeasurableSpace Ω
inst_5 : BorelSpace Ω
inst_6 : SecondCountableTopology Ω
Y : α → Ω
hX : Measurable X
hY_int : Integrable Y μ
⊢ μ[Y | MeasurableSpace.comap X mβ] =ᶠ[ae μ] fun (a : α) ↦
    @integral _ _ _ _ inst_4 (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) fun (y : Ω) ↦ y

Tactic:
condExp_ae_eq_integral_condDistrib hX hY_int.1.aemeasurable stronglyMeasurable_id hY_int

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, ProbabilityTheory.condExp_ae_eq_integral_condDistrib, stronglyMeasurable_id, And.left
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 ω, ω)) μ)

Tactic:
⟨fun x => hf.mk f x.2, hf.stronglyMeasurable_mk.comp_measurable measurable_snd, ?_⟩

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.StronglyMeasurable.comp_measurable, MeasureTheory.AEStronglyMeasurable.mk, measurable_snd, And.intro, Exists.intro, Prod.snd, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 μ
refine :
  (ae (F := Measure (β × Ω)) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)).EventuallyEq (β := F) (fun (x : β × Ω) ↦ f x.2)
    fun (x : β × Ω) ↦ AEStronglyMeasurable.mk f hf x.2
⊢ AEStronglyMeasurable (β := F) (m₀ := Prod.instMeasurableSpace) (fun (x : β × Ω) ↦ f x.2)
    (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)

Tactic:
refine ⟨fun x => hf.mk f x.2, hf.stronglyMeasurable_mk.comp_measurable measurable_snd, ?_⟩
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 μ
suffices :
  Measure.QuasiMeasurePreserving (α := β × Ω) (m0 := Prod.instMeasurableSpace) Prod.snd
    (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ) μ
⊢ (ae (F := Measure (β × Ω)) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)).EventuallyEq (β := F) (fun (x : β × Ω) ↦ f x.2)
    fun (x : β × Ω) ↦ AEStronglyMeasurable.mk f hf x.2

Tactic:
suffices h : Measure.QuasiMeasurePreserving Prod.snd (μ.map fun ω ↦ (X ω, ω)) μ from
    Measure.QuasiMeasurePreserving.ae_eq h hf.ae_eq_mk
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 ω, ω)) μ) μ

Tactic:
⟨measurable_snd, Measure.AbsolutelyContinuous.mk fun s hs hμs => ?_⟩

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk, MeasureTheory.Measure.QuasiMeasurePreserving.mk, measurable_snd
-- Module: Mathlib.Probability.Kernel.CondDistrib
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 μ
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∞)
⊢ Measure.QuasiMeasurePreserving (α := β × Ω) (m0 := Prod.instMeasurableSpace) Prod.snd
    (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ) μ

Tactic:
refine ⟨measurable_snd, Measure.AbsolutelyContinuous.mk fun s hs hμs => ?_⟩