-- Mathlib/Probability/Independence/ZeroOne.lean
theorem condExp_zero_or_one_of_measurableSet_limsup [StandardBorelSpace Ω]
    (hm : m ≤ m0) [IsFiniteMeasure μ]
    (h_le : ∀ n, s n ≤ m0) (h_indep : iCondIndep m hm s μ)
    (hf : ∀ t, p t → tᶜ ∈ f) (hns : Directed (· ≤ ·) ns) (hnsp : ∀ a, p (ns a))
    (hns_univ : ∀ n, ∃ a, n ∈ ns a) {t : Set Ω} (ht_tail : MeasurableSet[limsup s f] t) :
    ∀ᵐ ω ∂μ, (μ⟦t | m⟧) ω = 0 ∨ (μ⟦t | m⟧) ω = 1

Proof state:
case h.inr
Ω : 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✝ : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
h✝ : ∀ᵐ (x : Ω) ∂μ, ((condExpKernel μ m) x) t = 0 ∨ ((condExpKernel μ m) x) t = 1
ht : MeasurableSet t
ω : Ω
hω_eq : (((condExpKernel μ m) ω) t).toReal = (μ[t.indicator fun ω => 1|m]) ω
h : ((condExpKernel μ m) ω) t = 1
⊢ (((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω) t = ⊤) ∨ ((condExpKernel μ m) ω) t = 1

Tactic:
exact Or.inr h

Result:
no goals

Proof state:
Ω : 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✝ : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
⊢ ∀ᵐ (ω : Ω) ∂μ, (μ[t.indicator fun ω => 1|m]) ω = 0 ∨ (μ[t.indicator fun ω => 1|m]) ω = 1

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)

Result:
Ω : 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✝ : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
h : ∀ᵐ (x : Ω) ∂μ, ((condExpKernel μ m) x) t = 0 ∨ ((condExpKernel μ m) x) t = 1
⊢ ∀ᵐ (ω : Ω) ∂μ, (μ[t.indicator fun ω => 1|m]) ω = 0 ∨ (μ[t.indicator fun ω => 1|m]) ω = 1

Proof state:
Ω : 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✝ : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
h : ∀ᵐ (x : Ω) ∂μ, ((condExpKernel μ m) x) t = 0 ∨ ((condExpKernel μ m) x) t = 1
ht : MeasurableSet t
⊢ ∀ᵐ (ω : Ω) ∂μ, (μ[t.indicator fun ω => 1|m]) ω = 0 ∨ (μ[t.indicator fun ω => 1|m]) ω = 1

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

Result:
case h
Ω : 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✝ : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
h : ∀ᵐ (x : Ω) ∂μ, ((condExpKernel μ m) x) t = 0 ∨ ((condExpKernel μ m) x) t = 1
ht : MeasurableSet t
ω : Ω
hω_eq : (((condExpKernel μ m) ω) t).toReal = (μ[t.indicator fun ω => 1|m]) ω
hω : ((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω) t = 1
⊢ (μ[t.indicator fun ω => 1|m]) ω = 0 ∨ (μ[t.indicator fun ω => 1|m]) ω = 1

Proof state:
Ω : 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✝ : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
h : ∀ᵐ (x : Ω) ∂μ, ((condExpKernel μ m) x) t = 0 ∨ ((condExpKernel μ m) x) t = 1
⊢ ∀ᵐ (ω : Ω) ∂μ, (μ[t.indicator fun ω => 1|m]) ω = 0 ∨ (μ[t.indicator fun ω => 1|m]) ω = 1

Tactic:
have ht : MeasurableSet t := limsup_le_iSup.trans (iSup_le h_le) t ht_tail

Result:
Ω : 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✝ : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
h : ∀ᵐ (x : Ω) ∂μ, ((condExpKernel μ m) x) t = 0 ∨ ((condExpKernel μ m) x) t = 1
ht : MeasurableSet t
⊢ ∀ᵐ (ω : Ω) ∂μ, (μ[t.indicator fun ω => 1|m]) ω = 0 ∨ (μ[t.indicator fun ω => 1|m]) ω = 1

Proof state:
case h
Ω : 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✝ : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
h : ∀ᵐ (x : Ω) ∂μ, ((condExpKernel μ m) x) t = 0 ∨ ((condExpKernel μ m) x) t = 1
ht : MeasurableSet t
ω : Ω
hω_eq : (((condExpKernel μ m) ω) t).toReal = (μ[t.indicator fun ω => 1|m]) ω
hω : ((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω) t = 1
⊢ (μ[t.indicator fun ω => 1|m]) ω = 0 ∨ (μ[t.indicator fun ω => 1|m]) ω = 1

Tactic:
rw [← hω_eq, ENNReal.toReal_eq_zero_iff, ENNReal.toReal_eq_one_iff]

Result:
case h
Ω : 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✝ : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
h : ∀ᵐ (x : Ω) ∂μ, ((condExpKernel μ m) x) t = 0 ∨ ((condExpKernel μ m) x) t = 1
ht : MeasurableSet t
ω : Ω
hω_eq : (((condExpKernel μ m) ω) t).toReal = (μ[t.indicator fun ω => 1|m]) ω
hω : ((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω) t = 1
⊢ (((condExpKernel μ m) ω) t = 0 ∨ ((condExpKernel μ m) ω) t = ⊤) ∨ ((condExpKernel μ m) ω) t = 1