awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
h : ∀ᵐ (a : α) ∂μα, IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
t : Set Ω
h_indep : IndepSet t t κ μα
a : α
h_0_1_top :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h' : IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simpa only [measure_ne_top (κ a), or_false] using h_0_1_top

Premises used: MeasureTheory.measure_ne_top, or_false, DFunLike.coe
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
h : ∀ (a : α), IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
t : Set Ω
h_indep : IndepSet t t κ μα
⊢ ∀ᵐ (a : α) ∂μα,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
Kernel.measure_eq_zero_or_one_of_indepSet_self' (ae_of_all μα h) h_indep

Premises used: ProbabilityTheory.Kernel.measure_eq_zero_or_one_of_indepSet_self', MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
t : Set Ω
h_indep : IndepSet t t μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simpa only [ae_dirac_eq, Filter.eventually_pure]
    using Kernel.measure_eq_zero_or_one_of_indepSet_self h_indep

Premises used: ProbabilityTheory.Kernel.measure_eq_zero_or_one_of_indepSet_self, MeasureTheory.ae_dirac_eq, Filter.eventually_pure
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
hm : m ≤ m0
hμ : IsFiniteMeasure μ
t : Set Ω
ht : MeasurableSet t
h_indep : CondIndepSet m hm t t μ
⊢ ∀ (a : Ω), IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) a)

Tactic:
have (a : _) : IsFiniteMeasure (condExpKernel μ m a) := inferInstance
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
hm : m ≤ m0
hμ : IsFiniteMeasure μ
t : Set Ω
ht : MeasurableSet t
h_indep : CondIndepSet m hm t t μ
this : ∀ (a : Ω), IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) a)
⊢ ∀ᵐ (x : Ω) ∂μ,
    Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        (1 : ℝ≥0∞)

Tactic:
have h := ae_of_ae_trim hm (Kernel.measure_eq_zero_or_one_of_indepSet_self h_indep)
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
hm : m ≤ m0
hμ : IsFiniteMeasure μ
t : Set Ω
ht : MeasurableSet t
h_indep : CondIndepSet m hm t t μ
this : ∀ (a : Ω), IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) a)
h :
  ∀ᵐ (x : Ω) ∂μ,
    Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        (1 : ℝ≥0∞)
h₁ :
  ∀ (ω : Ω)
    (hω_eq :
      Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω)
    (hω :
      Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
          (0 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
          (1 : ℝ≥0∞)),
    Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 0 ∨ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 1
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 0 ∨ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 1

Tactic:
filter_upwards [condExpKernel_ae_eq_condExp hm ht, h] with ω hω_eq hω

Premises used: ProbabilityTheory.condExpKernel_ae_eq_condExp
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
hm : m ≤ m0
hμ : IsFiniteMeasure μ
t : Set Ω
ht : MeasurableSet t
h_indep : CondIndepSet m hm t t μ
this : ∀ (a : Ω), IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) a)
h :
  ∀ᵐ (x : Ω) ∂μ,
    Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
        (1 : ℝ≥0∞)
ω : Ω
hω_eq : Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω
hω :
  Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      (1 : ℝ≥0∞)
h₁ :
  Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = 0 ∨
    Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = 1
h₂ :
  Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      (0 : ℝ≥0∞) ∨
    Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = 1
h₃ :
  Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      (0 : ℝ≥0∞) ∨
    ENNReal.toReal ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t) = 1
h₄ h₅ h₆ h₇ :
  Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
      (1 : ℝ≥0∞)
⊢ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 0 ∨ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 1

Tactic:
rwa [← hω_eq, measureReal_eq_zero_iff, measureReal_def, ENNReal.toReal_eq_one_iff]

Premises used: MeasureTheory.measureReal_def, MeasureTheory.measureReal_eq_zero_iff, ENNReal.toReal_eq_one_iff
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
t : Set ι
⊢ Indep (⨆ n ∈ t, s n) (⨆ n ∈ tᶜ, s n) κ μα

Tactic:
indep_iSup_of_disjoint h_le h_indep disjoint_compl_right

Premises used: disjoint_compl_right, ProbabilityTheory.Kernel.indep_iSup_of_disjoint
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
μ : Measure Ω
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s μ
t : Set ι
⊢ Indep (⨆ n ∈ t, s n) (⨆ n ∈ tᶜ, s n) μ

Tactic:
Kernel.indep_biSup_compl h_le h_indep t

Premises used: ProbabilityTheory.Indep, ProbabilityTheory.Kernel.indep_biSup_compl
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m m0 : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
hm : m ≤ m0
inst_1 : IsFiniteMeasure μ
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iCondIndep m hm s μ
t : Set ι
⊢ CondIndep m (⨆ n ∈ t, s n) (⨆ n ∈ tᶜ, s n) hm μ

Tactic:
Kernel.indep_biSup_compl h_le h_indep t

Premises used: ProbabilityTheory.CondIndep, ProbabilityTheory.Kernel.indep_biSup_compl
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
p : Set ι → Prop
f : Filter ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
⊢ Indep (⨆ n ∈ t, s n) (limsup s f) κ μα

Tactic:
indep_of_indep_of_le_right (indep_biSup_compl h_le h_indep t) ?_

Premises used: ProbabilityTheory.Kernel.indep_of_indep_of_le_right, ProbabilityTheory.Kernel.indep_biSup_compl
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
p : Set ι → Prop
f : Filter ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
refine : limsup s f ≤ ⨆ n ∈ tᶜ, s n
⊢ Indep (⨆ n ∈ t, s n) (limsup s f) κ μα

Tactic:
refine indep_of_indep_of_le_right (indep_biSup_compl h_le h_indep t) ?_

Premises used: ProbabilityTheory.Kernel.indep_of_indep_of_le_right, ProbabilityTheory.Kernel.indep_biSup_compl
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
p : Set ι → Prop
f : Filter ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
⊢ IsCobounded (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) (Filter.map s f)

Tactic:
isBoundedDefault
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
p : Set ι → Prop
f : Filter ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
refine : ∀ᶠ (n : MeasurableSpace Ω) in Filter.map s f, n ≤ ⨆ n ∈ tᶜ, s n
⊢ limsup s f ≤ ⨆ n ∈ tᶜ, s n

Tactic:
refine limsSup_le_of_le (by isBoundedDefault) ?_

Premises used: Filter.limsSup_le_of_le
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
p : Set ι → Prop
f : Filter ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
simp : ∀ᶠ (a : ι) in f, s a ≤ ⨆ (n : ι), ⨆ (_ : n ∉ t), s n
⊢ ∀ᶠ (n : MeasurableSpace Ω) in Filter.map s f, n ≤ ⨆ n ∈ tᶜ, s n

Tactic:
simp only [Set.mem_compl_iff, eventually_map]

Premises used: Filter.eventually_map, Set.mem_compl_iff
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
p : Set ι → Prop
f : Filter ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
⊢ ∀ᶠ (a : ι) in f, s a ≤ ⨆ (n : ι), ⨆ (_ : n ∉ t), s n

Tactic:
eventually_of_mem (hf t ht) le_iSup₂

Premises used: le_iSup₂, Filter.eventually_of_mem
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
p : Set ι → Prop
f : Filter ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
⊢ ∀ᶠ (a : ι) in f, s a ≤ ⨆ (n : ι), ⨆ (_ : n ∉ t), s n

Tactic:
exact eventually_of_mem (hf t ht) le_iSup₂

Premises used: le_iSup₂, Filter.eventually_of_mem
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
μ : Measure Ω
p : Set ι → Prop
f : Filter ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s μ
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
⊢ Indep (⨆ n ∈ t, s n) (limsup s f) μ

Tactic:
Kernel.indep_biSup_limsup h_le h_indep hf ht

Premises used: ProbabilityTheory.Kernel.indep_biSup_limsup, ProbabilityTheory.Indep
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m m0 : MeasurableSpace Ω
μ : Measure Ω
p : Set ι → Prop
f : Filter ι
inst : StandardBorelSpace Ω
hm : m ≤ m0
inst_1 : IsFiniteMeasure μ
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iCondIndep m hm s μ
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
t : Set ι
ht : p t
⊢ CondIndep m (⨆ n ∈ t, s n) (limsup s f) hm μ

Tactic:
Kernel.indep_biSup_limsup h_le h_indep hf ht

Premises used: ProbabilityTheory.CondIndep, ProbabilityTheory.Kernel.indep_biSup_limsup
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
inl : ∀ (h_indep : iIndep s κ 0), Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ 0
inr : ∀ (hμ : μα ≠ 0), Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ μα
⊢ Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ μα

Tactic:
rcases eq_or_ne μα 0 with rfl | hμ

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
h_indep : iIndep s κ 0
⊢ Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ 0

Tactic:
simp
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
⊢ ∃ (η : Kernel α Ω),
    EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω) ∧
      IsMarkovKernel η

Tactic:
exists_ae_eq_isMarkovKernel h_indep.ae_isProbabilityMeasure hμ

Premises used: ProbabilityTheory.Kernel.exists_ae_eq_isMarkovKernel, ProbabilityTheory.Kernel.iIndep.ae_isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
inr :
  ∀ (η : Kernel α Ω)
    (η_eq : EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ μα
⊢ Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ μα

Tactic:
obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μα] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel h_indep.ae_isProbabilityMeasure hμ

Premises used: ProbabilityTheory.Kernel.exists_ae_eq_isMarkovKernel, ProbabilityTheory.Kernel.iIndep.ae_isProbabilityMeasure, ProbabilityTheory.Kernel
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
⊢ iIndep s η μα

Tactic:
replace h_indep := h_indep.congr η_eq
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
h_indep : iIndep s η μα
inr : Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) η μα
⊢ Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ μα

Tactic:
apply Indep.congr (Filter.EventuallyEq.symm η_eq)

Premises used: ProbabilityTheory.Kernel.Indep.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
h_indep : iIndep s η μα
inr : ∀ (i : β), Indep (⨆ n ∈ ns i, s n) (limsup s f) η μα
inr₁ : ∀ (i : β), ⨆ n ∈ ns i, s n ≤ m0
inr₂ : limsup s f ≤ m0
inr₃ : Directed (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) fun (i : β) ↦ ⨆ n ∈ ns i, s n
⊢ Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) η μα

Tactic:
apply indep_iSup_of_directed_le

Premises used: ProbabilityTheory.Kernel.indep_iSup_of_directed_le
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
h_indep : iIndep s η μα
⊢ ∀ (i : β), Indep (⨆ n ∈ ns i, s n) (limsup s f) η μα

Tactic:
fun a => indep_biSup_limsup h_le h_indep hf (hnsp a)

Premises used: ProbabilityTheory.Kernel.indep_biSup_limsup
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
h_indep : iIndep s η μα
⊢ ∀ (i : β), Indep (⨆ n ∈ ns i, s n) (limsup s f) η μα

Tactic:
exact fun a => indep_biSup_limsup h_le h_indep hf (hnsp a)

Premises used: ProbabilityTheory.Kernel.indep_biSup_limsup
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
h_indep : iIndep s η μα
⊢ ∀ (i : β), ⨆ n ∈ ns i, s n ≤ m0

Tactic:
fun a => iSup₂_le fun n _ => h_le n

Premises used: iSup₂_le
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
h_indep : iIndep s η μα
⊢ ∀ (i : β), ⨆ n ∈ ns i, s n ≤ m0

Tactic:
exact fun a => iSup₂_le fun n _ => h_le n

Premises used: iSup₂_le
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
h_indep : iIndep s η μα
⊢ limsup s f ≤ m0

Tactic:
limsup_le_iSup.trans (iSup_le h_le)

Premises used: Filter.limsup_le_iSup, iSup_le, LE.le.trans
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
h_indep : iIndep s η μα
⊢ limsup s f ≤ m0

Tactic:
exact limsup_le_iSup.trans (iSup_le h_le)

Premises used: Filter.limsup_le_iSup, iSup_le, LE.le.trans
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μα) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
h_indep : iIndep s η μα
a b : β
inr :
  ∀ (c : β) (hc : (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns a) (ns c) ∧ (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns b) (ns c)),
    ∃ (z : β),
      (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) a)
          ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) z) ∧
        (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) b)
          ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) z)
⊢ ∃ (z : β),
    (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) a)
        ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) z) ∧
      (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) b)
        ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) z)

Tactic:
obtain ⟨c, hc⟩ := hns a b