-- Mathlib/Probability/Independence/Kernel.lean
theorem indep_iSup_of_directed_le {Ω} {m : ι → MeasurableSpace Ω} {m' m0 : MeasurableSpace Ω}
    {κ : Kernel α Ω} {μ : Measure α} [IsZeroOrMarkovKernel κ] (h_indep : ∀ i, Indep (m i) m' κ μ)
    (h_le : ∀ i, m i ≤ m0) (h_le' : m' ≤ m0) (hm : Directed (· ≤ ·) m) :
    Indep (⨆ i, m i) m' κ μ

Proof state:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x1 x2 => x1 ≤ x2) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ n, p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ Indep (⨆ i, m i) m' κ μ

Tactic:
have h_pi_system_indep : IndepSets (⋃ n, p n) p' κ μ := by
  refine IndepSets.iUnion ?_
  conv at h_indep =>
    intro i
    rw [h_gen_n i, h_gen']
  exact fun n => (h_indep n).indepSets

Result:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x1 x2 => x1 ≤ x2) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ n, p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
h_pi_system_indep : IndepSets (⋃ n, p n) p' κ μ
⊢ Indep (⨆ i, m i) m' κ μ

Proof state:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x1 x2 => x1 ≤ x2) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ n, p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ ∀ (n : ι), IndepSets (p n) p' κ μ

Tactic:
conv at h_indep =>
  intro i
  rw [h_gen_n i, h_gen']

Result:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x1 x2 => x1 ≤ x2) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ n, p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
h_indep : ∀ (i : ι), Indep (generateFrom (p i)) (generateFrom p') κ μ
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ ∀ (n : ι), IndepSets (p n) p' κ μ

Proof state:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x1 x2 => x1 ≤ x2) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ n, p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
⊢ Indep (⨆ i, m i) m' κ μ

Tactic:
have h_gen' : m' = generateFrom p' := (@generateFrom_measurableSet Ω m').symm

Result:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x1 x2 => x1 ≤ x2) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ n, p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ Indep (⨆ i, m i) m' κ μ

Proof state:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x1 x2 => x1 ≤ x2) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ n, p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
h_pi_system_indep : IndepSets (⋃ n, p n) p' κ μ
⊢ Indep (⨆ i, m i) m' κ μ

Tactic:
refine IndepSets.indep (iSup_le h_le) h_le' hp_supr_pi hp'_pi ?_ h_gen' h_pi_system_indep

Result:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x1 x2 => x1 ≤ x2) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ n, p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
h_pi_system_indep : IndepSets (⋃ n, p n) p' κ μ
⊢ ⨆ i, m i = generateFrom (⋃ n, p n)

Proof state:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x1 x2 => x1 ≤ x2) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ n, p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ IndepSets (⋃ n, p n) p' κ μ

Tactic:
refine IndepSets.iUnion ?_

Result:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Directed (fun x1 x2 => x1 ≤ x2) m
p : ι → Set (Set Ω) := fun n => {t | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem (⋃ n, p n)
p' : Set (Set Ω) := {t | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ ∀ (n : ι), IndepSets (p n) p' κ μ