awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Conditional
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
⊢ StronglyMeasurable (β := ℝ) ((X ⁻¹' s).indicator 1)

Tactic:
stronglyMeasurable_const.indicator (hX hs)

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.StronglyMeasurable.indicator
-- Module: Mathlib.Probability.Independence.Conditional
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
⊢ StronglyMeasurable (β := ℝ) ((X ⁻¹' s).indicator 1)

Tactic:
exact stronglyMeasurable_const.indicator (hX hs)

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.StronglyMeasurable.indicator
-- Module: Mathlib.Probability.Independence.Conditional
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
⊢ Integrable (ε := ℝ) ((X ⁻¹' s).indicator 1) μ

Tactic:
(integrable_indicator_iff ((hX.le hm') hs)).2 integrableOn_const

Premises used: Iff.mpr, Measurable.le, MeasureTheory.integrableOn_const, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.Probability.Independence.Conditional
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
⊢ Integrable (ε := ℝ) ((X ⁻¹' s).indicator 1) μ

Tactic:
exact (integrable_indicator_iff ((hX.le hm') hs)).2 integrableOn_const

Premises used: Iff.mpr, Measurable.le, MeasureTheory.integrableOn_const, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.Probability.Independence.Conditional
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']
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']
⊢ μ[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

Premises used: Set.indicator, Set.preimage, OfNat.ofNat
-- Module: Mathlib.Probability.Independence.Conditional
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
⊢ CondIndepFun m' hm' X Y μ

Tactic:
(condIndepFun_of_measurable_left hY hX).symm

Premises used: ProbabilityTheory.CondIndepFun.symm, ProbabilityTheory.condIndepFun_of_measurable_left
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Z : Ω → β'
hX : Measurable X
hZ : Measurable Z
⊢ Z ⟂ᵢ[Z, hZ; μ] X

Tactic:
condIndepFun_of_measurable_left (comap_measurable Z) hX

Premises used: ProbabilityTheory.condIndepFun_of_measurable_left, comap_measurable
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
X : Ω → β
Z : Ω → β'
hX : Measurable X
hZ : Measurable Z
⊢ X ⟂ᵢ[Z, hZ; μ] Z

Tactic:
condIndepFun_of_measurable_right hX (comap_measurable Z)

Premises used: ProbabilityTheory.condIndepFun_of_measurable_right, comap_measurable
-- Module: Mathlib.Probability.Independence.Conditional
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 (Ω × β × β')) (μ.trim hm' ⊗ₘ (condExpKernel μ m').map fun (ω : Ω) ↦ (f ω, g ω))
      (μ.trim hm' ⊗ₘ ((condExpKernel μ m').map f ×ₖ (condExpKernel μ m').map g))

Tactic:
Kernel.indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map hf hg

Premises used: ProbabilityTheory.Kernel.indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map, ProbabilityTheory.CondIndepFun
-- Module: Mathlib.Probability.Independence.Conditional
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 (β × β'))
rw₁ 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))
⊢ 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 (β × β'))

Tactic:
rw [condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map hf hg, ← Kernel.compProd_eq_iff]

Premises used: ProbabilityTheory.condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map, ProbabilityTheory.Kernel.compProd_eq_iff
-- Module: Mathlib.Probability.Independence.Conditional
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
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')
⊢ 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')

Tactic:
rw [condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map hf hg]

Premises used: ProbabilityTheory.condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map
-- Module: Mathlib.Probability.Independence.Conditional
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 ω)) μ)
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')
⊢ 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:
congr!
-- Module: Mathlib.Probability.Independence.Conditional
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
⊢ Measurable (β := β × β') fun (ω : Ω) ↦ (f ω, g ω)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Conditional
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
⊢ Measurable (α := Ω × Ω) (β := Ω × β × β') (Prod.map id fun (ω : Ω) ↦ (f ω, g ω))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Conditional
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 (Ω × β × β'))
    (Measure.map (Function.comp (β := Ω × Ω) (Prod.map id fun (ω : Ω) ↦ (f ω, g ω)) fun (a : Ω) ↦ (id a, id a)) μ)
    (Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ)
⊢ Eq (α := Measure (Ω × β × β')) (μ.trim hm' ⊗ₘ (condExpKernel μ m').map fun (ω : Ω) ↦ (f ω, g ω))
    (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)]

Premises used: le_rfl, measurable_id, MeasureTheory.Measure.compProd_map, Measurable.prodMk, ProbabilityTheory.compProd_trim_condExpKernel, Measurable.mono, MeasureTheory.Measure.map_map
-- Module: Mathlib.Probability.Independence.Conditional
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 (Ω × β × β'))
    (Measure.map (Function.comp (β := Ω × Ω) (Prod.map id fun (ω : Ω) ↦ (f ω, g ω)) fun (a : Ω) ↦ (id a, id a)) μ)
    (Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ)

Tactic:
rfl
-- Module: Mathlib.Probability.Independence.Conditional
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 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')
⊢ 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:
rw [Measure.compProd_eq_comp_prod]

Premises used: MeasureTheory.Measure.compProd_eq_comp_prod
-- Module: Mathlib.Probability.Independence.Conditional
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
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 ⋯) ↔
    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 (γ × β × β')))
⊢ 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 (γ × β × β')))

Tactic:
rw [condIndepFun_iff_map_prod_eq_prod_comp_trim hf hg]

Premises used: ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_comp_trim
-- Module: Mathlib.Probability.Independence.Conditional
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
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 ⋯ :
                    (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∞)
⊢ 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 (γ × β × β')))

Tactic:
simp_rw [Measure.ext_prod₃_iff]

Premises used: MeasureTheory.Measure.ext_prod₃_iff
-- Module: Mathlib.Probability.Independence.Conditional
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 γ} (hs : MeasurableSet s), MeasurableSet (k ⁻¹' s)

Tactic:
have hk_meas {s : Set γ} (hs : MeasurableSet s) : MeasurableSet[mγ.comap k] (k ⁻¹' s) :=
    ⟨s, hs, rfl⟩
-- Module: Mathlib.Probability.Independence.Conditional
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
⊢ Measurable (β := γ × β × β') fun (ω : Ω) ↦ (k ω, f ω, g ω)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Conditional
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∞)
rw₁ : Measurable (β := Ω × β × β') fun (ω : Ω) ↦ (ω, f ω, g ω)
⊢ 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:
rw [Measure.map_apply (by fun_prop) (hs.prod (ht.prod hu)),
      Measure.map_apply _ ((hk_meas hs).prod (ht.prod hu))]

Premises used: MeasureTheory.Measure.map_apply, MeasurableSet.prod
-- Module: Mathlib.Probability.Independence.Conditional
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∞) ((μ : (a : Set Ω) → ℝ≥0∞) ((fun (ω : Ω) ↦ (k ω, f ω, g ω)) ⁻¹' s ×ˢ t ×ˢ u) : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) ((fun (ω : Ω) ↦ (ω, f ω, g ω)) ⁻¹' (k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)

Tactic:
simp [Set.mk_preimage_prod]

Premises used: Set.mk_preimage_prod
-- Module: Mathlib.Probability.Independence.Conditional
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
⊢ Measurable (β := β × β') fun (ω : Ω) ↦ (f ω, g ω)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Conditional
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
⊢ Measurable (β := Ω × β × β') fun (ω : Ω) ↦ (ω, f ω, g ω)

Tactic:
exact (measurable_id.mono le_rfl hk.comap_le).prodMk (by fun_prop)

Premises used: le_rfl, measurable_id, Measurable.comap_le, Measurable.prodMk, Measurable.mono
-- Module: Mathlib.Probability.Independence.Conditional
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∞)

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)