awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
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 : β
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨c, hc⟩ := hns a b
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
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)
have 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)
Tactic: refine ⟨c, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: refine ⟨c, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
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)
have inr : ∀ (n : ι) (hn : n ∈ ns a), n ∈ ns c
Tactic: refine iSup_mono fun n => iSup_mono' fun hn => ⟨?_, le_rfl⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
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)
have inr : ∀ (n : ι) (hn : n ∈ ns b), n ∈ ns c
Tactic: refine iSup_mono fun n => iSup_mono' fun hn => ⟨?_, le_rfl⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
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 (⨆ (n : ι), s n) (limsup s f) κ μα
have rw : Indep (⨆ (a : β), ⨆ n ∈ ns a, s n) (limsup s f) κ μα
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
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 (⨆ (n : ι), s n) (limsup s f) κ μα
have suffices : Eq.{u_2 + 1} (α := MeasurableSpace Ω) (⨆ (a : β), ⨆ n ∈ ns a, s n) (⨆ (n : ι), s n)
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
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
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 Ω) (⨆ (a : β), ⨆ n ∈ ns a, s n) (⨆ (n : ι), s n)
have rw : Eq.{u_2 + 1} (α := MeasurableSpace Ω) (⨆ (j : ι), ⨆ (i : β), ⨆ (_ : j ∈ ns i), s j) (⨆ (n : ι), s n)
Tactic: rw [iSup_comm]
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
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)
have refine : ∀ (n : ι), ⨆ (i : β), ⨆ (_ : n ∈ ns i), s n = s n
Tactic: refine iSup_congr fun n => ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
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)
have rw : Eq.{u_2 + 1} (α := MeasurableSpace Ω) (⨆ (i : β), ⨆ (_ : n ∈ ns i), s n) (⨆ (i : β), ⨆ (_ : n ∈ ns i), s n)
Tactic: rw [iSup_exists]
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (hypothesis)
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 : ι
⊢ ⨆ (i : β), ⨆ (_ : n ∈ ns i), s n = s n
have h : 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]
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (hypothesis)
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)
⊢ ⨆ (i : β), ⨆ (_ : n ∈ ns i), s n = s n
have this : Nonempty (∃ (i : β), n ∈ ns i)
Tactic: haveI : Nonempty (∃ i : β, n ∈ ns i) := ⟨hns_univ n⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
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)
⊢ ⨆ (i : β), ⨆ (_ : n ∈ ns i), s n = s n
have rw : ⨆ (_ : ∃ (i : β), n ∈ ns i), s n = s n
Tactic: rw [h, iSup_const]
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
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
⊢ ⨆ (i : β), ⨆ (_ : n ∈ ns i), s n = s n
have rw₁ : s n = s n
Tactic: rw [h, iSup_const]
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
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 : α) ∂μα,
    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∞)
have apply : ∀ᵐ (a : α) ∂μα, IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
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)
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
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 : α) ∂μα, IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α)
          {x : α | (fun (a : α) ↦ IsProbabilityMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)) x} x →
        Membership.mem (γ := Set α)
          {x : α | (fun (a : α) ↦ IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)) x} x}
    a
Tactic: filter_upwards [h_indep.ae_isProbabilityMeasure] with a ha using by infer_instance
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
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
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α | (fun (a : α) ↦ IsProbabilityMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)) x} x →
          Membership.mem (γ := Set α)
            {x : α | (fun (a : α) ↦ IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)) x} x}
      a
⊢ ∀ᵐ (a : α) ∂μα, IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
have h₁ : ∀ (a : α),
  IsProbabilityMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a) →
    IsFiniteMeasure.{u_2} (α := Ω) (m0 := m0) ((κ : (a : α) → Measure Ω) a)
Tactic: filter_upwards [h_indep.ae_isProbabilityMeasure] with a ha using by infer_instance
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (hypothesis)
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
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 0 ∨ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 1
have 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∞)
Tactic: have h := ae_of_ae_trim hm
    (Kernel.measure_zero_or_one_of_measurableSet_limsup h_le h_indep hf hns hnsp hns_univ ht_tail)
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (hypothesis)
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
t : Set Ω
ht_tail : MeasurableSet t
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∞)
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 0 ∨ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 1
have ht : MeasurableSet t
Tactic: have ht : MeasurableSet t := limsup_le_iSup.trans (iSup_le h_le) t ht_tail
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
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
t : Set Ω
ht_tail : MeasurableSet t
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∞)
ht : MeasurableSet t
⊢ ∀ᵐ (ω : Ω) ∂μ,
    Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 0 ∨ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 1
have 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
Tactic: filter_upwards [condExpKernel_ae_eq_condExp hm ht, h] with ω hω_eq hω
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
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
t : Set Ω
ht_tail : MeasurableSet t
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∞)
ht : MeasurableSet t
ω : Ω
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
have h₁ : Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = 0 ∨
  Measure.real (m := m0) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) t = 1
Tactic: rwa [← hω_eq, measureReal_eq_zero_iff, measureReal_def, ENNReal.toReal_eq_one_iff]
-- Lean 4 proof step from Mathlib.Probability.Independence.ZeroOne (goal)
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
t : Set Ω
ht_tail : MeasurableSet t
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∞)
ht : MeasurableSet t
ω : Ω
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
⊢ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 0 ∨ Eq (α := ℝ) (μ[t.indicator fun (ω : Ω) ↦ 1 | m] ω) 1
have 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
Tactic: rwa [← hω_eq, measureReal_eq_zero_iff, measureReal_def, ENNReal.toReal_eq_one_iff]