awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
⊢ IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) S)

Tactic:
exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _

Premises used: MeasurableSpace.isPiSystem_measurableSet, isPiSystem_piiUnionInter
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
⊢ IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) T)

Tactic:
isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _

Premises used: MeasurableSpace.isPiSystem_measurableSet, isPiSystem_piiUnionInter
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
⊢ IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) T)

Tactic:
exact isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _

Premises used: MeasurableSpace.isPiSystem_measurableSet, isPiSystem_piiUnionInter
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
⊢ IndepSets (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) S)
    (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) T) η μ

Tactic:
indepSets_piiUnionInter_of_disjoint (h_indep.congr η_eq) hST

Premises used: ProbabilityTheory.Kernel.iIndep.congr, ProbabilityTheory.Kernel.indepSets_piiUnionInter_of_disjoint
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
h_indep : iIndep m κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω)
hη : IsMarkovKernel η
⊢ IndepSets (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) S)
    (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) T) η μ

Tactic:
exact indepSets_piiUnionInter_of_disjoint (h_indep.congr η_eq) hST

Premises used: ProbabilityTheory.Kernel.iIndep.congr, ProbabilityTheory.Kernel.indepSets_piiUnionInter_of_disjoint
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
⊢ ∀ (n : ι), IsPiSystem (p n)

Tactic:
have hp : ∀ n, IsPiSystem (p n) := fun n => @isPiSystem_measurableSet Ω (m n)
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
⊢ ∀ (n : ι), m n = generateFrom (p n)

Tactic:
have h_gen_n : ∀ n, m n = generateFrom (p n) := fun n =>
    (@generateFrom_measurableSet Ω (m n)).symm
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
⊢ IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)

Tactic:
have hp_supr_pi : IsPiSystem (⋃ n, p n) := isPiSystem_iUnion_of_directed_le p hp hm
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
⊢ IsPiSystem p'

Tactic:
have hp'_pi : IsPiSystem p' := @isPiSystem_measurableSet Ω m'
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
hp'_pi : IsPiSystem p'
⊢ m' = generateFrom p'

Tactic:
have h_gen' : m' = generateFrom p' := (@generateFrom_measurableSet Ω m').symm
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ IndepSets (⋃ (n : ι), p n) p' κ μ

Tactic:
IndepSets.iUnion ?_

Premises used: ProbabilityTheory.Kernel.IndepSets.iUnion
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
refine : ∀ (n : ι), IndepSets (p n) p' κ μ
⊢ IndepSets (⋃ (n : ι), p n) p' κ μ

Tactic:
refine IndepSets.iUnion ?_

Premises used: ProbabilityTheory.Kernel.IndepSets.iUnion
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
i : ι
rw : Indep (generateFrom (p i)) (generateFrom p') κ μ
| Indep (m i) m' κ μ

Tactic:
rw [h_gen_n i, h_gen']
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ ∀ (i : ι), Indep (generateFrom (p i)) (generateFrom p') κ μ

Tactic:
conv at h_indep =>
      intro i
      rw [h_gen_n i, h_gen']
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
h_indep₁ : ∀ (i : ι), Indep (generateFrom (p i)) (generateFrom p') κ μ
⊢ IsPiSystem p'

Tactic:
conv at h_indep =>
      intro i
      rw [h_gen_n i, h_gen']
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
h_indep₁ : ∀ (i : ι), Indep (generateFrom (p i)) (generateFrom p') κ μ
hp'_pi₁ : IsPiSystem p'
⊢ m' = generateFrom p'

Tactic:
conv at h_indep =>
      intro i
      rw [h_gen_n i, h_gen']
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | 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' κ μ

Tactic:
fun n => (h_indep n).indepSets

Premises used: ProbabilityTheory.Kernel.Indep.indepSets
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | 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' κ μ

Tactic:
exact fun n => (h_indep n).indepSets

Premises used: ProbabilityTheory.Kernel.Indep.indepSets
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
⊢ IndepSets (⋃ (n : ι), p n) p' κ μ

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
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | 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:
IndepSets.indep (iSup_le h_le) h_le' hp_supr_pi hp'_pi ?_ h_gen' h_pi_system_indep

Premises used: iSup_le, ProbabilityTheory.Kernel.IndepSets.indep
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
h_pi_system_indep : IndepSets (⋃ (n : ι), p n) p' κ μ
refine : Eq.{u_4 + 1} (α := MeasurableSpace Ω) (⨆ (i : ι), m i) (generateFrom (⋃ (n : ι), p n))
⊢ 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

Premises used: iSup_le, ProbabilityTheory.Kernel.IndepSets.indep
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
h_pi_system_indep : IndepSets (⋃ (n : ι), p n) p' κ μ
⊢ Eq.{u_4 + 1} (α := MeasurableSpace Ω) (⨆ (i : ι), m i) (generateFrom (⋃ (n : ι), p n))

Tactic:
(generateFrom_iUnion_measurableSet _).symm

Premises used: MeasurableSpace.generateFrom_iUnion_measurableSet, setOf, Eq.symm
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : 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 : MeasurableSpace Ω) ↦ x1 ≤ x2) m
p : ι → Set (Set Ω) := fun (n : ι) ↦ {t : Set Ω | MeasurableSet t}
hp : ∀ (n : ι), IsPiSystem (p n)
h_gen_n : ∀ (n : ι), m n = generateFrom (p n)
hp_supr_pi : IsPiSystem.{u_4} (α := Ω) (⋃ (n : ι), p n)
p' : Set (Set Ω) := {t : Set Ω | MeasurableSet t}
hp'_pi : IsPiSystem p'
h_gen' : m' = generateFrom p'
h_pi_system_indep : IndepSets (⋃ (n : ι), p n) p' κ μ
⊢ Eq.{u_4 + 1} (α := MeasurableSpace Ω) (⨆ (i : ι), m i) (generateFrom (⋃ (n : ι), p n))

Tactic:
exact (generateFrom_iUnion_measurableSet _).symm

Premises used: MeasurableSpace.generateFrom_iUnion_measurableSet, Eq.symm
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Preorder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
i : ι
⊢ Indep (generateFrom {t : Set Ω | ∃ (n : ι), Membership.mem (γ := Set ι) {i} n ∧ s n = t})
    (generateFrom {t : Set Ω | ∃ (k : ι), Membership.mem (γ := Set ι) {j : ι | j < i} k ∧ s k = t}) κ μ

Tactic:
iIndepSet.indep_generateFrom_of_disjoint hsm hs { i } {j | j < i}
      (Set.disjoint_singleton_left.mpr (lt_irrefl _))

Premises used: Iff.mpr, ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_of_disjoint, lt_irrefl, Set.disjoint_singleton_left, setOf, LT.lt, Singleton.singleton
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Preorder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
i : ι
h :
  Eq (α := MeasurableSpace Ω) (generateFrom {s i})
    (generateFrom {t : Set Ω | ∃ (n : ι), Membership.mem (γ := Set ι) {i} n ∧ s n = t})
⊢ Indep (generateFrom {s i}) (generateFrom {t : Set Ω | ∃ j < i, s j = t}) κ μ

Tactic:
convert!
    iIndepSet.indep_generateFrom_of_disjoint hsm hs { i } {j | j < i}
      (Set.disjoint_singleton_left.mpr (lt_irrefl _)) using 1

Premises used: Iff.mpr, ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_of_disjoint, lt_irrefl, Set.disjoint_singleton_left, setOf, LT.lt, Singleton.singleton
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Preorder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
i : ι
⊢ Eq (α := MeasurableSpace Ω) (generateFrom {s i})
    (generateFrom {t : Set Ω | ∃ (n : ι), Membership.mem (γ := Set ι) {i} n ∧ s n = t})

Tactic:
simp only [Set.mem_singleton_iff, exists_eq_left, Set.setOf_eq_eq_singleton']

Premises used: Set.setOf_eq_eq_singleton', exists_eq_left, Set.mem_singleton_iff
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Preorder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
i k : ι
hk : i < k
⊢ Indep (generateFrom {t : Set Ω | ∃ (n : ι), Membership.mem (γ := Set ι) {k} n ∧ s n = t})
    (generateFrom {t : Set Ω | ∃ (k : ι), Membership.mem (γ := Set ι) {j : ι | j ≤ i} k ∧ s k = t}) κ μ

Tactic:
iIndepSet.indep_generateFrom_of_disjoint hsm hs { k } {j | j ≤ i}
      (Set.disjoint_singleton_left.mpr hk.not_ge)

Premises used: Iff.mpr, ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_of_disjoint, Set.disjoint_singleton_left, setOf, LE.le, LT.lt.not_ge, Singleton.singleton
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Preorder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
i k : ι
hk : i < k
h :
  Eq (α := MeasurableSpace Ω) (generateFrom {s k})
    (generateFrom {t : Set Ω | ∃ (n : ι), Membership.mem (γ := Set ι) {k} n ∧ s n = t})
⊢ Indep (generateFrom {s k}) (generateFrom {t : Set Ω | ∃ j ≤ i, s j = t}) κ μ

Tactic:
convert!
    iIndepSet.indep_generateFrom_of_disjoint hsm hs { k } {j | j ≤ i}
      (Set.disjoint_singleton_left.mpr hk.not_ge) using 1

Premises used: Iff.mpr, ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_of_disjoint, Set.disjoint_singleton_left, setOf, LE.le, LT.lt.not_ge, Singleton.singleton
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Preorder ι
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
i k : ι
hk : i < k
⊢ Eq (α := MeasurableSpace Ω) (generateFrom {s k})
    (generateFrom {t : Set Ω | ∃ (n : ι), Membership.mem (γ := Set ι) {k} n ∧ s n = t})

Tactic:
simp only [Set.mem_singleton_iff, exists_eq_left, Set.setOf_eq_eq_singleton']

Premises used: Set.setOf_eq_eq_singleton', exists_eq_left, Set.mem_singleton_iff
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ℕ → Set Ω
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : iIndepSet s κ μ
n : ℕ
⊢ Indep (generateFrom {s (n + 1)}) (generateFrom {t : Set Ω | ∃ k ≤ n, s k = t}) κ μ

Tactic:
iIndepSet.indep_generateFrom_le hsm hs _ n.lt_succ_self

Premises used: ProbabilityTheory.Kernel.iIndepSet.indep_generateFrom_le, setOf, Nat.lt_succ_self
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
ι : Type u_3
_mα : MeasurableSpace α
inst : SemilatticeSup ι
Ω : Type u_4
m : ι → MeasurableSpace Ω
m' m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst_1 : IsZeroOrMarkovKernel κ
h_indep : ∀ (i : ι), Indep (m i) m' κ μ
h_le : ∀ (i : ι), m i ≤ m0
h_le' : m' ≤ m0
hm : Monotone m
⊢ Indep (⨆ (i : ι), m i) m' κ μ

Tactic:
indep_iSup_of_directed_le h_indep h_le h_le' (Monotone.directed_le hm)

Premises used: ProbabilityTheory.Kernel.indep_iSup_of_directed_le, Monotone.directed_le