-- Mathlib/Probability/Independence/ZeroOne.lean
theorem Kernel.indep_iSup_directed_limsup (h_le : ∀ n, s n ≤ m0) (h_indep : iIndep s κ μα)
    (hf : ∀ t, p t → tᶜ ∈ f) (hns : Directed (· ≤ ·) ns) (hnsp : ∀ a, p (ns a)) :
    Indep (⨆ a, ⨆ n ∈ ns a, s n) (limsup s f) κ μα

Proof state:
α : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
⊢ Indep (⨆ a, ⨆ n ∈ ns a, s n) (limsup s f) κ μα

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

Result:
case inl
α : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
h_indep : iIndep s κ 0
⊢ Indep (⨆ a, ⨆ n ∈ ns a, s n) (limsup s f) κ 0

case inr
α : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
⊢ Indep (⨆ a, ⨆ n ∈ ns a, s n) (limsup s f) κ μα

Proof state:
case inr.intro.intro.hm.intro.refine_2
α : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᶠ[ae μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
a b c : β
hc : (fun x1 x2 => x1 ≤ x2) (ns a) (ns c) ∧ (fun x1 x2 => x1 ≤ x2) (ns b) (ns c)
n : ι
hn : n ∈ ns b
⊢ n ∈ ns c

Tactic:
exact hc.2 hn

Result:
no goals

Proof state:
case inr.intro.intro.hm
α : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᶠ[ae μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
⊢ Directed (fun x1 x2 => x1 ≤ x2) fun i => ⨆ n ∈ ns i, s n

Tactic:
intro a b

Result:
case inr.intro.intro.hm
α : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᶠ[ae μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
a b : β
⊢ ∃ z,
    (fun x1 x2 => x1 ≤ x2) ((fun i => ⨆ n ∈ ns i, s n) a) ((fun i => ⨆ n ∈ ns i, s n) z) ∧
      (fun x1 x2 => x1 ≤ x2) ((fun i => ⨆ n ∈ ns i, s n) b) ((fun i => ⨆ n ∈ ns i, s n) z)

Proof state:
case inl
α : 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 => 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

Result:
no goals

Proof state:
case inr.intro.intro
α : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᶠ[ae μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
⊢ Indep (⨆ a, ⨆ n ∈ ns a, s n) (limsup s f) η μα

Tactic:
apply indep_iSup_of_directed_le

Result:
case inr.intro.intro.h_indep
α : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᶠ[ae μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
⊢ ∀ (i : β), Indep (⨆ n ∈ ns i, s n) (limsup s f) η μα

case inr.intro.intro.h_le
α : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᶠ[ae μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
⊢ ∀ (i : β), ⨆ n ∈ ns i, s n ≤ m0

case inr.intro.intro.h_le'
α : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᶠ[ae μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
⊢ limsup s f ≤ m0

case inr.intro.intro.hm
α : 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 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᶠ[ae μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
⊢ Directed (fun x1 x2 => x1 ≤ x2) fun i => ⨆ n ∈ ns i, s n