-- 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:
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)

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

Result:
case inr.intro.intro.hm.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 η μα
a b c : β
hc : (fun x1 x2 => x1 ≤ x2) (ns a) (ns c) ∧ (fun x1 x2 => x1 ≤ x2) (ns b) (ns c)
⊢ ∃ 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 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
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
η : Kernel α Ω
η_eq : ⇑κ =ᶠ[ae μα] ⇑η
hη : IsMarkovKernel η
⊢ Indep (⨆ a, ⨆ n ∈ ns a, s n) (limsup s f) κ μα

Tactic:
replace h_indep := h_indep.congr η_eq

Result:
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) κ μα

Proof state:
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) η μα

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

Result:
no goals

Proof state:
case inr.intro.intro.hm.intro.refine_1
α : 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 a
⊢ n ∈ ns c

Tactic:
exact hc.1 hn

Result:
no goals

Proof state:
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

Tactic:
exact limsup_le_iSup.trans (iSup_le h_le)

Result:
no goals

Proof state:
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

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

Result:
no goals

Proof state:
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) κ μα

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

Result:
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
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
η : Kernel α Ω
η_eq : ⇑κ =ᶠ[ae μα] ⇑η
hη : IsMarkovKernel η
⊢ Indep (⨆ a, ⨆ n ∈ ns a, s n) (limsup s f) κ μα

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.congr (Filter.EventuallyEq.symm η_eq)

Result:
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) η μα