awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
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∞)
⊢ (((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∞)
have 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∞) ≠
  ∞
Tactic: rw [← ENNReal.ofReal_toReal h_ne_top, hst_eq, h, Pi.mul_apply, ← hs_eq, ← ht_eq,
      ← ENNReal.toReal_mul, ENNReal.ofReal_toReal]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
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 μ
⊢ 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'])
have 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'])
Tactic: rw [iCondIndepSets_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
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'])
⊢ 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'])
have hπ₁ : ∀ (i : ι) (s_1 : Set Ω) (_hs : Membership.mem (γ := Set (Set Ω)) {s i} s_1), MeasurableSet s_1
Tactic: rw [iCondIndepSets_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
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_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'])
have 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'])
Tactic: simp_all only [Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
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_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'])
have 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'])
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
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'])
⊢ (∀ (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'])
have 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'])
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
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
⊢ CondIndepSets m' hm' {s} {t} μ ↔
    μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
      HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
have 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']
Tactic: rw [condIndepSets_iff _ _ _ _ ?_ ?_]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
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']
⊢ CondIndepSets m' hm' {s} {t} μ ↔
    μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
      HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
have rw₁ : ∀ (s_1 : Set Ω), Membership.mem (γ := Set (Set Ω)) {s} s_1 → MeasurableSet s_1
Tactic: rw [condIndepSets_iff _ _ _ _ ?_ ?_]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
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
⊢ CondIndepSets m' hm' {s} {t} μ ↔
    μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
      HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
have rw₂ : ∀ (s : Set Ω), Membership.mem (γ := Set (Set Ω)) {t} s → MeasurableSet s
Tactic: rw [condIndepSets_iff _ _ _ _ ?_ ?_]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
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'
⊢ MeasurableSet s'
have hs'₁ : s' = s
Tactic: rw [Set.mem_singleton_iff] at hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (hypothesis)
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'
⊢ MeasurableSet s'
have hs'₁ : s' = t
Tactic: rw [Set.mem_singleton_iff] at hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
m : ι → MeasurableSpace Ω
hm : ∀ (i : ι), m i ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ iCondIndep m' hm' m μ ↔
    ∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (f i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'])
have rw : (∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s, Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (f i)),
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
      (∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'])) ↔
  ∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (f i)),
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
      (∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'])
Tactic: rw [iCondIndep_iff_iCondIndepSets, iCondIndepSets_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
m : ι → MeasurableSpace Ω
hm : ∀ (i : ι), m i ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
rw :
  (∀ (s : Finset ι) {f : ι → Set Ω}
      (_H : ∀ i ∈ s, Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} (f i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'])) ↔
    ∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (f i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'])
⊢ iCondIndep m' hm' m μ ↔
    ∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (f i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, f i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ s, μ[(f i).indicator fun (ω : Ω) ↦ 1 | m'])
have hπ : ∀ (i : ι) (s : Set Ω) (_hs : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s), MeasurableSet s
Tactic: rw [iCondIndep_iff_iCondIndepSets, iCondIndepSets_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ CondIndep m' m₁ m₂ hm' μ ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
have rw : (∀ (t1 t2 : Set Ω),
    Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t1 →
      Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t2 →
        μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
          HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']) ↔
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
          HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
Tactic: rw [condIndep_iff_condIndepSets, condIndepSets_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
rw :
  (∀ (t1 t2 : Set Ω),
      Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t1 →
        Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']) ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
⊢ CondIndep m' m₁ m₂ hm' μ ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
have hs1 : ∀ (s : Set Ω), Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s → MeasurableSet s
Tactic: rw [condIndep_iff_condIndepSets, condIndepSets_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
rw :
  (∀ (t1 t2 : Set Ω),
      Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t1 →
        Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']) ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
hs1 : ∀ (s : Set Ω), Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s → MeasurableSet s
⊢ CondIndep m' m₁ m₂ hm' μ ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
have hs2 : ∀ (s : Set Ω), Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s → MeasurableSet s
Tactic: rw [condIndep_iff_condIndepSets, condIndepSets_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hs : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ iCondIndepSet m' hm' s μ ↔
    ∀ (S : Finset ι),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, s i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ S, μ[(s i).indicator fun (ω : Ω) ↦ 1 | m'])
have rw : 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 [iCondIndepSet_iff_iCondIndepSets_singleton _ _ _ hs, iCondIndepSets_singleton_iff _ _ _ hs]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hs : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
rw :
  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'])
⊢ iCondIndepSet m' hm' s μ ↔
    ∀ (S : Finset ι),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, s i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ S, μ[(s i).indicator fun (ω : Ω) ↦ 1 | m'])
have rw₁ : (∀ (S : Finset ι),
    (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ S, s i) fun (ω : Ω) ↦ 1 | m']
      (∏ i ∈ S, μ[(s 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: rw [iCondIndepSet_iff_iCondIndepSets_singleton _ _ _ hs, iCondIndepSets_singleton_iff _ _ _ hs]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ CondIndepSet m' hm' s t μ ↔
    μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
      HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
have rw : 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 [condIndepSet_iff_condIndepSets_singleton _ _ hs ht μ, condIndepSets_singleton_iff _ _ hs ht]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
rw :
  CondIndepSets m' hm' {s} {t} μ ↔
    μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
      HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
⊢ CondIndepSet m' hm' s t μ ↔
    μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
      HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
have rw₁ : μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m'] ↔
  μ[(s ∩ t).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
    HMul.hMul (α := Ω → ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m'] μ[t.indicator fun (ω : Ω) ↦ 1 | m']
Tactic: rw [condIndepSet_iff_condIndepSets_singleton _ _ hs ht μ, condIndepSets_singleton_iff _ _ hs ht]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : ι → Type u_3
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
hf : ∀ (i : ι), Measurable (f i)
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ iCondIndep m' hm' (fun (x : ι) ↦ MeasurableSpace.comap (f x) (m x)) μ ↔
    ∀ (s : Finset ι) {g : ι → Set Ω} (_H : ∀ i ∈ s, MeasurableSet (g i)),
      (ae μ).EventuallyEq (β := ℝ) μ[Set.indicator (⋂ i ∈ s, g i) fun (ω : Ω) ↦ 1 | m']
        (∏ i ∈ s, μ[(g i).indicator fun (ω : Ω) ↦ 1 | m'])
have hm : ∀ (i : ι), MeasurableSpace.comap (f i) (m i) ≤ mΩ
Tactic: rw [iCondIndep_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
hf : Measurable f
hg : Measurable g
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ CondIndepFun m' hm' f g μ ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
            HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
have rw : CondIndep m' (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) hm' μ ↔
  ∀ (t1 t2 : Set Ω),
    MeasurableSet t1 →
      MeasurableSet t2 →
        μ[(t1 ∩ t2).indicator fun (ω : Ω) ↦ 1 | m'] =ᶠ[ae μ]
          HMul.hMul (α := Ω → ℝ) μ[t1.indicator fun (ω : Ω) ↦ 1 | m'] μ[t2.indicator fun (ω : Ω) ↦ 1 | m']
Tactic: rw [condIndepFun_iff_condIndep, condIndep_iff _ _ _ _ hf.comap_le hg.comap_le]