awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hs1_eq :
  ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs2_eq :
  ∀ s ∈ s2,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1,
    ∀ t ∈ s2,
      (ae μ).EventuallyEq (β := ℝ)
        (fun (ω : Ω) ↦
          ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)))
        μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m']
s t : Set Ω
hs : s ∈ s1
ht : t ∈ s2
h :
  μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
refine_2 :
  (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (ω : Ω) ↦ (((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t))
    fun (a : Ω) ↦
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∀ᵐ (a : Ω) ∂μ.trim hm',
    (((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
refine ((stronglyMeasurable_condExpKernel ((hs1 s hs).inter (hs2 t ht))).ae_eq_trim_iff hm'
      ((measurable_condExpKernel (hs1 s hs)).mul
        (measurable_condExpKernel (hs2 t ht))).stronglyMeasurable).mpr ?_

Premises used: Iff.mpr, Measurable.mul, Measurable.stronglyMeasurable, ProbabilityTheory.stronglyMeasurable_condExpKernel, ProbabilityTheory.measurable_condExpKernel, MeasureTheory.StronglyMeasurable.ae_eq_trim_iff, MeasurableSet.inter
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hs1_eq :
  ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs2_eq :
  ∀ s ∈ s2,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1,
    ∀ t ∈ s2,
      (ae μ).EventuallyEq (β := ℝ)
        (fun (ω : Ω) ↦
          ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)))
        μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m']
s t : Set Ω
hs : s ∈ s1
ht : t ∈ s2
h :
  μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
h₁ :
  ∀ (ω : Ω)
    (hs_eq :
      ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) =
        μ[s.indicator fun (ω : Ω) ↦ 1 | m'] ω)
    (ht_eq :
      ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t) =
        μ[t.indicator fun (ω : Ω) ↦ 1 | m'] ω)
    (hst_eq :
      ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)) =
        μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] ω)
    (h :
      μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] ω =
        HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m'] ω),
    (((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (ω : Ω) ↦ (((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t))
    fun (a : Ω) ↦
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((condExpKernel μ m' : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
filter_upwards [hs1_eq s hs, hs2_eq t ht, hs12_eq s hs t ht, h] with ω hs_eq ht_eq hst_eq h
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hs1_eq :
  ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs2_eq :
  ∀ s ∈ s2,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1,
    ∀ t ∈ s2,
      (ae μ).EventuallyEq (β := ℝ)
        (fun (ω : Ω) ↦
          ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)))
        μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m']
s t : Set Ω
hs : s ∈ s1
ht : t ∈ s2
h_1 :
  μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
ω : Ω
hs_eq :
  ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) =
    μ[s.indicator fun (ω : Ω) ↦ 1 | m'] ω
ht_eq :
  ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t) =
    μ[t.indicator fun (ω : Ω) ↦ 1 | m'] ω
hst_eq :
  ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)) =
    μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] ω
h :
  μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] ω =
    HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m'] ω
⊢ Ne (α := ℝ≥0∞) ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
have h_ne_top : condExpKernel μ m' ω (s ∩ t) ≠ ∞ := measure_ne_top (condExpKernel μ m' ω) _
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hs1_eq :
  ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs2_eq :
  ∀ s ∈ s2,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1,
    ∀ t ∈ s2,
      (ae μ).EventuallyEq (β := ℝ)
        (fun (ω : Ω) ↦
          ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)))
        μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m']
s t : Set Ω
hs : s ∈ s1
ht : t ∈ s2
h_1 :
  μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
ω : Ω
hs_eq :
  ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) =
    μ[s.indicator fun (ω : Ω) ↦ 1 | m'] ω
ht_eq :
  ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t) =
    μ[t.indicator fun (ω : Ω) ↦ 1 | m'] ω
hst_eq :
  ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)) =
    μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] ω
h :
  μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] ω =
    HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m'] ω
h_ne_top :
  Ne (α := ℝ≥0∞) ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
h₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) ≠
    ∞
⊢ (((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [← ENNReal.ofReal_toReal h_ne_top, hst_eq, h, Pi.mul_apply, ← hs_eq, ← ht_eq,
      ← ENNReal.toReal_mul, ENNReal.ofReal_toReal]

Premises used: Pi.mul_apply, ENNReal.ofReal_toReal, ENNReal.toReal_mul
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hs1_eq :
  ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs2_eq :
  ∀ s ∈ s2,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1,
    ∀ t ∈ s2,
      (ae μ).EventuallyEq (β := ℝ)
        (fun (ω : Ω) ↦
          ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)))
        μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m']
s t : Set Ω
hs : s ∈ s1
ht : t ∈ s2
h_1 :
  μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
ω : Ω
hs_eq :
  ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) =
    μ[s.indicator fun (ω : Ω) ↦ 1 | m'] ω
ht_eq :
  ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t) =
    μ[t.indicator fun (ω : Ω) ↦ 1 | m'] ω
hst_eq :
  ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)) =
    μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] ω
h :
  μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] ω =
    HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m'] ω
h_ne_top :
  Ne (α := ℝ≥0∞) ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) ≠
    ∞

Tactic:
ENNReal.mul_ne_top (measure_ne_top (condExpKernel μ m' ω) s)
      (measure_ne_top (condExpKernel μ m' ω) t)

Premises used: MeasureTheory.measure_ne_top, ENNReal.mul_ne_top, ProbabilityTheory.condExpKernel, DFunLike.coe
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hs1_eq :
  ∀ s ∈ s1,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs2_eq :
  ∀ s ∈ s2,
    (ae μ).EventuallyEq (β := ℝ)
      (fun (ω : Ω) ↦
        ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
      μ[s.indicator fun (ω : Ω) ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1,
    ∀ t ∈ s2,
      (ae μ).EventuallyEq (β := ℝ)
        (fun (ω : Ω) ↦
          ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)))
        μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m']
s t : Set Ω
hs : s ∈ s1
ht : t ∈ s2
h_1 :
  μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
ω : Ω
hs_eq :
  ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s) =
    μ[s.indicator fun (ω : Ω) ↦ 1 | m'] ω
ht_eq :
  ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t) =
    μ[t.indicator fun (ω : Ω) ↦ 1 | m'] ω
hst_eq :
  ENNReal.toReal ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t)) =
    μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] ω
h :
  μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] ω =
    HMul.hMul (α := Ω → ℝ) (β := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m'] ω
h_ne_top :
  Ne (α := ℝ≥0∞) ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      ((((condExpKernel μ m' : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) ≠
    ∞

Tactic:
exact ENNReal.mul_ne_top (measure_ne_top (condExpKernel μ m' ω) s)
      (measure_ne_top (condExpKernel μ m' ω) t)

Premises used: MeasureTheory.measure_ne_top, ENNReal.mul_ne_top, ProbabilityTheory.condExpKernel, DFunLike.coe
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
rw :
  (∀ (s_1 : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s_1, Membership.mem (γ := Set (Set Ω)) {s i} (f i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s_1, f i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ s_1, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'])) ↔
    ∀ (S : Finset ι),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, s i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ S, μ[(s i).indicator fun (ω : Ω) ↦ 1 | m'])
hπ₁ : ∀ (i : ι) (s_1 : Set Ω) (_hs : Membership.mem (γ := Set (Set Ω)) {s i} s_1), MeasurableSet s_1
⊢ iCondIndepSets m' hm' (fun (i : ι) ↦ {s i}) μ ↔
    ∀ (S : Finset ι),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, s i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ S, μ[(s i).indicator fun (ω : Ω) ↦ 1 | m'])

Tactic:
rw [iCondIndepSets_iff]

Premises used: ProbabilityTheory.iCondIndepSets_iff
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
simp_all :
  (∀ (s_1 : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s_1, f i = s i),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s_1, s i) fun (ω : Ω) ↦ 1 | m']
        (∏ x ∈ s_1, μ[(s x).indicator fun (ω : Ω) ↦ 1 | m'])) ↔
    ∀ (S : Finset ι),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, s i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ S, μ[(s i).indicator fun (ω : Ω) ↦ 1 | m'])
⊢ (∀ (s_1 : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s_1, Membership.mem (γ := Set (Set Ω)) {s i} (f i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s_1, f i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ s_1, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'])) ↔
    ∀ (S : Finset ι),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, s i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ S, μ[(s i).indicator fun (ω : Ω) ↦ 1 | m'])

Tactic:
simp_all only [Set.mem_singleton_iff]

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
mp :
  (∀ (s_1 : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s_1, f i = s i),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s_1, s i) fun (ω : Ω) ↦ 1 | m']
        (∏ x ∈ s_1, μ[(s x).indicator fun (ω : Ω) ↦ 1 | m'])) →
    ∀ (S : Finset ι),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, s i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ S, μ[(s i).indicator fun (ω : Ω) ↦ 1 | m'])
mpr :
  (∀ (S : Finset ι),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, s i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ S, μ[(s i).indicator fun (ω : Ω) ↦ 1 | m'])) →
    ∀ (s_1 : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s_1, f i = s i),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s_1, s i) fun (ω : Ω) ↦ 1 | m']
        (∏ x ∈ s_1, μ[(s x).indicator fun (ω : Ω) ↦ 1 | m'])
⊢ (∀ (s_1 : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s_1, f i = s i),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s_1, s i) fun (ω : Ω) ↦ 1 | m']
        (∏ x ∈ s_1, μ[(s x).indicator fun (ω : Ω) ↦ 1 | m'])) ↔
    ∀ (S : Finset ι),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, s i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ S, μ[(s i).indicator fun (ω : Ω) ↦ 1 | m'])

Tactic:
constructor
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h :
  ∀ (s_1 : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s_1, f i = s i),
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s_1, s i) fun (ω : Ω) ↦ 1 | m']
      (∏ x ∈ s_1, μ[(s x).indicator fun (ω : Ω) ↦ 1 | m'])
S : Finset ι
⊢ (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, s i) fun (ω : Ω) ↦ 1 | m']
    (∏ i ∈ S, μ[(s i).indicator fun (ω : Ω) ↦ 1 | m'])

Tactic:
simp [*]
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ (∀ (S : Finset ι),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, s i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ S, μ[(s i).indicator fun (ω : Ω) ↦ 1 | m'])) →
    ∀ (s_1 : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s_1, f i = s i),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s_1, s i) fun (ω : Ω) ↦ 1 | m']
        (∏ x ∈ s_1, μ[(s x).indicator fun (ω : Ω) ↦ 1 | m'])

Tactic:
grind
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ ∀ (i : ι) (s_1 : Set Ω) (_hs : Membership.mem (γ := Set (Set Ω)) {s i} s_1), MeasurableSet s_1

Tactic:
simpa
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
rw :
  (∀ (t1 t2 : Set Ω),
      Membership.mem (γ := Set (Set Ω)) {s} t1 →
        Membership.mem (γ := Set (Set Ω)) {t} t2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']) ↔
    μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
      HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
rw₁ : ∀ (s_1 : Set Ω), Membership.mem (γ := Set (Set Ω)) {s} s_1 → MeasurableSet s_1
rw₂ : ∀ (s : Set Ω), Membership.mem (γ := Set (Set Ω)) {t} s → MeasurableSet s
⊢ CondIndepSets m' hm' {s} {t} μ ↔
    μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
      HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']

Tactic:
rw [condIndepSets_iff _ _ _ _ ?_ ?_]

Premises used: ProbabilityTheory.condIndepSets_iff
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (∀ (t1 t2 : Set Ω),
      Membership.mem (γ := Set (Set Ω)) {s} t1 →
        Membership.mem (γ := Set (Set Ω)) {t} t2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']) ↔
    μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
      HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' : Set Ω
hs' : Membership.mem (γ := Set (Set Ω)) {s} s'
⊢ s' = s

Tactic:
rw [Set.mem_singleton_iff] at hs'

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' : Set Ω
hs' : s' = s
rwa rwa₁ rwa₂ rwa₃ : MeasurableSet s
⊢ MeasurableSet s'

Tactic:
rwa [hs']
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' : Set Ω
hs' : Membership.mem (γ := Set (Set Ω)) {t} s'
⊢ s' = t

Tactic:
rw [Set.mem_singleton_iff] at hs'

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' : Set Ω
hs' : s' = t
rwa rwa₁ rwa₂ rwa₃ : MeasurableSet t
⊢ MeasurableSet s'

Tactic:
rwa [hs']
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
m : ι → MeasurableSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ iCondIndep m' hm' m μ ↔ iCondIndepSets m' hm' (fun (x : ι) ↦ {s : Set Ω | MeasurableSet s}) μ

Tactic:
simp only [iCondIndep, iCondIndepSets, Kernel.iIndep]

Premises used: ProbabilityTheory.Kernel.iIndep, ProbabilityTheory.iCondIndep, ProbabilityTheory.iCondIndepSets