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

Tactic:
calc
      ∫⁻ a, condDistrib Y X μ (X a) s ∂μ ≤ ∫⁻ _, 1 ∂μ := lintegral_mono fun a => prob_le_one
      _ = μ univ := lintegral_one
      _ < ∞ := measure_lt_top _ _

Premises used: MeasureTheory.measure_lt_top, Set.univ, MeasureTheory.prob_le_one, MeasureTheory.lintegral_mono, DFunLike.coe, MeasureTheory.lintegral_one
-- 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
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
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)
⊢ ∀ᵐ (b : β) ∂Measure.map X μ,
    @Integrable.{u_4, u_3} F _ _ _ inst (fun (ω : Ω) ↦ f (b, ω))
      (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) b)

Tactic:
rw [condDistrib, ← Measure.fst_map_prodMk₀ (X := X) hY]

Premises used: ProbabilityTheory.condDistrib, MeasureTheory.Measure.fst_map_prodMk₀
-- 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
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
⊢ ∀ᵐ (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:
hf_int.condKernel_ae

Premises used: MeasureTheory.Integrable.condKernel_ae
-- 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
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
⊢ ∀ᵐ (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:
exact hf_int.condKernel_ae

Premises used: MeasureTheory.Integrable.condKernel_ae
-- 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
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
⊢ ∀ᵐ (a : α) ∂μ,
    @Integrable.{u_4, u_3} F _ _ _ inst (fun (ω : Ω) ↦ f (X a, ω))
      (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a))

Tactic:
ae_of_ae_map hX (hf_int.condDistrib_ae_map hY)

Premises used: MeasureTheory.ae_of_ae_map, MeasureTheory.Integrable.condDistrib_ae_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
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
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)) μ))
⊢ @Integrable ℝ _ _ _ mβ
    (fun (x : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) x) fun (y : Ω) ↦ ‖f (x, y)‖)
    (Measure.map X μ)

Tactic:
rw [condDistrib, ← Measure.fst_map_prodMk₀ (X := X) hY]

Premises used: ProbabilityTheory.condDistrib, MeasureTheory.Measure.fst_map_prodMk₀
-- 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
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
⊢ @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:
hf_int.integral_norm_condKernel

Premises used: MeasureTheory.Integrable.integral_norm_condKernel
-- 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
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
⊢ @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:
exact hf_int.integral_norm_condKernel

Premises used: MeasureTheory.Integrable.integral_norm_condKernel
-- 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
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
⊢ Integrable (ε := ℝ)
    (fun (a : α) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) fun (y : Ω) ↦
        ‖f (X a, y)‖)
    μ

Tactic:
(hf_int.integral_norm_condDistrib_map hY).comp_aemeasurable hX

Premises used: MeasureTheory.Integrable.comp_aemeasurable, MeasureTheory.Integrable.integral_norm_condDistrib_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
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
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)) μ))
⊢ @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 μ)

Tactic:
rw [condDistrib, ← Measure.fst_map_prodMk₀ (X := X) hY]

Premises used: ProbabilityTheory.condDistrib, MeasureTheory.Measure.fst_map_prodMk₀
-- 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
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
          ((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:
hf_int.norm_integral_condKernel

Premises used: MeasureTheory.Integrable.norm_integral_condKernel
-- 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
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
          ((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:
exact hf_int.norm_integral_condKernel

Premises used: MeasureTheory.Integrable.norm_integral_condKernel
-- 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
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
⊢ Integrable (ε := ℝ)
    (fun (a : α) ↦
      norm.{u_4} (E := F)
        (@integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) fun (y : Ω) ↦
          f (X a, y)))
    μ

Tactic:
(hf_int.norm_integral_condDistrib_map hY).comp_aemeasurable hX

Premises used: MeasureTheory.Integrable.comp_aemeasurable, MeasureTheory.Integrable.norm_integral_condDistrib_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
hY : AEMeasurable Y μ
hf_int : @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
⊢ @Integrable.{u_4, u_2} F _ _ _ mβ
    (fun (x : β) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) x) fun (y : Ω) ↦ f (x, y))
    (Measure.map X μ)

Tactic:
(integrable_norm_iff (hf_int.1.integral_condDistrib_map hY)).mp
    (hf_int.norm_integral_condDistrib_map hY)

Premises used: MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map, MeasureTheory.integrable_norm_iff, MeasureTheory.Integrable.norm_integral_condDistrib_map, And.left, Iff.mp
-- 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
hX : AEMeasurable 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 : α) ↦
      @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) fun (y : Ω) ↦ f (X a, y))
    μ

Tactic:
(hf_int.integral_condDistrib_map hY).comp_aemeasurable hX

Premises used: MeasureTheory.Integrable.comp_aemeasurable, MeasureTheory.Integrable.integral_condDistrib_map
-- 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 Ω
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∞)
rw₆ rw₇ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t ∩ Y ⁻¹' 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)

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]

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.restrict_map, ProbabilityTheory.condDistrib, MeasurableSet.prod, AEMeasurable.prodMk, MeasureTheory.Measure.map_apply_of_aemeasurable, MeasureTheory.Measure.fst_map_prodMk₀, MeasureTheory.lintegral_map, ProbabilityTheory.Kernel.measurable_coe, MeasureTheory.Measure.setLIntegral_condKernel_eq_measure_prod, Set.mk_preimage_prod
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
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)
⊢ ∫⁻ (a : α) in t,
      ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s ∂μ =
    (μ : (a : Set α) → ℝ≥0∞) (t ∩ Y ⁻¹' s)

Tactic:
obtain ⟨t', ht', rfl⟩ := ht

Premises used: rfl
-- 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 : AEMeasurable Y μ
hs : MeasurableSet s
t' : Set β
ht' : MeasurableSet t'
rw rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' t' ∩ Y ⁻¹' 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)

Tactic:
rw [setLIntegral_preimage_condDistrib hX hY hs ht']

Premises used: ProbabilityTheory.setLIntegral_preimage_condDistrib
-- 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
⊢ (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β]

Tactic:
ae_eq_condExp_of_forall_setIntegral_eq hX.comap_le ?_ ?_ ?_ ?_

Premises used: Measurable.comap_le, MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq
-- 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
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 ∂μ)
refine_4 :
  AEStronglyMeasurable (β := ℝ)
    (fun (a : α) ↦ Measure.real (m := inst) (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) 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β]

Tactic:
refine ae_eq_condExp_of_forall_setIntegral_eq hX.comap_le ?_ ?_ ?_ ?_

Premises used: Measurable.comap_le, MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq
-- 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
⊢ Integrable (ε := ℝ) ((Y ⁻¹' s).indicator fun (ω : α) ↦ 1) μ

Tactic:
(integrable_const _).indicator (hY hs)

Premises used: MeasureTheory.Integrable.indicator
-- 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
⊢ Integrable (ε := ℝ) ((Y ⁻¹' s).indicator fun (ω : α) ↦ 1) μ

Tactic:
exact (integrable_const _).indicator (hY hs)

Premises used: MeasureTheory.Integrable.indicator
-- 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
⊢ ∀ (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:
fun t _ _ => (integrable_toReal_condDistrib hX.aemeasurable hs).integrableOn

Premises used: Measurable.aemeasurable, MeasureTheory.Integrable.integrableOn, ProbabilityTheory.integrable_toReal_condDistrib
-- 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
⊢ ∀ (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:
exact fun t _ _ => (integrable_toReal_condDistrib hX.aemeasurable hs).integrableOn

Premises used: Measurable.aemeasurable, MeasureTheory.Integrable.integrableOn, ProbabilityTheory.integrable_toReal_condDistrib
-- 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
refine_3 :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ)
      (∫ (x : α) in t, Measure.real (m := inst) (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X x)) s ∂μ)
      (∫ (x : α) in t, (Y ⁻¹' s).indicator (fun (ω : α) ↦ 1) x ∂μ)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ)
      (∫ (x : α) in t, Measure.real (m := inst) (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X x)) s ∂μ)
      (∫ (x : α) in t, (Y ⁻¹' s).indicator (fun (ω : α) ↦ 1) x ∂μ)

Tactic:
_