awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
ω : Ω
pos : ∀ (h : ω ∈ X ⁻¹' s), norm (E := ℝ) (1 ω) ≤ 1
⊢ norm (E := ℝ) (if ω ∈ X ⁻¹' s then 1 ω else 0) ≤ 1
have neg : ∀ (h : ω ∉ X ⁻¹' s), norm (E := ℝ) 0 ≤ 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
⊢ HMul.hMul (α := (x : Ω) → ℝ) ((X ⁻¹' s).indicator 1) μ[(Y ⁻¹' t).indicator 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[(X ⁻¹' s).indicator 1 | m'] μ[(Y ⁻¹' t).indicator 1 | m']
have hf : StronglyMeasurable (β := ℝ) ((X ⁻¹' s).indicator 1)
Tactic: nth_rw 2 [condExp_of_stronglyMeasurable hm']
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
hf : StronglyMeasurable (β := ℝ) ((X ⁻¹' s).indicator 1)
⊢ HMul.hMul (α := (x : Ω) → ℝ) ((X ⁻¹' s).indicator 1) μ[(Y ⁻¹' t).indicator 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[(X ⁻¹' s).indicator 1 | m'] μ[(Y ⁻¹' t).indicator 1 | m']
have hfi : Integrable (ε := ℝ) ((X ⁻¹' s).indicator 1) μ
Tactic: nth_rw 2 [condExp_of_stronglyMeasurable hm']
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
⊢ μ[HMul.hMul (α := (x : Ω) → ℝ) ((X ⁻¹' s).indicator 1) ((Y ⁻¹' t).indicator 1) | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[(X ⁻¹' s).indicator 1 | m'] μ[(Y ⁻¹' t).indicator 1 | m']
have calc : μ[HMul.hMul (α := (x : Ω) → ℝ) ((X ⁻¹' s).indicator 1) ((Y ⁻¹' t).indicator 1) | m'] =ᶠ[ae μ]
  HMul.hMul (α := (x : Ω) → ℝ) ((X ⁻¹' s).indicator 1) μ[(Y ⁻¹' t).indicator 1 | m']
Tactic: calc μ[(X ⁻¹' s).indicator 1 * (Y ⁻¹' t).indicator 1 | m']
  _ =ᵐ[μ] (X ⁻¹' s).indicator 1 * μ[(Y ⁻¹' t).indicator 1 | m'] := by
    refine condExp_stronglyMeasurable_mul_of_bound hm' (stronglyMeasurable_const.indicator (hX hs))
      ((integrable_indicator_iff (hY ht)).2 integrableOn_const) 1 (ae_of_all μ fun ω ↦ ?_)
    rw [Set.indicator]
    split_ifs with h <;> simp
  _ =ᵐ[μ] μ[(X ⁻¹' s).indicator 1 | m'] * μ[(Y ⁻¹' t).indicator 1 | m'] := by
    nth_rw 2 [condExp_of_stronglyMeasurable hm']
    · exact stronglyMeasurable_const.indicator (hX hs)
    · exact (integrable_indicator_iff ((hX.le hm') hs)).2 integrableOn_const
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Y : Ω → β'
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
t : Set β'
ht : MeasurableSet t
calc :
  μ[HMul.hMul (α := (x : Ω) → ℝ) ((X ⁻¹' s).indicator 1) ((Y ⁻¹' t).indicator 1) | m'] =ᶠ[ae μ]
    HMul.hMul (α := (x : Ω) → ℝ) ((X ⁻¹' s).indicator 1) μ[(Y ⁻¹' t).indicator 1 | m']
⊢ μ[HMul.hMul (α := (x : Ω) → ℝ) ((X ⁻¹' s).indicator 1) ((Y ⁻¹' t).indicator 1) | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[(X ⁻¹' s).indicator 1 | m'] μ[(Y ⁻¹' t).indicator 1 | m']
have calc₁ : HMul.hMul (α := (x : Ω) → ℝ) ((X ⁻¹' s).indicator 1) μ[(Y ⁻¹' t).indicator 1 | m'] =ᶠ[ae μ]
  HMul.hMul (α := Ω → ℝ) μ[(X ⁻¹' s).indicator 1 | m'] μ[(Y ⁻¹' t).indicator 1 | m']
Tactic: calc μ[(X ⁻¹' s).indicator 1 * (Y ⁻¹' t).indicator 1 | m']
  _ =ᵐ[μ] (X ⁻¹' s).indicator 1 * μ[(Y ⁻¹' t).indicator 1 | m'] := by
    refine condExp_stronglyMeasurable_mul_of_bound hm' (stronglyMeasurable_const.indicator (hX hs))
      ((integrable_indicator_iff (hY ht)).2 integrableOn_const) 1 (ae_of_all μ fun ω ↦ ?_)
    rw [Set.indicator]
    split_ifs with h <;> simp
  _ =ᵐ[μ] μ[(X ⁻¹' s).indicator 1 | m'] * μ[(Y ⁻¹' t).indicator 1 | m'] := by
    nth_rw 2 [condExp_of_stronglyMeasurable hm']
    · exact stronglyMeasurable_const.indicator (hX hs)
    · exact (integrable_indicator_iff ((hX.le hm') hs)).2 integrableOn_const
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : CountableOrCountablyGenerated Ω (β × β')
hf : Measurable f
hg : Measurable g
⊢ CondIndepFun m' hm' f g μ ↔
    (ae (μ.trim hm')).EventuallyEq (β := Measure (β × β'))
      (⇑((condExpKernel μ m').map fun (ω : Ω) ↦ (f ω, g ω)) : (a : Ω) → Measure (β × β'))
      (⇑((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g) : (a : Ω) → Measure (β × β'))
have rw : Eq (α := Measure (Ω × β × β')) (μ.trim hm' ⊗ₘ (condExpKernel μ m').map fun (ω : Ω) ↦ (f ω, g ω))
    (μ.trim hm' ⊗ₘ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) ↔
  (ae (μ.trim hm')).EventuallyEq (β := Measure (β × β'))
    (⇑((condExpKernel μ m').map fun (ω : Ω) ↦ (f ω, g ω)) : (a : Ω) → Measure (β × β'))
    (⇑((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g) : (a : Ω) → Measure (β × β'))
Tactic: rw [condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map hf hg, ← Kernel.compProd_eq_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : CountableOrCountablyGenerated Ω (β × β')
hf : Measurable f
hg : Measurable g
rw :
  Eq (α := Measure (Ω × β × β')) (μ.trim hm' ⊗ₘ (condExpKernel μ m').map fun (ω : Ω) ↦ (f ω, g ω))
      (μ.trim hm' ⊗ₘ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) ↔
    (ae (μ.trim hm')).EventuallyEq (β := Measure (β × β'))
      (⇑((condExpKernel μ m').map fun (ω : Ω) ↦ (f ω, g ω)) : (a : Ω) → Measure (β × β'))
      (⇑((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g) : (a : Ω) → Measure (β × β'))
⊢ CondIndepFun m' hm' f g μ ↔
    (ae (μ.trim hm')).EventuallyEq (β := Measure (β × β'))
      (⇑((condExpKernel μ m').map fun (ω : Ω) ↦ (f ω, g ω)) : (a : Ω) → Measure (β × β'))
      (⇑((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g) : (a : Ω) → Measure (β × β'))
have rw₁ : Eq (α := Measure (Ω × β × β')) (μ.trim hm' ⊗ₘ (condExpKernel μ m').map fun (ω : Ω) ↦ (f ω, g ω))
    (μ.trim hm' ⊗ₘ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) ↔
  Eq (α := Measure (Ω × β × β')) (μ.trim hm' ⊗ₘ (condExpKernel μ m').map fun (ω : Ω) ↦ (f ω, g ω))
    (μ.trim hm' ⊗ₘ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g))
Tactic: rw [condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map hf hg, ← Kernel.compProd_eq_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ CondIndepFun m' hm' f g μ ↔
    Eq (α := Measure (Ω × β × β')) (Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ)
      ((⇑(Kernel.id ×ₖ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) : (a : Ω) → Measure (Ω × β × β')) ∘ₘ
        μ.trim hm')
have rw : Eq (α := Measure (Ω × β × β')) (μ.trim hm' ⊗ₘ (condExpKernel μ m').map fun (ω : Ω) ↦ (f ω, g ω))
    (μ.trim hm' ⊗ₘ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) ↔
  Eq (α := Measure (Ω × β × β')) (Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ)
    ((⇑(Kernel.id ×ₖ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) : (a : Ω) → Measure (Ω × β × β')) ∘ₘ
      μ.trim hm')
Tactic: rw [condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map hf hg]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ Eq (α := Measure (Ω × β × β')) (μ.trim hm' ⊗ₘ (condExpKernel μ m').map fun (ω : Ω) ↦ (f ω, g ω))
      (μ.trim hm' ⊗ₘ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) ↔
    Eq (α := Measure (Ω × β × β')) (Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ)
      ((⇑(Kernel.id ×ₖ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) : (a : Ω) → Measure (Ω × β × β')) ∘ₘ
        μ.trim hm')
have a : Eq (α := Measure (Ω × β × β')) (μ.trim hm' ⊗ₘ (condExpKernel μ m').map fun (ω : Ω) ↦ (f ω, g ω))
  (Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ)
Tactic: congr!
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
a :
  Eq (α := Measure (Ω × β × β')) (μ.trim hm' ⊗ₘ (condExpKernel μ m').map fun (ω : Ω) ↦ (f ω, g ω))
    (Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ)
⊢ Eq (α := Measure (Ω × β × β')) (μ.trim hm' ⊗ₘ (condExpKernel μ m').map fun (ω : Ω) ↦ (f ω, g ω))
      (μ.trim hm' ⊗ₘ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) ↔
    Eq (α := Measure (Ω × β × β')) (Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ)
      ((⇑(Kernel.id ×ₖ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) : (a : Ω) → Measure (Ω × β × β')) ∘ₘ
        μ.trim hm')
have a₁ : Eq (α := Measure (Ω × β × β')) (μ.trim hm' ⊗ₘ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g))
  ((⇑(Kernel.id ×ₖ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) : (a : Ω) → Measure (Ω × β × β')) ∘ₘ
    μ.trim hm')
Tactic: congr!
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ Eq (α := Measure (Ω × β × β')) (μ.trim hm' ⊗ₘ (condExpKernel μ m').map fun (ω : Ω) ↦ (f ω, g ω))
    (Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ)
have a : Eq (α := Measure (Ω × β × β'))
  (Measure.map (Function.comp (β := Ω × Ω) (Prod.map id fun (ω : Ω) ↦ (f ω, g ω)) fun (a : Ω) ↦ (id a, id a)) μ)
  (Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ)
Tactic: rw [Measure.compProd_map (by fun_prop), compProd_trim_condExpKernel,
      Measure.map_map (by fun_prop) ((measurable_id.mono le_rfl hm').prodMk measurable_id)]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ Eq (α := Measure (Ω × β × β')) (μ.trim hm' ⊗ₘ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g))
    ((⇑(Kernel.id ×ₖ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) : (a : Ω) → Measure (Ω × β × β')) ∘ₘ
      μ.trim hm')
have a : Eq (α := Measure (Ω × β × β'))
  ((⇑(Kernel.id ×ₖ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) : (a : Ω) → Measure (Ω × β × β')) ∘ₘ
    μ.trim hm')
  ((⇑(Kernel.id ×ₖ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g)) : (a : Ω) → Measure (Ω × β × β')) ∘ₘ
    μ.trim hm')
Tactic: rw [Measure.compProd_eq_comp_prod]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
⊢ f ⟂ᵢ[k, hk; μ] g ↔
    Eq (α := Measure (γ × β × β')) (Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')))
have rw : Eq (α := Measure (Ω × β × β')) (Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ)
    ((⇑(Kernel.id ×ₖ
            (Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) f ×ₖ
              Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) g)) :
        (a : Ω) → Measure (Ω × β × β')) ∘ₘ
      μ.trim sorry) ↔
  Eq (α := Measure (γ × β × β')) (Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ)
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')))
Tactic: rw [condIndepFun_iff_map_prod_eq_prod_comp_trim hf hg]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
⊢ Eq (α := Measure (Ω × β × β')) (Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ)
      ((⇑(Kernel.id ×ₖ
              (Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) f ×ₖ
                Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) g)) :
          (a : Ω) → Measure (Ω × β × β')) ∘ₘ
        μ.trim ⋯) ↔
    Eq (α := Measure (γ × β × β')) (Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ)
      (Measure.bind (mα := mγ) (Measure.map k μ)
        (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')))
have simp_rw : (∀ {s : Set Ω} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞)
            ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            (((⇑(Kernel.id ×ₖ
                          (Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) f ×ₖ
                            Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) g)) :
                      (a : Ω) → Measure (Ω × β × β')) ∘ₘ
                    μ.trim sorry :
                  (a : Set (Ω × β × β')) → ℝ≥0∞)
                (s ×ˢ t ×ˢ u) :
              ℝ≥0∞)) ↔
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞)
            ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            ((Measure.bind (mα := mγ) (Measure.map k μ)
                    (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')) :
                  (a : Set (γ × β × β')) → ℝ≥0∞)
                (s ×ˢ t ×ˢ u) :
              ℝ≥0∞)
Tactic: simp_rw [Measure.ext_prod₃_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
⊢ (∀ {s : Set Ω} {t : Set β} {u : Set β'},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            Eq (α := ℝ≥0∞)
              ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
              (((⇑(Kernel.id ×ₖ
                            (Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) f ×ₖ
                              Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) g)) :
                        (a : Ω) → Measure (Ω × β × β')) ∘ₘ
                      μ.trim ⋯ :
                    (a : Set (Ω × β × β')) → ℝ≥0∞)
                  (s ×ˢ t ×ˢ u) :
                ℝ≥0∞)) ↔
    ∀ {s : Set γ} {t : Set β} {u : Set β'},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            Eq (α := ℝ≥0∞)
              ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
              ((Measure.bind (mα := mγ) (Measure.map k μ)
                      (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')) :
                    (a : Set (γ × β × β')) → ℝ≥0∞)
                  (s ×ˢ t ×ˢ u) :
                ℝ≥0∞)
have hk_meas : ∀ {s : Set γ} (hs : MeasurableSet s), MeasurableSet (k ⁻¹' s)
Tactic: have hk_meas {s : Set γ} (hs : MeasurableSet s) : MeasurableSet[mγ.comap k] (k ⁻¹' s) :=
    ⟨s, hs, rfl⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ} (hs : MeasurableSet s), MeasurableSet (k ⁻¹' s)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
    ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) ((k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) ((fun (ω : Ω) ↦ (k ω, f ω, g ω)) ⁻¹' s ×ˢ t ×ˢ u) : ℝ≥0∞)
  ((μ : (a : Set Ω) → ℝ≥0∞) ((fun (ω : Ω) ↦ (ω, f ω, g ω)) ⁻¹' (k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)
Tactic: rw [Measure.map_apply (by fun_prop) (hs.prod (ht.prod hu)),
      Measure.map_apply _ ((hk_meas hs).prod (ht.prod hu))]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ} (hs : MeasurableSet s), MeasurableSet (k ⁻¹' s)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) ((fun (ω : Ω) ↦ (k ω, f ω, g ω)) ⁻¹' s ×ˢ t ×ˢ u) : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) ((fun (ω : Ω) ↦ (ω, f ω, g ω)) ⁻¹' (k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
    ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) ((k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)
have rw₁ : Measurable (β := Ω × β × β') fun (ω : Ω) ↦ (ω, f ω, g ω)
Tactic: rw [Measure.map_apply (by fun_prop) (hs.prod (ht.prod hu)),
      Measure.map_apply _ ((hk_meas hs).prod (ht.prod hu))]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ} (hs : MeasurableSet s), MeasurableSet (k ⁻¹' s)
⊢ (∀ {s : Set Ω} {t : Set β} {u : Set β'},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            Eq (α := ℝ≥0∞)
              ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
              (((⇑(Kernel.id ×ₖ
                            (Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) f ×ₖ
                              Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) g)) :
                        (a : Ω) → Measure (Ω × β × β')) ∘ₘ
                      μ.trim ⋯ :
                    (a : Set (Ω × β × β')) → ℝ≥0∞)
                  (s ×ˢ t ×ˢ u) :
                ℝ≥0∞)) ↔
    ∀ {s : Set γ} {t : Set β} {u : Set β'},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            Eq (α := ℝ≥0∞)
              ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
              ((Measure.bind (mα := mγ) (Measure.map k μ)
                      (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')) :
                    (a : Set (γ × β × β')) → ℝ≥0∞)
                  (s ×ˢ t ×ˢ u) :
                ℝ≥0∞)
have h_left : ∀ {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) (hu : MeasurableSet u),
  Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
    ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) ((k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)
Tactic: have h_left {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t)
      (hu : MeasurableSet u) :
      (μ.map (fun ω ↦ (k ω, f ω, g ω))) (s ×ˢ t ×ˢ u) =
        (@Measure.map _ _ _ ((mγ.comap k).prod inferInstance)
          (fun ω ↦ (ω, f ω, g ω)) μ) ((k ⁻¹' s) ×ˢ t ×ˢ u) := by
    rw [Measure.map_apply (by fun_prop) (hs.prod (ht.prod hu)),
      Measure.map_apply _ ((hk_meas hs).prod (ht.prod hu))]
    · simp [Set.mk_preimage_prod]
    · exact (measurable_id.mono le_rfl hk.comap_le).prodMk (by fun_prop)