awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Conditional
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'])
hπ : ∀ (i : ι) (s : Set Ω) (_hs : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s), MeasurableSet s
⊢ 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'])

Tactic:
rw [iCondIndep_iff_iCondIndepSets, iCondIndepSets_iff]

Premises used: ProbabilityTheory.iCondIndepSets_iff, ProbabilityTheory.iCondIndep_iff_iCondIndepSets
-- Module: Mathlib.Probability.Independence.Conditional
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 μ
⊢ (∀ (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:
rfl
-- Module: Mathlib.Probability.Independence.Conditional
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 μ
⊢ ∀ (i : ι) (s : Set Ω) (_hs : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s), MeasurableSet s

Tactic:
hm

Premises used: MeasurableSet, Set.Mem, setOf
-- Module: Mathlib.Probability.Independence.Conditional
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 μ
⊢ ∀ (i : ι) (s : Set Ω) (_hs : Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s), MeasurableSet s

Tactic:
exact hm
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ CondIndep m' m₁ m₂ hm' μ ↔ CondIndepSets m' hm' {s : Set Ω | MeasurableSet s} {s : Set Ω | MeasurableSet s} μ

Tactic:
simp only [CondIndep, CondIndepSets, Kernel.Indep]

Premises used: ProbabilityTheory.Kernel.Indep, ProbabilityTheory.CondIndep, ProbabilityTheory.CondIndepSets
-- Module: Mathlib.Probability.Independence.Conditional
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
hs2 : ∀ (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']

Tactic:
rw [condIndep_iff_condIndepSets, condIndepSets_iff]

Premises used: ProbabilityTheory.condIndepSets_iff, ProbabilityTheory.condIndep_iff_condIndepSets
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ (∀ (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:
rfl
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ ∀ (s : Set Ω), Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s → MeasurableSet s

Tactic:
hm₁

Premises used: MeasurableSet, Set.Mem, setOf
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ ∀ (s : Set Ω), Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s → MeasurableSet s

Tactic:
exact hm₁
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ ∀ (s : Set Ω), Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s → MeasurableSet s

Tactic:
hm₂

Premises used: MeasurableSet, Set.Mem, setOf
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ ∀ (s : Set Ω), Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} s → MeasurableSet s

Tactic:
exact hm₂
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ iCondIndepSet m' hm' s μ ↔ iCondIndep m' hm' (fun (i : ι) ↦ generateFrom {s i}) μ

Tactic:
simp only [iCondIndepSet, iCondIndep, Kernel.iIndepSet]

Premises used: ProbabilityTheory.Kernel.iIndepSet, ProbabilityTheory.iCondIndepSet, ProbabilityTheory.iCondIndep
-- Module: Mathlib.Probability.Independence.Conditional
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 μ ↔ iCondIndepSets m' hm' (fun (i : ι) ↦ {s i}) μ

Tactic:
Kernel.iIndepSet_iff_iIndepSets_singleton hs

Premises used: ProbabilityTheory.iCondIndepSet, ProbabilityTheory.iCondIndepSets, ProbabilityTheory.Kernel.iIndepSet_iff_iIndepSets_singleton
-- Module: Mathlib.Probability.Independence.Conditional
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'])
rw₁ 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'])
⊢ 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'])

Tactic:
rw [iCondIndepSet_iff_iCondIndepSets_singleton _ _ _ hs, iCondIndepSets_singleton_iff _ _ _ hs]

Premises used: ProbabilityTheory.iCondIndepSets_singleton_iff, ProbabilityTheory.iCondIndepSet_iff_iCondIndepSets_singleton
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s t : Set Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ CondIndepSet m' hm' s t μ ↔ CondIndep m' (generateFrom {s}) (generateFrom {t}) hm' μ

Tactic:
simp only [CondIndepSet, CondIndep, Kernel.IndepSet]

Premises used: ProbabilityTheory.CondIndep, ProbabilityTheory.CondIndepSet, ProbabilityTheory.Kernel.IndepSet
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s t : Set Ω
hs_meas : MeasurableSet s
ht_meas : MeasurableSet t
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ CondIndepSet m' hm' s t μ ↔ CondIndepSets m' hm' {s} {t} μ

Tactic:
Kernel.indepSet_iff_indepSets_singleton hs_meas ht_meas _ _

Premises used: ProbabilityTheory.CondIndepSet, ProbabilityTheory.Kernel.indepSet_iff_indepSets_singleton, ProbabilityTheory.CondIndepSets
-- Module: Mathlib.Probability.Independence.Conditional
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']
rw₁ 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']
⊢ CondIndepSet 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]

Premises used: ProbabilityTheory.condIndepSets_singleton_iff, ProbabilityTheory.condIndepSet_iff_condIndepSets_singleton
-- Module: Mathlib.Probability.Independence.Conditional
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
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ iCondIndepFun m' hm' (β := β) f μ ↔ iCondIndep m' hm' (fun (x : ι) ↦ MeasurableSpace.comap (f x) (m x)) μ

Tactic:
simp only [iCondIndepFun, iCondIndep, Kernel.iIndepFun]

Premises used: ProbabilityTheory.iCondIndepFun, ProbabilityTheory.iCondIndep, ProbabilityTheory.Kernel.iIndepFun
-- Module: Mathlib.Probability.Independence.Conditional
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 μ
hm : ∀ (i : ι), MeasurableSpace.comap (f i) (m i) ≤ mΩ
⊢ 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'])

Tactic:
rw [iCondIndep_iff]

Premises used: ProbabilityTheory.iCondIndep_iff
-- Module: Mathlib.Probability.Independence.Conditional
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 μ
⊢ ∀ (i : ι), MeasurableSpace.comap (f i) (m i) ≤ mΩ

Tactic:
fun i ↦ (hf i).comap_le

Premises used: Measurable.comap_le
-- Module: Mathlib.Probability.Independence.Conditional
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 μ
⊢ ∀ (i : ι), MeasurableSpace.comap (f i) (m i) ≤ mΩ

Tactic:
exact fun i ↦ (hf i).comap_le

Premises used: Measurable.comap_le
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ CondIndepFun m' hm' f g μ ↔ CondIndep m' (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) hm' μ

Tactic:
simp only [CondIndepFun, CondIndep, Kernel.IndepFun]

Premises used: ProbabilityTheory.Kernel.IndepFun, ProbabilityTheory.CondIndep, ProbabilityTheory.CondIndepFun
-- Module: Mathlib.Probability.Independence.Conditional
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 μ
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']
rw₁ rw₂ :
  (∀ (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']) ↔
    ∀ (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']
⊢ 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']

Tactic:
rw [condIndepFun_iff_condIndep, condIndep_iff _ _ _ _ hf.comap_le hg.comap_le]

Premises used: ProbabilityTheory.condIndep_iff, Measurable.comap_le, ProbabilityTheory.condIndepFun_iff_condIndep
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s₁ s₂ : Set (Set Ω)
h : CondIndepSets m' hm' s₁ s₂ μ
⊢ CondIndepSets m' hm' s₂ s₁ μ

Tactic:
Kernel.IndepSets.symm h

Premises used: ProbabilityTheory.Kernel.IndepSets.symm, ProbabilityTheory.CondIndepSets
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s₁ s₂ s₃ : Set (Set Ω)
h_indep : CondIndepSets m' hm' s₁ s₂ μ
h31 : s₃ ⊆ s₁
⊢ CondIndepSets m' hm' s₃ s₂ μ

Tactic:
Kernel.indepSets_of_indepSets_of_le_left h_indep h31

Premises used: ProbabilityTheory.Kernel.indepSets_of_indepSets_of_le_left, ProbabilityTheory.CondIndepSets
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s₁ s₂ s₃ : Set (Set Ω)
h_indep : CondIndepSets m' hm' s₁ s₂ μ
h32 : s₃ ⊆ s₂
⊢ CondIndepSets m' hm' s₁ s₃ μ

Tactic:
Kernel.indepSets_of_indepSets_of_le_right h_indep h32

Premises used: ProbabilityTheory.Kernel.indepSets_of_indepSets_of_le_right, ProbabilityTheory.CondIndepSets
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s₁ s₂ s' : Set (Set Ω)
h₁ : CondIndepSets m' hm' s₁ s' μ
h₂ : CondIndepSets m' hm' s₂ s' μ
⊢ CondIndepSets m' hm' (s₁ ∪ s₂) s' μ

Tactic:
Kernel.IndepSets.union h₁ h₂

Premises used: ProbabilityTheory.Kernel.IndepSets.union, ProbabilityTheory.CondIndepSets
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s₁ s₂ s' : Set (Set Ω)
⊢ CondIndepSets m' hm' (s₁ ∪ s₂) s' μ ↔ CondIndepSets m' hm' s₁ s' μ ∧ CondIndepSets m' hm' s₂ s' μ

Tactic:
Kernel.IndepSets.union_iff

Premises used: ProbabilityTheory.Kernel.IndepSets.union_iff, ProbabilityTheory.CondIndepSets
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : ι → Set (Set Ω)
s' : Set (Set Ω)
hyp : ∀ (n : ι), CondIndepSets m' hm' (s n) s' μ
⊢ CondIndepSets m' hm' (⋃ (n : ι), s n) s' μ

Tactic:
Kernel.IndepSets.iUnion hyp

Premises used: ProbabilityTheory.Kernel.IndepSets.iUnion, ProbabilityTheory.CondIndepSets
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : ι → Set (Set Ω)
s' : Set (Set Ω)
u : Set ι
hyp : ∀ n ∈ u, CondIndepSets m' hm' (s n) s' μ
⊢ CondIndepSets m' hm' (⋃ n ∈ u, s n) s' μ

Tactic:
Kernel.IndepSets.biUnion hyp

Premises used: ProbabilityTheory.Kernel.IndepSets.biUnion, ProbabilityTheory.CondIndepSets
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s₁ s' s₂ : Set (Set Ω)
h₁ : CondIndepSets m' hm' s₁ s' μ
⊢ CondIndepSets m' hm' (s₁ ∩ s₂) s' μ

Tactic:
Kernel.IndepSets.inter s₂ h₁

Premises used: ProbabilityTheory.CondIndepSets, ProbabilityTheory.Kernel.IndepSets.inter
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : ι → Set (Set Ω)
s' : Set (Set Ω)
h : ∃ (n : ι), CondIndepSets m' hm' (s n) s' μ
⊢ CondIndepSets m' hm' (⋂ (n : ι), s n) s' μ

Tactic:
Kernel.IndepSets.iInter h

Premises used: ProbabilityTheory.Kernel.IndepSets.iInter, ProbabilityTheory.CondIndepSets
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : ι → Set (Set Ω)
s' : Set (Set Ω)
u : Set ι
h : ∃ n ∈ u, CondIndepSets m' hm' (s n) s' μ
⊢ CondIndepSets m' hm' (⋂ n ∈ u, s n) s' μ

Tactic:
Kernel.IndepSets.bInter h

Premises used: ProbabilityTheory.Kernel.IndepSets.bInter, ProbabilityTheory.CondIndepSets
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
⊢ CondIndepSet m' hm' s ∅ μ

Tactic:
Kernel.indepSet_empty_right s

Premises used: ProbabilityTheory.CondIndepSet, ProbabilityTheory.Kernel.indepSet_empty_right
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
⊢ CondIndepSet m' hm' ∅ s μ

Tactic:
Kernel.indepSet_empty_left s

Premises used: ProbabilityTheory.Kernel.indepSet_empty_left, ProbabilityTheory.CondIndepSet
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h : CondIndep m' m₁ m₂ hm' μ
⊢ CondIndep m' m₂ m₁ hm' μ

Tactic:
CondIndepSets.symm h

Premises used: ProbabilityTheory.Kernel.Indep, ProbabilityTheory.CondIndep, ProbabilityTheory.CondIndepSets.symm
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m₁ m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ CondIndep m' m₁ ⊥ hm' μ

Tactic:
Kernel.indep_bot_right m₁

Premises used: ProbabilityTheory.CondIndep, ProbabilityTheory.Kernel.indep_bot_right
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m₁ m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ CondIndep m' ⊥ m₁ hm' μ

Tactic:
(Kernel.indep_bot_right m₁).symm

Premises used: ProbabilityTheory.Kernel.Indep.symm, ProbabilityTheory.CondIndep, ProbabilityTheory.Kernel.indep_bot_right
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' m₁ m₂ m₃ mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h_indep : CondIndep m' m₁ m₂ hm' μ
h31 : m₃ ≤ m₁
⊢ CondIndep m' m₃ m₂ hm' μ

Tactic:
Kernel.indep_of_indep_of_le_left h_indep h31

Premises used: ProbabilityTheory.Kernel.indep_of_indep_of_le_left, ProbabilityTheory.CondIndep
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
m' m₁ m₂ m₃ mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h_indep : CondIndep m' m₁ m₂ hm' μ
h32 : m₃ ≤ m₂
⊢ CondIndep m' m₁ m₃ hm' μ

Tactic:
Kernel.indep_of_indep_of_le_right h_indep h32

Premises used: ProbabilityTheory.CondIndep, ProbabilityTheory.Kernel.indep_of_indep_of_le_right
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : ι → Set (Set Ω)
h_indep : iCondIndepSets m' hm' s μ
i j : ι
hij : i ≠ j
⊢ CondIndepSets m' hm' (s i) (s j) μ

Tactic:
Kernel.iIndepSets.indepSets h_indep hij

Premises used: ProbabilityTheory.Kernel.iIndepSets.indepSets, ProbabilityTheory.CondIndepSets
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
m : ι → MeasurableSpace Ω
h_indep : iCondIndep m' hm' m μ
i j : ι
hij : i ≠ j
⊢ CondIndep m' (m i) (m j) hm' μ

Tactic:
Kernel.iIndep.indep h_indep hij

Premises used: ProbabilityTheory.CondIndep, ProbabilityTheory.Kernel.iIndep.indep
-- Module: Mathlib.Probability.Independence.Conditional
Goal:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : ι → Type u_3
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf_Indep : iCondIndepFun m' hm' (β := β) f μ
i j : ι
hij : i ≠ j
⊢ CondIndepFun m' hm' (f i) (f j) μ

Tactic:
Kernel.iIndepFun.indepFun hf_Indep hij

Premises used: ProbabilityTheory.Kernel.iIndepFun.indepFun, ProbabilityTheory.CondIndepFun