awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : IsFiniteKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
ν : Measure α
inst_3 : IsFiniteMeasure ν
h :
  ∀ (p : α × β) (hp : (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η) p = μ.rnDeriv ν p.1),
    ((μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) * (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η)) p = μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p
⊢ (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) * (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)] fun (p : α × β) ↦
    μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p

Tactic:
filter_upwards [rnDeriv_measure_compProd_left μ ν η] with p hp

Premises used: ProbabilityTheory.rnDeriv_measure_compProd_left
-- Module: Mathlib.Probability.Kernel.Composition.RadonNikodym
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteKernel κ
inst_2 : IsFiniteKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
ν : Measure α
inst_3 : IsFiniteMeasure ν
p : α × β
hp : (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η) p = μ.rnDeriv ν p.1
h : (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p * (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η) p = μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p
h₁ : (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p * μ.rnDeriv ν p.1 = μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p
h₂ h₃ : μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p = μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p
⊢ ((μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) * (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η)) p = μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p

Tactic:
rw [Pi.mul_apply, hp, mul_comm]

Premises used: Pi.mul_apply, mul_comm
-- 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 : α → Ω
inst_5 : MeasurableSpace β
rw :
  IsMarkovKernel.{u_2, u_3} (α := β) (β := Ω) (mα := inst_5) (mβ := inst)
    (Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ))
⊢ IsMarkovKernel (mα := inst_5) (mβ := inst) (condDistrib Y X μ)

Tactic:
rw [condDistrib]

Premises used: ProbabilityTheory.condDistrib
-- 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 : α → Ω
inst_5 : MeasurableSpace β
⊢ IsMarkovKernel.{u_2, u_3} (α := β) (β := Ω) (mα := inst_5) (mβ := inst)
    (Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ))

Tactic:
infer_instance
-- 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 β
inst_4 : MeasurableSingletonClass β
hY : Measurable Y
x : β
hX : Ne (α := ℝ≥0∞) (((Measure.map X μ : Measure β) : (a : Set β) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : Measure β) : (a : Set β) → ℝ≥0∞)
            {x})⁻¹ :
        ℝ≥0∞)
      ((Measure.map (fun (a : α) ↦ (X a, Y a)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (SProd.sprod (α := Set β) {x} s) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((Measure.map X μ : Measure β) : (a : Set β) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      ((Measure.map (fun (a : α) ↦ (X a, Y a)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (SProd.sprod (α := Set β) {x} s) : ℝ≥0∞)
rw₁ :
  Ne (α := ℝ≥0∞)
    (((Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : Measure β) : (a : Set β) → ℝ≥0∞)
        {x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((Measure.map X μ : Measure β) : (a : Set β) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      ((Measure.map (fun (a : α) ↦ (X a, Y a)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (SProd.sprod (α := Set β) {x} s) : ℝ≥0∞)

Tactic:
rw [condDistrib, Measure.condKernel_apply_of_ne_zero _ s]

Premises used: MeasureTheory.Measure.condKernel_apply_of_ne_zero, ProbabilityTheory.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 β
inst_4 : MeasurableSingletonClass β
hY : Measurable Y
x : β
hX : Ne (α := ℝ≥0∞) (((Measure.map X μ : Measure β) : (a : Set β) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
rw rw₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((Measure.map X μ : Measure β) : (a : Set β) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      ((Measure.map (fun (a : α) ↦ (X a, Y a)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (SProd.sprod (α := Set β) {x} s) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((Measure.map X μ : Measure β) : (a : Set β) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      ((Measure.map (fun (a : α) ↦ (X a, Y a)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (SProd.sprod (α := Set β) {x} s) : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : Measure β) : (a : Set β) → ℝ≥0∞)
            {x})⁻¹ :
        ℝ≥0∞)
      ((Measure.map (fun (a : α) ↦ (X a, Y a)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (SProd.sprod (α := Set β) {x} s) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((((Measure.map X μ : Measure β) : (a : Set β) → ℝ≥0∞) {x})⁻¹ : ℝ≥0∞)
      ((Measure.map (fun (a : α) ↦ (X a, Y a)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (SProd.sprod (α := Set β) {x} s) : ℝ≥0∞)

Tactic:
rw [Measure.fst_map_prodMk hY]

Premises used: MeasureTheory.Measure.fst_map_prodMk
-- 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 β
inst_4 : MeasurableSingletonClass β
hY : Measurable Y
x : β
hX : Ne (α := ℝ≥0∞) (((Measure.map X μ : Measure β) : (a : Set β) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
rwa rwa₁ rwa₂ rwa₃ : Ne (α := ℝ≥0∞) (((Measure.map X μ : Measure β) : (a : Set β) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞)
    (((Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : Measure β) : (a : Set β) → ℝ≥0∞)
        {x} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rwa [Measure.fst_map_prodMk hY]

Premises used: MeasureTheory.Measure.fst_map_prodMk
-- 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 β
hY : AEMeasurable Y μ
rw :
  Eq (α := Measure (β × Ω)) (Measure.map X μ ⊗ₘ Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ))
    (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
rw₁ :
  Eq (α := Measure (β × Ω))
    (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) ⊗ₘ
      Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ))
    (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
rw₂ rw₃ :
  Eq (α := Measure (β × Ω)) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
⊢ Eq (α := Measure (β × Ω)) (Measure.map X μ ⊗ₘ condDistrib Y X μ) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)

Tactic:
rw [condDistrib, ← Measure.fst_map_prodMk₀ hY, Measure.disintegrate]

Premises used: ProbabilityTheory.condDistrib, MeasureTheory.Measure.fst_map_prodMk₀, MeasureTheory.Measure.disintegrate
-- 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 β
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
rw : Eq (α := Measure Ω) (Measure.snd (Measure.map X μ ⊗ₘ condDistrib Y X μ)) (Measure.map Y μ)
rw₁ : Eq (α := Measure Ω) (Measure.snd.{u_2, u_3} (α := β) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) (Measure.map Y μ)
rw₂ rw₃ : Eq (α := Measure Ω) (Measure.map Y μ) (Measure.map Y μ)
⊢ Eq (α := Measure Ω) (Measure.bind (mα := mβ) (Measure.map X μ) (⇑(condDistrib Y X μ) : (a : β) → Measure Ω))
    (Measure.map Y μ)

Tactic:
rw [← Measure.snd_compProd, compProd_map_condDistrib hY, Measure.snd_map_prodMk₀ hX]

Premises used: MeasureTheory.Measure.snd_compProd, MeasureTheory.Measure.snd_map_prodMk₀, ProbabilityTheory.compProd_map_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 β
X' : α → β
Y' : α → Ω
hY : Y =ᶠ[ae μ] Y'
hX : X =ᶠ[ae μ] X'
rw :
  Eq (α := Kernel β Ω) (Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ))
    (Measure.condKernel (Measure.map (fun (a : α) ↦ (X' a, Y' a)) μ))
⊢ Eq (α := Kernel β Ω) (condDistrib Y X μ) (condDistrib Y' X' μ)

Tactic:
rw [condDistrib, condDistrib]

Premises used: ProbabilityTheory.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 β
X' : α → β
Y' : α → Ω
hY : Y =ᶠ[ae μ] Y'
hX : X =ᶠ[ae μ] X'
e_ρ : Eq (α := Measure (β × Ω)) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) (Measure.map (fun (a : α) ↦ (X' a, Y' a)) μ)
⊢ Eq (α := Kernel β Ω) (Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ))
    (Measure.condKernel (Measure.map (fun (a : α) ↦ (X' a, Y' a)) μ))

Tactic:
congr 1
-- 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 β
X' : α → β
Y' : α → Ω
hY : Y =ᶠ[ae μ] Y'
hX : X =ᶠ[ae μ] X'
e_ρ : (ae μ).EventuallyEq (β := β × Ω) (fun (a : α) ↦ (X a, Y a)) fun (a : α) ↦ (X' a, Y' a)
⊢ Eq (α := Measure (β × Ω)) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) (Measure.map (fun (a : α) ↦ (X' a, Y' a)) μ)

Tactic:
rw [Measure.map_congr]

Premises used: MeasureTheory.Measure.map_congr
-- 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 β
X' : α → β
Y' : α → Ω
hY : Y =ᶠ[ae μ] Y'
hX : X =ᶠ[ae μ] X'
a : α
ha : X a = X' a
hb : Y a = Y' a
rw : (X' a, Y a) = (X' a, Y' a)
rw₁ rw₂ : (X' a, Y' a) = (X' a, Y' a)
⊢ (X a, Y a) = (X' a, Y' a)

Tactic:
rw [ha, hb]
-- 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 β
X' : α → β
Y' : α → Ω
hY : Y =ᶠ[ae μ] Y'
hX : X =ᶠ[ae μ] X'
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ X x = X' x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Y x = Y' x) x} x →
                Membership.mem (γ := Set α)
                  {x : α |
                    (fun (x : α) ↦ Eq (α := β × Ω) ((fun (a : α) ↦ (X a, Y a)) x) ((fun (a : α) ↦ (X' a, Y' a)) x)) x}
                  x}
            x}
      a
h₁ h₂ : ∀ (a : α) (ha : X a = X' a) (hb : Y a = Y' a), (X a, Y a) = (X' a, Y' a)
⊢ (ae μ).EventuallyEq (β := β × Ω) (fun (a : α) ↦ (X a, Y a)) fun (a : α) ↦ (X' a, Y' a)

Tactic:
filter_upwards [hX, hY] with a ha hb using by rw [ha, hb]
-- 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 β
X' : α → β
hX : X =ᶠ[ae μ] X'
⊢ Y =ᶠ[ae μ] Y

Tactic:
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 β
Y' : α → Ω
hY : Y =ᶠ[ae μ] Y'
⊢ X =ᶠ[ae μ] X

Tactic:
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 Ω
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦
    ((((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s

Tactic:
(Kernel.measurable_coe _ hs).comp (Measurable.of_comap_le le_rfl)

Premises used: le_rfl, Measurable.comp, Measurable.of_comap_le, ProbabilityTheory.Kernel.measurable_coe
-- 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
hf : StronglyMeasurable f
rw :
  StronglyMeasurable.{u_2, u_4} (β := F) fun (x : β) ↦
    @integral _ _ _ _ inst ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) x)
      fun (y : Ω) ↦ f (x, y)
⊢ StronglyMeasurable.{u_2, u_4} (β := F) fun (x : β) ↦
    @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) x) fun (y : Ω) ↦ f (x, y)

Tactic:
rw [condDistrib]

Premises used: ProbabilityTheory.condDistrib
-- 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
hf : StronglyMeasurable f
⊢ StronglyMeasurable.{u_2, u_4} (β := F) fun (x : β) ↦
    @integral _ _ _ _ inst ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) x)
      fun (y : Ω) ↦ f (x, y)

Tactic:
hf.integral_kernel_prod_right'

Premises used: MeasureTheory.StronglyMeasurable.integral_kernel_prod_right'
-- 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
hf : StronglyMeasurable f
⊢ StronglyMeasurable.{u_2, u_4} (β := F) fun (x : β) ↦
    @integral _ _ _ _ inst ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) x)
      fun (y : Ω) ↦ f (x, y)

Tactic:
exact hf.integral_kernel_prod_right'

Premises used: MeasureTheory.StronglyMeasurable.integral_kernel_prod_right'
-- 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 : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
rw :
  AEStronglyMeasurable.{u_2, u_4} (β := F) (m₀ := 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)) μ))
⊢ 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 μ)

Tactic:
rw [← Measure.fst_map_prodMk₀ hY, condDistrib]

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 : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
⊢ AEStronglyMeasurable.{u_2, u_4} (β := F) (m₀ := 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.integral_condKernel

Premises used: MeasureTheory.AEStronglyMeasurable.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 : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
⊢ AEStronglyMeasurable.{u_2, u_4} (β := F) (m₀ := 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.integral_condKernel

Premises used: MeasureTheory.AEStronglyMeasurable.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 : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f (Measure.map (fun (a : α) ↦ (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:
(hf.integral_condDistrib_map hY).comp_aemeasurable hX

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

Tactic:
(hf.integral_condDistrib).comp_measurable <| Measurable.of_comap_le le_rfl

Premises used: le_rfl, Measurable.of_comap_le, MeasureTheory.StronglyMeasurable.integral_condDistrib, MeasureTheory.StronglyMeasurable.comp_measurable
-- 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 : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f (Measure.map (fun (a : α) ↦ (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:
(hf.integral_condDistrib_map hY).comp_ae_measurable' hX

Premises used: MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map, MeasureTheory.AEStronglyMeasurable.comp_ae_measurable'
-- 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 β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
h :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((Measure.map X μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ) : Measure β) : (a : Set β) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ Eq (α := Measure β) (Measure.map X μ) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))

Tactic:
ext s hs
-- 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 β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β × Ω) (fun (x : α) ↦ (X x, Y x)) (Prod.fst ⁻¹' s)) : ℝ≥0∞)
h₁ : Measurable (β := β × Ω) fun (x : α) ↦ (X x, Y x)
h₂ : MeasurableSet (α := β × Ω) (Prod.fst ⁻¹' s)
⊢ Eq (α := ℝ≥0∞) (((Measure.map X μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ) : Measure β) : (a : Set β) → ℝ≥0∞) s :
      ℝ≥0∞)

Tactic:
rw [Measure.map_apply hX hs, Measure.fst_apply hs, Measure.map_apply]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.fst_apply
-- 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 β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
s : Set β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β × Ω) (fun (x : α) ↦ (X x, Y x)) (Prod.fst ⁻¹' s)) : ℝ≥0∞)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl