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 Ω
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)
⊢ 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₆ : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t ∩ Y ⁻¹' s)) = μ.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]
-- 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)
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)
⊢ 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₇ : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t ∩ Y ⁻¹' s)) = ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (hypothesis)
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)) μ)
⊢ 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)
have hf_int' : 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
-- 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)) μ
⊢ 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)
have 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 μ
Tactic: refine (ae_eq_condExp_of_forall_setIntegral_eq hX.comap_le hf_int' (fun s _ _ => ?_) ?_ ?_).symm
-- 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)) μ
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 μ
⊢ 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)
have 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) ∂μ)
Tactic: refine (ae_eq_condExp_of_forall_setIntegral_eq hX.comap_le hf_int' (fun s _ _ => ?_) ?_ ?_).symm
-- 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)) μ
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) ∂μ)
⊢ 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)
have 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))
  μ
Tactic: refine (ae_eq_condExp_of_forall_setIntegral_eq hX.comap_le hf_int' (fun s _ _ => ?_) ?_ ?_).symm
-- 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∞)
⊢ 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) ∂μ)
have 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) ∂μ)
Tactic: rw [← integral_map hX.aemeasurable (f := fun x' => ∫ y, f (x', y) ∂(condDistrib Y X μ) x')]
-- 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.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) ∂μ)
⊢ 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) ∂μ)
have 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)))
Tactic: rw [← integral_map hX.aemeasurable (f := fun x' => ∫ y, f (x', y) ∂(condDistrib Y X μ) x')]
-- 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∞)
⊢ 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)))
have 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)
Tactic: rw [← Measure.restrict_map hX ht]
-- 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∞)
⊢ 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)
  (@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) ∂μ)
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) ∂μ)
⊢ 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)
  (@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) ∂μ)
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) ∂μ)
⊢ 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)
  (@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) ∂μ)
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) ∂μ)
⊢ 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)
  (@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) ∂μ)
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]