awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
⊢ (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
have h2 : (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)] 0
Tactic: have h2 : (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η] 0 := by
    refine Measure.rnDeriv_eq_zero_of_mutuallySingular ?_ ?_
    · exact Measure.MutuallySingular.compProd_of_left (μ.mutuallySingular_singularPart _) _ _
    · exact Measure.AbsolutelyContinuous.rfl
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
κ η : Kernel α β
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsFiniteKernel κ
inst_3 : IsFiniteKernel η
h :
  (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
h2 : (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)] 0
⊢ (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)]
    (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)
have h₁ : ∀ (x : α × β)
  (hx :
    (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x =
      ((μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) + (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η)) x)
  (hx2 : (μ.singularPart ν ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x = 0 x),
  (ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x =
    (μ.singularPart ν ⊗ₘ κ + ν.withDensity (μ.rnDeriv ν) ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) x
Tactic: filter_upwards [h, h2] with x hx hx2
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
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 ν
⊢ (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)] fun (p : α × β) ↦ μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p
have refine : (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) * (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)] fun (p : α × β) ↦
  μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p
Tactic: refine Filter.EventuallyEq.trans (Measure.rnDeriv_mul_rnDeriv h_ac).symm ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
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 ν
⊢ (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) * (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η) =ᶠ[ae (ν ⊗ₘ η)] fun (p : α × β) ↦
    μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p
have h : ∀ (p : α × β) (hp : (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η) p = μ.rnDeriv ν p.1),
  ((μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) * (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η)) p = μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p
Tactic: filter_upwards [rnDeriv_measure_compProd_left μ ν η] with p hp
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
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
⊢ ((μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) * (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η)) p = μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p
have h : (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p * (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η) p = μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p
Tactic: rw [Pi.mul_apply, hp, mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
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
⊢ ((μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) * (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η)) p = μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p
have h₁ : (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p * μ.rnDeriv ν p.1 = μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p
Tactic: rw [Pi.mul_apply, hp, mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Composition.RadonNikodym (goal)
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
⊢ ((μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) * (μ ⊗ₘ η).rnDeriv (ν ⊗ₘ η)) p = μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p
have h₂ : μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p = μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p
Tactic: rw [Pi.mul_apply, hp, mul_comm]
-- 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 : α → Ω
inst_5 : MeasurableSpace β
⊢ IsMarkovKernel (mα := inst_5) (mβ := inst) (condDistrib Y X μ)
have rw : IsMarkovKernel.{u_2, u_3} (α := β) (β := Ω) (mα := inst_5) (mβ := inst)
  (Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ))
Tactic: rw [condDistrib]
-- 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 β
inst_4 : MeasurableSingletonClass β
hY : Measurable Y
x : β
hX : Ne (α := ℝ≥0∞) (((Measure.map X μ : Measure β) : (a : Set β) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
⊢ ((((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∞)
have 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∞)
Tactic: rw [condDistrib, Measure.condKernel_apply_of_ne_zero _ s]
-- 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 β
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∞)
⊢ ((((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∞)
have 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∞)
Tactic: rw [condDistrib, Measure.condKernel_apply_of_ne_zero _ s]
-- 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 β
inst_4 : MeasurableSingletonClass β
hY : Measurable Y
x : β
hX : Ne (α := ℝ≥0∞) (((Measure.map X μ : Measure β) : (a : Set β) → ℝ≥0∞) {x} : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set Ω
⊢ 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∞)
have 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∞)
Tactic: rw [Measure.fst_map_prodMk hY]
-- 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 β
hY : AEMeasurable Y μ
⊢ Eq (α := Measure (β × Ω)) (Measure.map X μ ⊗ₘ condDistrib Y X μ) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
have rw : Eq (α := Measure (β × Ω)) (Measure.map X μ ⊗ₘ Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ))
  (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
Tactic: rw [condDistrib, ← Measure.fst_map_prodMk₀ hY, Measure.disintegrate]
-- 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 β
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)) μ)
⊢ Eq (α := Measure (β × Ω)) (Measure.map X μ ⊗ₘ condDistrib Y X μ) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
have 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)) μ)
Tactic: rw [condDistrib, ← Measure.fst_map_prodMk₀ hY, Measure.disintegrate]
-- 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 β
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)) μ)
⊢ Eq (α := Measure (β × Ω)) (Measure.map X μ ⊗ₘ condDistrib Y X μ) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
have rw₂ : Eq (α := Measure (β × Ω)) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
Tactic: rw [condDistrib, ← Measure.fst_map_prodMk₀ hY, Measure.disintegrate]
-- 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 β
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
⊢ Eq (α := Measure Ω) (Measure.bind (mα := mβ) (Measure.map X μ) (⇑(condDistrib Y X μ) : (a : β) → Measure Ω))
    (Measure.map Y μ)
have rw : Eq (α := Measure Ω) (Measure.snd (Measure.map X μ ⊗ₘ condDistrib Y X μ)) (Measure.map Y μ)
Tactic: rw [← Measure.snd_compProd, compProd_map_condDistrib hY, Measure.snd_map_prodMk₀ hX]
-- 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 β
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
rw : Eq (α := Measure Ω) (Measure.snd (Measure.map X μ ⊗ₘ condDistrib Y X μ)) (Measure.map Y μ)
⊢ Eq (α := Measure Ω) (Measure.bind (mα := mβ) (Measure.map X μ) (⇑(condDistrib Y X μ) : (a : β) → Measure Ω))
    (Measure.map Y μ)
have rw₁ : Eq (α := Measure Ω) (Measure.snd.{u_2, u_3} (α := β) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) (Measure.map Y μ)
Tactic: rw [← Measure.snd_compProd, compProd_map_condDistrib hY, Measure.snd_map_prodMk₀ hX]
-- 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 β
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 μ)
⊢ Eq (α := Measure Ω) (Measure.bind (mα := mβ) (Measure.map X μ) (⇑(condDistrib Y X μ) : (a : β) → Measure Ω))
    (Measure.map Y μ)
have rw₂ : Eq (α := Measure Ω) (Measure.map Y μ) (Measure.map Y μ)
Tactic: rw [← Measure.snd_compProd, compProd_map_condDistrib hY, Measure.snd_map_prodMk₀ hX]
-- 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 β
X' : α → β
Y' : α → Ω
hY : Y =ᶠ[ae μ] Y'
hX : X =ᶠ[ae μ] X'
⊢ Eq (α := Kernel β Ω) (condDistrib Y X μ) (condDistrib Y' X' μ)
have rw : Eq (α := Kernel β Ω) (Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ))
  (Measure.condKernel (Measure.map (fun (a : α) ↦ (X' a, Y' a)) μ))
Tactic: rw [condDistrib, condDistrib]
-- 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 β
X' : α → β
Y' : α → Ω
hY : Y =ᶠ[ae μ] Y'
hX : X =ᶠ[ae μ] X'
⊢ Eq (α := Kernel β Ω) (Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ))
    (Measure.condKernel (Measure.map (fun (a : α) ↦ (X' a, Y' a)) μ))
have e_ρ : Eq (α := Measure (β × Ω)) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) (Measure.map (fun (a : α) ↦ (X' a, Y' a)) μ)
Tactic: congr 1
-- 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 β
X' : α → β
Y' : α → Ω
hY : Y =ᶠ[ae μ] Y'
hX : X =ᶠ[ae μ] X'
⊢ Eq (α := Measure (β × Ω)) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) (Measure.map (fun (a : α) ↦ (X' a, Y' a)) μ)
have e_ρ : (ae μ).EventuallyEq (β := β × Ω) (fun (a : α) ↦ (X a, Y a)) fun (a : α) ↦ (X' a, Y' a)
Tactic: rw [Measure.map_congr]
-- 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 β
X' : α → β
Y' : α → Ω
hY : Y =ᶠ[ae μ] Y'
hX : X =ᶠ[ae μ] X'
a : α
ha : X a = X' a
hb : Y a = Y' a
⊢ (X a, Y a) = (X' a, Y' a)
have rw : (X' a, Y a) = (X' a, Y' a)
Tactic: rw [ha, hb]
-- 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 β
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)
⊢ (X a, Y a) = (X' a, Y' a)
have rw₁ : (X' a, Y' a) = (X' a, Y' a)
Tactic: rw [ha, hb]
-- 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 β
X' : α → β
Y' : α → Ω
hY : Y =ᶠ[ae μ] Y'
hX : X =ᶠ[ae μ] X'
⊢ (ae μ).EventuallyEq (β := β × Ω) (fun (a : α) ↦ (X a, Y a)) fun (a : α) ↦ (X' a, Y' a)
have 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
Tactic: filter_upwards [hX, hY] with a ha hb using by rw [ha, hb]
-- 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 β
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
⊢ (ae μ).EventuallyEq (β := β × Ω) (fun (a : α) ↦ (X a, Y a)) fun (a : α) ↦ (X' a, Y' a)
have h₁ : ∀ (a : α), X a = X' a → Y a = Y' a → (X a, Y a) = (X' a, Y' a)
Tactic: filter_upwards [hX, hY] with a ha hb using by rw [ha, hb]
-- 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
hY : AEMeasurable Y μ
hf : AEStronglyMeasurable (m₀ := Prod.instMeasurableSpace) f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
⊢ (∀ᵐ (a : β) ∂Measure.map X μ,
        @Integrable.{u_4, u_3} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω))
          (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) a)) ∧
      @Integrable ℝ _ _ _ mβ
        (fun (a : β) ↦
          @integral _ _ _ _ inst (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖)
        (Measure.map X μ) ↔
    @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
have rw : (∀ᵐ (a : β) ∂Measure.map X μ,
      @Integrable.{u_4, u_3} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω))
        ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) a)) ∧
    @Integrable ℝ _ _ _ mβ
      (fun (a : β) ↦
        @integral _ _ _ _ inst ((Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) : (a : β) → Measure Ω) a)
          fun (ω : Ω) ↦ ‖f (a, ω)‖)
      (Measure.map X μ) ↔
  @Integrable _ _ _ _ Prod.instMeasurableSpace f (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)
Tactic: rw [condDistrib, ← hf.ae_integrable_condKernel_iff, Measure.fst_map_prodMk₀ hY]