awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 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)

Tactic:
⟨c, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- 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 c : β
hc : (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns a) (ns c) ∧ (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns b) (ns c)
inr :
  (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) a)
    ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) c)
inr₁ :
  (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) b)
    ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) 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)

Tactic:
refine ⟨c, ?_, ?_⟩
-- 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 c : β
hc : (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns a) (ns c) ∧ (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns b) (ns c)
⊢ (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) a)
    ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) c)

Tactic:
iSup_mono fun n => iSup_mono' fun hn => ⟨?_, le_rfl⟩

Premises used: le_rfl, iSup_mono', Exists.intro, iSup_mono
-- 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 c : β
hc : (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns a) (ns c) ∧ (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns b) (ns c)
inr : ∀ (n : ι) (hn : n ∈ ns a), n ∈ ns c
⊢ (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) a)
    ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) c)

Tactic:
refine iSup_mono fun n => iSup_mono' fun hn => ⟨?_, le_rfl⟩

Premises used: iSup_mono', Exists.intro, iSup_mono
-- 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 c : β
hc : (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns a) (ns c) ∧ (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns b) (ns c)
⊢ (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) b)
    ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) c)

Tactic:
iSup_mono fun n => iSup_mono' fun hn => ⟨?_, le_rfl⟩

Premises used: le_rfl, iSup_mono', Exists.intro, iSup_mono
-- 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 c : β
hc : (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns a) (ns c) ∧ (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns b) (ns c)
inr : ∀ (n : ι) (hn : n ∈ ns b), n ∈ ns c
⊢ (fun (x1 x2 : MeasurableSpace Ω) ↦ x1 ≤ x2) ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) b)
    ((fun (i : β) ↦ (⨆ n ∈ ns i, s n : MeasurableSpace Ω)) c)

Tactic:
refine iSup_mono fun n => iSup_mono' fun hn => ⟨?_, le_rfl⟩

Premises used: iSup_mono', Exists.intro, iSup_mono
-- 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 c : β
hc : (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns a) (ns c) ∧ (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns b) (ns c)
n : ι
hn : n ∈ ns a
⊢ n ∈ ns c

Tactic:
hc.1 hn

Premises used: And.left
-- 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 c : β
hc : (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns a) (ns c) ∧ (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns b) (ns c)
n : ι
hn : n ∈ ns a
⊢ n ∈ ns c

Tactic:
exact hc.1 hn

Premises used: And.left
-- 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 c : β
hc : (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns a) (ns c) ∧ (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns b) (ns c)
n : ι
hn : n ∈ ns b
⊢ n ∈ ns c

Tactic:
hc.2 hn

Premises used: And.right
-- 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 c : β
hc : (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns a) (ns c) ∧ (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) (ns b) (ns c)
n : ι
hn : n ∈ ns b
⊢ n ∈ ns c

Tactic:
exact hc.2 hn

Premises used: And.right
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
μ : 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)
⊢ Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) μ

Tactic:
Kernel.indep_iSup_directed_limsup h_le h_indep hf hns hnsp

Premises used: ProbabilityTheory.Kernel.indep_iSup_directed_limsup, ProbabilityTheory.Indep
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m m0 : MeasurableSpace Ω
μ : Measure Ω
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
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
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
⊢ CondIndep m (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) hm μ

Tactic:
Kernel.indep_iSup_directed_limsup h_le h_indep hf hns hnsp

Premises used: ProbabilityTheory.Kernel.indep_iSup_directed_limsup, ProbabilityTheory.CondIndep
-- 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)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
this : Eq.{u_2 + 1} (α := MeasurableSpace Ω) (⨆ (a : β), ⨆ n ∈ ns a, s n) (⨆ (n : ι), s n)
rw : Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ μα
⊢ Indep (⨆ (n : ι), s n) (limsup s f) κ μα

Tactic:
rw [← this]
-- 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)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
this : Eq.{u_2 + 1} (α := MeasurableSpace Ω) (⨆ (a : β), ⨆ n ∈ ns a, s n) (⨆ (n : ι), s n)
⊢ Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ μα

Tactic:
indep_iSup_directed_limsup h_le h_indep hf hns hnsp

Premises used: ProbabilityTheory.Kernel.indep_iSup_directed_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)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
this : Eq.{u_2 + 1} (α := MeasurableSpace Ω) (⨆ (a : β), ⨆ n ∈ ns a, s n) (⨆ (n : ι), s n)
⊢ Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ μα

Tactic:
exact indep_iSup_directed_limsup h_le h_indep hf hns hnsp

Premises used: ProbabilityTheory.Kernel.indep_iSup_directed_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)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
suffices : Eq.{u_2 + 1} (α := MeasurableSpace Ω) (⨆ (a : β), ⨆ n ∈ ns a, s n) (⨆ (n : ι), s n)
⊢ Indep (⨆ (n : ι), s n) (limsup s f) κ μα

Tactic:
suffices (⨆ a, ⨆ n ∈ ns a, s n) = ⨆ n, s n by
    rw [← this]
    exact indep_iSup_directed_limsup h_le h_indep hf hns hnsp
-- 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)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
rw : Eq.{u_2 + 1} (α := MeasurableSpace Ω) (⨆ (j : ι), ⨆ (i : β), ⨆ (_ : j ∈ ns i), s j) (⨆ (n : ι), s n)
⊢ Eq.{u_2 + 1} (α := MeasurableSpace Ω) (⨆ (a : β), ⨆ n ∈ ns a, s n) (⨆ (n : ι), s n)

Tactic:
rw [iSup_comm]

Premises used: iSup_comm
-- 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)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
⊢ Eq.{u_2 + 1} (α := MeasurableSpace Ω) (⨆ (j : ι), ⨆ (i : β), ⨆ (_ : j ∈ ns i), s j) (⨆ (n : ι), s n)

Tactic:
iSup_congr fun n => ?_

Premises used: iSup_congr
-- 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)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
refine : ∀ (n : ι), ⨆ (i : β), ⨆ (_ : n ∈ ns i), s n = s n
⊢ Eq.{u_2 + 1} (α := MeasurableSpace Ω) (⨆ (j : ι), ⨆ (i : β), ⨆ (_ : j ∈ ns i), s j) (⨆ (n : ι), s n)

Tactic:
refine iSup_congr fun n => ?_

Premises used: iSup_congr
-- 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)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
n : ι
rw rw₁ : Eq.{u_2 + 1} (α := MeasurableSpace Ω) (⨆ (i : β), ⨆ (_ : n ∈ ns i), s n) (⨆ (i : β), ⨆ (_ : n ∈ ns i), s n)
⊢ Eq.{u_2 + 1} (α := MeasurableSpace Ω) (⨆ (i : β), ⨆ (_ : n ∈ ns i), s n) (⨆ (_ : ∃ (i : β), n ∈ ns i), s n)

Tactic:
rw [iSup_exists]

Premises used: iSup_exists
-- 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)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
n : ι
⊢ Eq.{u_2 + 1} (α := MeasurableSpace Ω) (⨆ (i : β), ⨆ (_ : n ∈ ns i), s n) (⨆ (_ : ∃ (i : β), n ∈ ns i), s n)

Tactic:
have h : ⨆ (i : β) (_ : n ∈ ns i), s n = ⨆ _ : ∃ i, n ∈ ns i, s n := by rw [iSup_exists]
-- 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)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
n : ι
h : Eq.{u_2 + 1} (α := MeasurableSpace Ω) (⨆ (i : β), ⨆ (_ : n ∈ ns i), s n) (⨆ (_ : ∃ (i : β), n ∈ ns i), s n)
⊢ Nonempty (∃ (i : β), n ∈ ns i)

Tactic:
haveI : Nonempty (∃ i : β, n ∈ ns i) := ⟨hns_univ n⟩
-- 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)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
n : ι
h : Eq.{u_2 + 1} (α := MeasurableSpace Ω) (⨆ (i : β), ⨆ (_ : n ∈ ns i), s n) (⨆ (_ : ∃ (i : β), n ∈ ns i), s n)
this : Nonempty (∃ (i : β), n ∈ ns i)
rw : ⨆ (_ : ∃ (i : β), n ∈ ns i), s n = s n
rw₁ rw₂ : s n = s n
⊢ ⨆ (i : β), ⨆ (_ : n ∈ ns i), s n = s n

Tactic:
rw [h, iSup_const]

Premises used: iSup_const
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
μ : 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)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
⊢ Indep (⨆ (n : ι), s n) (limsup s f) μ

Tactic:
Kernel.indep_iSup_limsup h_le h_indep hf hns hnsp hns_univ

Premises used: ProbabilityTheory.Kernel.indep_iSup_limsup, ProbabilityTheory.Indep
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m m0 : MeasurableSpace Ω
μ : Measure Ω
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
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
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
⊢ CondIndep m (⨆ (n : ι), s n) (limsup s f) hm μ

Tactic:
Kernel.indep_iSup_limsup h_le h_indep hf hns hnsp hns_univ

Premises used: ProbabilityTheory.Kernel.indep_iSup_limsup, ProbabilityTheory.CondIndep
-- 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)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
⊢ Indep (limsup s f) (limsup s f) κ μα

Tactic:
indep_of_indep_of_le_left (indep_iSup_limsup h_le h_indep hf hns hnsp hns_univ) limsup_le_iSup

Premises used: ProbabilityTheory.Kernel.indep_iSup_limsup, ProbabilityTheory.Kernel.indep_of_indep_of_le_left, Filter.limsup_le_iSup
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
μ : 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)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
⊢ Indep (limsup s f) (limsup s f) μ

Tactic:
Kernel.indep_limsup_self h_le h_indep hf hns hnsp hns_univ

Premises used: ProbabilityTheory.Kernel.indep_limsup_self, ProbabilityTheory.Indep
-- Module: Mathlib.Probability.Independence.ZeroOne
Goal:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m m0 : MeasurableSpace Ω
μ : Measure Ω
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
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
hns : Directed (fun (x1 x2 : Set ι) ↦ x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
⊢ CondIndep m (limsup s f) (limsup s f) hm μ

Tactic:
Kernel.indep_limsup_self h_le h_indep hf hns hnsp hns_univ

Premises used: ProbabilityTheory.Kernel.indep_limsup_self, ProbabilityTheory.CondIndep
-- 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)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
apply : ∀ᵐ (a : α) ∂μα, IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
⊢ ∀ᵐ (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:
apply measure_eq_zero_or_one_of_indepSet_self' ?_
    ((indep_limsup_self h_le h_indep hf hns hnsp hns_univ).indepSet_of_measurableSet ht_tail
      ht_tail)

Premises used: ProbabilityTheory.Kernel.measure_eq_zero_or_one_of_indepSet_self', ProbabilityTheory.Kernel.indep_limsup_self, ProbabilityTheory.Kernel.Indep.indepSet_of_measurableSet
-- 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)
hns_univ : ∀ (n : ι), ∃ (a : β), n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
a : α
ha : IsProbabilityMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
⊢ IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)

Tactic:
infer_instance