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
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)) μ)
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)) μ)
⊢ (∀ᵐ (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 μ) ↔
  (∀ᵐ (a : β) ∂Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ),
      @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.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ))
Tactic: rw [condDistrib, ← hf.ae_integrable_condKernel_iff, 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
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 (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) x) fun (y : Ω) ↦ f (x, y)
have 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)
Tactic: rw [condDistrib]
-- 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
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 (((condDistrib Y X μ : Kernel β Ω) : (a : β) → Measure Ω) x) fun (y : Ω) ↦ f (x, y))
    (Measure.map X μ)
have 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)) μ))
Tactic: rw [← Measure.fst_map_prodMk₀ hY, 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 β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
⊢ Eq (α := Measure β) (Measure.map X μ) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
have 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∞)
Tactic: ext s hs
-- 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 : 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∞) (((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∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' s) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β × Ω) (fun (x : α) ↦ (X x, Y x)) (Prod.fst ⁻¹' s)) : ℝ≥0∞)
Tactic: rw [Measure.map_apply hX hs, Measure.fst_apply hs, Measure.map_apply]
-- 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 : 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∞)
⊢ 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∞)
have h₁ : Measurable (β := β × Ω) fun (x : α) ↦ (X x, Y x)
Tactic: rw [Measure.map_apply hX hs, Measure.fst_apply hs, Measure.map_apply]
-- 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 : 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)
⊢ 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∞)
have h₂ : MeasurableSet (α := β × Ω) (Prod.fst ⁻¹' s)
Tactic: rw [Measure.map_apply hX hs, Measure.fst_apply hs, Measure.map_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (hypothesis)
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 μ ⊗ₘ κ
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
have heq : Eq (α := Measure β) (Measure.map X μ) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
Tactic: have heq : μ.map X = (μ.map (fun x ↦ (X x, Y x))).fst := by
    ext s hs
    rw [Measure.map_apply hX hs, Measure.fst_apply hs, Measure.map_apply]
    exacts [rfl, Measurable.prod hX hY, measurable_fst hs]
-- 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 : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Eq (α := Measure β) (Measure.map X μ) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
have rw : EventuallyEq.{u_2, u_3} (β := Measure Ω)
  (ae (F := Measure β) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ)))
  (⇑(Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
Tactic: rw [heq, 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 β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Eq (α := Measure β) (Measure.map X μ) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω)
    (ae (F := Measure β) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ)))
    (⇑(Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
have symm : EventuallyEq.{u_2, u_3} (β := Measure Ω)
  (ae (F := Measure β) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ)))
  (⇑κ : (a : β) → Measure Ω) (⇑(Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) : (a : β) → Measure Ω)
Tactic: symm
-- 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 : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Eq (α := Measure β) (Measure.map X μ) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω)
    (ae (F := Measure β) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ)))
    (⇑κ : (a : β) → Measure Ω) (⇑(Measure.condKernel (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) : (a : β) → Measure Ω)
have refine : Measure.map (fun (a : α) ↦ (X a, Y a)) μ =
  Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) ⊗ₘ κ
Tactic: refine eq_condKernel_of_measure_eq_compProd _ ?_
-- 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 : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Eq (α := Measure β) (Measure.map X μ) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (x : α) ↦ (X x, Y x)) μ))
⊢ Measure.map (fun (a : α) ↦ (X a, Y a)) μ =
    Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ) ⊗ₘ κ
have h : Eq (α := Measure β) (Measure.fst.{u_2, u_3} (β := Ω) (Measure.map (fun (a : α) ↦ (X a, Y a)) μ)) (Measure.map X μ)
Tactic: convert! hκ
-- 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 μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
have pos : ∀ (hX : AEMeasurable X μ),
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
Tactic: by_cases hX : AEMeasurable X μ
-- 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 μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
pos :
  ∀ (hX : AEMeasurable X μ),
    EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
      (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
have neg : ∀ (hX : ¬AEMeasurable X μ),
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
Tactic: by_cases hX : AEMeasurable X μ
-- 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 μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
this :
  EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (AEMeasurable.mk X hX) μ))
    (⇑(condDistrib (AEMeasurable.mk Y hY) (AEMeasurable.mk X hX) μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
have rwa : EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (AEMeasurable.mk X hX) μ))
  (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
Tactic: rwa [Measure.map_congr hX.ae_eq_mk, condDistrib_congr hY.ae_eq_mk hX.ae_eq_mk]
-- 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 μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map X μ))
    (⇑(condDistrib Y X μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
have pos : EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (AEMeasurable.mk X hX) μ))
  (⇑(condDistrib (AEMeasurable.mk Y hY) (AEMeasurable.mk X hX) μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
Tactic: suffices condDistrib (hY.mk Y) (hX.mk X) μ =ᵐ[μ.map (hX.mk X)] κ by
    rwa [Measure.map_congr hX.ae_eq_mk, condDistrib_congr hY.ae_eq_mk hX.ae_eq_mk]
-- 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 μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (AEMeasurable.mk X hX) μ))
    (⇑(condDistrib (AEMeasurable.mk Y hY) (AEMeasurable.mk X hX) μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
have pos : Eq (α := Measure (β × Ω)) (Measure.map (fun (x : α) ↦ (AEMeasurable.mk X hX x, AEMeasurable.mk Y hY x)) μ)
  (Measure.map (fun (x : α) ↦ (X x, Y x)) μ)
Tactic: refine condDistrib_ae_eq_of_measure_eq_compProd_of_measurable (μ := μ)
    hX.measurable_mk hY.measurable_mk ((Eq.trans ?_ hκ).trans ?_)
-- 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 μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
pos :
  Eq (α := Measure (β × Ω)) (Measure.map (fun (x : α) ↦ (AEMeasurable.mk X hX x, AEMeasurable.mk Y hY x)) μ)
    (Measure.map (fun (x : α) ↦ (X x, Y x)) μ)
⊢ EventuallyEq.{u_2, u_3} (β := Measure Ω) (ae (F := Measure β) (Measure.map (AEMeasurable.mk X hX) μ))
    (⇑(condDistrib (AEMeasurable.mk Y hY) (AEMeasurable.mk X hX) μ) : (a : β) → Measure Ω) (⇑κ : (a : β) → Measure Ω)
have pos₁ : Measure.map X μ ⊗ₘ κ = Measure.map (AEMeasurable.mk X hX) μ ⊗ₘ κ
Tactic: refine condDistrib_ae_eq_of_measure_eq_compProd_of_measurable (μ := μ)
    hX.measurable_mk hY.measurable_mk ((Eq.trans ?_ hκ).trans ?_)
-- 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 μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
⊢ Eq (α := Measure (β × Ω)) (Measure.map (fun (x : α) ↦ (AEMeasurable.mk X hX x, AEMeasurable.mk Y hY x)) μ)
    (Measure.map (fun (x : α) ↦ (X x, Y x)) μ)
have pos : (ae μ).EventuallyEq (β := β × Ω) (fun (x : α) ↦ (AEMeasurable.mk X hX x, AEMeasurable.mk Y hY x)) fun (x : α) ↦
  (X x, Y x)
Tactic: refine 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 μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
a : α
haX : X a = AEMeasurable.mk X hX a
haY : Y a = AEMeasurable.mk Y hY a
⊢ (AEMeasurable.mk X hX a, AEMeasurable.mk Y hY a) = (X a, Y a)
have rw : (AEMeasurable.mk X hX a, AEMeasurable.mk Y hY a) = (AEMeasurable.mk X hX a, Y a)
Tactic: rw [haX, haY]
-- 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 μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
a : α
haX : X a = AEMeasurable.mk X hX a
haY : Y a = AEMeasurable.mk Y hY a
rw : (AEMeasurable.mk X hX a, AEMeasurable.mk Y hY a) = (AEMeasurable.mk X hX a, Y a)
⊢ (AEMeasurable.mk X hX a, AEMeasurable.mk Y hY a) = (X a, Y a)
have rw₁ : (AEMeasurable.mk X hX a, AEMeasurable.mk Y hY a) = (AEMeasurable.mk X hX a, AEMeasurable.mk Y hY a)
Tactic: rw [haX, haY]
-- 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 μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
⊢ (ae μ).EventuallyEq (β := β × Ω) (fun (x : α) ↦ (AEMeasurable.mk X hX x, AEMeasurable.mk Y hY x)) fun (x : α) ↦
    (X x, Y x)
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ X x = AEMeasurable.mk X hX x) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Y x = AEMeasurable.mk Y hY x) x} x →
              Membership.mem (γ := Set α)
                {x : α |
                  (fun (x : α) ↦
                      Eq (α := β × Ω) ((fun (x : α) ↦ (AEMeasurable.mk X hX x, AEMeasurable.mk Y hY x)) x)
                        ((fun (x : α) ↦ (X x, Y x)) x))
                    x}
                x}
          x}
    a
Tactic: filter_upwards [hX.ae_eq_mk, hY.ae_eq_mk] with a haX haY using by rw [haX, haY]
-- 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 μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst_4 : IsFiniteKernel κ
hκ : Measure.map (fun (x : α) ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ X x = AEMeasurable.mk X hX x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Y x = AEMeasurable.mk Y hY x) x} x →
                Membership.mem (γ := Set α)
                  {x : α |
                    (fun (x : α) ↦
                        Eq (α := β × Ω) ((fun (x : α) ↦ (AEMeasurable.mk X hX x, AEMeasurable.mk Y hY x)) x)
                          ((fun (x : α) ↦ (X x, Y x)) x))
                      x}
                  x}
            x}
      a
⊢ (ae μ).EventuallyEq (β := β × Ω) (fun (x : α) ↦ (AEMeasurable.mk X hX x, AEMeasurable.mk Y hY x)) fun (x : α) ↦
    (X x, Y x)
have h₁ : ∀ (a : α),
  X a = AEMeasurable.mk X hX a →
    Y a = AEMeasurable.mk Y hY a → (AEMeasurable.mk X hX a, AEMeasurable.mk Y hY a) = (X a, Y a)
Tactic: filter_upwards [hX.ae_eq_mk, hY.ae_eq_mk] with a haX haY using by rw [haX, haY]