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 α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : (↑p1 : Set ι) ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : (↑p2 : Set ι) ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : (i : ι) → Set Ω := fun (i : ι) ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
h_P_inter_1 :
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
      (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
a : α
h_P_inter :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
    (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
ha1 :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ p1, f1 i) : ℝ≥0∞)
    (∏ i ∈ p1, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f1 i) : ℝ≥0∞)
ha2 :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ p2, f2 i) : ℝ≥0∞)
    (∏ i ∈ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f2 i) : ℝ≥0∞)
h' : IsProbabilityMeasure.{u_2} (α := Ω) (m0 := _mΩ) ((κ : (a : α) → Measure Ω) a)
n : ι
h1 : n ∉ p1
h : n ∉ p2
⊢ (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (univ ∩ univ) = HMul.hMul (α := ℝ≥0∞) 1 1

Tactic:
simp only [measure_univ, one_mul, mul_one, Set.inter_univ, Set.univ_inter]

Premises used: Set.inter_univ, MeasureTheory.IsProbabilityMeasure.measure_univ, Set.univ_inter, mul_one, one_mul
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set (Set Ω)
S T : Set ι
h_indep : iIndepSets s κ μ
hST : Disjoint S T
t1 t2 : Set Ω
p1 : Finset ι
hp1 : (↑p1 : Set ι) ⊆ S
f1 : ι → Set Ω
ht1_m : ∀ x ∈ p1, f1 x ∈ s x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
p2 : Finset ι
hp2 : (↑p2 : Set ι) ⊆ T
f2 : ι → Set Ω
ht2_m : ∀ x ∈ p2, f2 x ∈ s x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
g : (i : ι) → Set Ω := fun (i : ι) ↦ (if i ∈ p1 then f1 i else univ) ∩ if i ∈ p2 then f2 i else univ
h_P_inter_1 :
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
      (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
a : α
h_P_inter :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) : ℝ≥0∞)
    (∏ n ∈ p1 ∪ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) : ℝ≥0∞)
ha1 :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ p1, f1 i) : ℝ≥0∞)
    (∏ i ∈ p1, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f1 i) : ℝ≥0∞)
ha2 :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋂ i ∈ p2, f2 i) : ℝ≥0∞)
    (∏ i ∈ p2, (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f2 i) : ℝ≥0∞)
h' : IsProbabilityMeasure.{u_2} (α := Ω) (m0 := _mΩ) ((κ : (a : α) → Measure Ω) a)
⊢ ∀ (n : ι),
    (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (g n) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        (if n ∈ p1 then (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f1 n) else 1 : ℝ≥0∞)
        (if n ∈ p2 then (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f2 n) else 1 : ℝ≥0∞)

Tactic:
have h_μg : ∀ n, κ a (g n) = (ite (n ∈ p1) (κ a (f1 n)) 1) * (ite (n ∈ p2) (κ a (f2 n)) 1) := by
    intro n
    dsimp only [g]
    split_ifs with h1 h2
    · exact absurd rfl (Set.disjoint_iff_forall_ne.mp hST (hp1 h1) (hp2 h2))
    all_goals simp only [measure_univ, one_mul, mul_one, Set.inter_univ, Set.univ_inter]
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
S T : Set ι
hST : Disjoint S T
inl :
  ∀ (hs : iIndepSet s κ 0),
    Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ 0
inr :
  ∀ (hμ : μ ≠ 0), Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ μ
⊢ Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ μ

Tactic:
rcases eq_or_ne μ 0 with rfl | hμ

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
S T : Set ι
hST : Disjoint S T
hs : iIndepSet s κ 0
⊢ Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ 0

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
⊢ ∃ (η : Kernel α Ω),
    Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω) ∧
      IsMarkovKernel η

Tactic:
exists_ae_eq_isMarkovKernel hs.ae_isProbabilityMeasure hμ

Premises used: ProbabilityTheory.Kernel.exists_ae_eq_isMarkovKernel, ProbabilityTheory.Kernel.iIndep.ae_isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
S T : Set ι
hST : Disjoint S T
hμ : μ ≠ 0
inr :
  ∀ (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η),
    Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ μ
⊢ Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ μ

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

Premises used: ProbabilityTheory.Kernel.exists_ae_eq_isMarkovKernel, ProbabilityTheory.Kernel.iIndep.ae_isProbabilityMeasure, ProbabilityTheory.Kernel
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
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 η
inr : Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) η μ
⊢ Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ μ

Tactic:
apply Indep.congr (Filter.EventuallyEq.symm η_eq)

Premises used: ProbabilityTheory.Kernel.Indep.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
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 η
inr :
  Indep (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) S)) (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) T)) η
    μ
⊢ Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) η μ

Tactic:
rw [← generateFrom_piiUnionInter_singleton_left, ← generateFrom_piiUnionInter_singleton_left]

Premises used: generateFrom_piiUnionInter_singleton_left
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
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 η
⊢ Indep (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) S)) (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) T)) η
    μ

Tactic:
IndepSets.indep'
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht))
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht)) ?_ ?_ ?_

Premises used: MeasurableSpace.measurableSet_generateFrom, generateFrom_piiUnionInter_le, ProbabilityTheory.Kernel.IndepSets.indep', Singleton.singleton
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
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 η
inr :
  ∀ (t : Set Ω) (ht : Membership.mem (γ := Set (Set Ω)) (piiUnionInter (fun (k : ι) ↦ {s k}) S) t) (n : ι),
    generateFrom {s n} ≤ _mΩ
inr₁ :
  ∀ (t : Set Ω) (ht : Membership.mem (γ := Set (Set Ω)) (piiUnionInter (fun (k : ι) ↦ {s k}) T) t) (n : ι),
    generateFrom {s n} ≤ _mΩ
inr₂ : IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (k : ι) ↦ {s k}) S)
inr₃ : IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (k : ι) ↦ {s k}) T)
inr₄ : IndepSets (piiUnionInter (fun (k : ι) ↦ {s k}) S) (piiUnionInter (fun (k : ι) ↦ {s k}) T) η μ
⊢ Indep (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) S)) (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) T)) η
    μ

Tactic:
refine
    IndepSets.indep'
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht))
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht)) ?_ ?_ ?_

Premises used: MeasurableSpace.measurableSet_generateFrom, generateFrom_piiUnionInter_le, ProbabilityTheory.Kernel.IndepSets.indep'
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
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 η
t : Set Ω
ht : Membership.mem (γ := Set (Set Ω)) (piiUnionInter (fun (k : ι) ↦ {s k}) S) t
⊢ ∀ (n : ι), generateFrom {s n} ≤ _mΩ

Tactic:
fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k

Premises used: Eq.rec, Set.mem_singleton_iff, Iff.mp, Eq.symm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
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 η
t : Set Ω
ht : Membership.mem (γ := Set (Set Ω)) (piiUnionInter (fun (k : ι) ↦ {s k}) S) t
⊢ ∀ (n : ι), generateFrom {s n} ≤ _mΩ

Tactic:
exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
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 η
t : Set Ω
ht : Membership.mem (γ := Set (Set Ω)) (piiUnionInter (fun (k : ι) ↦ {s k}) T) t
⊢ ∀ (n : ι), generateFrom {s n} ≤ _mΩ

Tactic:
fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k

Premises used: Eq.rec, Set.mem_singleton_iff, Iff.mp, Eq.symm, MeasurableSpace.generateFrom_le
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
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 η
t : Set Ω
ht : Membership.mem (γ := Set (Set Ω)) (piiUnionInter (fun (k : ι) ↦ {s k}) T) t
⊢ ∀ (n : ι), generateFrom {s n} ≤ _mΩ

Tactic:
exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k

Premises used: MeasurableSpace.generateFrom_le
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
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 (k : ι) ↦ {s k}) S)

Tactic:
isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _

Premises used: IsPiSystem.singleton, isPiSystem_piiUnionInter
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
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 (k : ι) ↦ {s k}) S)

Tactic:
exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _

Premises used: IsPiSystem.singleton, isPiSystem_piiUnionInter
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
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 (k : ι) ↦ {s k}) T)

Tactic:
isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _

Premises used: IsPiSystem.singleton, isPiSystem_piiUnionInter
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
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 (k : ι) ↦ {s k}) T)

Tactic:
exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _

Premises used: IsPiSystem.singleton, isPiSystem_piiUnionInter
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
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 (k : ι) ↦ {s k}) S) (piiUnionInter (fun (k : ι) ↦ {s k}) T) η μ

Tactic:
indepSets_piiUnionInter_of_disjoint (iIndep.iIndepSets (fun n => rfl) (hs.congr η_eq)) hST

Premises used: ProbabilityTheory.Kernel.iIndepSet.congr, ProbabilityTheory.Kernel.indepSets_piiUnionInter_of_disjoint, ProbabilityTheory.Kernel.iIndep.iIndepSets, rfl
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s κ μ
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 (k : ι) ↦ {s k}) S) (piiUnionInter (fun (k : ι) ↦ {s k}) T) η μ

Tactic:
exact indepSets_piiUnionInter_of_disjoint (iIndep.iIndepSets (fun n => rfl) (hs.congr η_eq)) hST

Premises used: ProbabilityTheory.Kernel.iIndepSet.congr, ProbabilityTheory.Kernel.indepSets_piiUnionInter_of_disjoint, ProbabilityTheory.Kernel.iIndep.iIndepSets, rfl
-- 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
inl : ∀ (h_indep : iIndep m κ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ 0
inr : ∀ (hμ : μ ≠ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ

Tactic:
rcases eq_or_ne μ 0 with rfl | hμ

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Probability.Independence.Kernel.Indep
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
m : ι → MeasurableSpace Ω
h_le : ∀ (i : ι), m i ≤ _mΩ
S T : Set ι
hST : Disjoint S T
h_indep : iIndep m κ 0
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ 0

Tactic:
simp
-- 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 α Ω),
    Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω) ∧
      IsMarkovKernel η

Tactic:
exists_ae_eq_isMarkovKernel h_indep.ae_isProbabilityMeasure hμ

Premises used: ProbabilityTheory.Kernel.exists_ae_eq_isMarkovKernel, ProbabilityTheory.Kernel.iIndep.ae_isProbabilityMeasure
-- 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
inr :
  ∀ (η : Kernel α Ω)
    (η_eq :
      Filter.EventuallyEq.{u_1, u_2} (β := Measure Ω) (ae μ) (⇑κ : (a : α) → Measure Ω) (⇑η : (a : α) → Measure Ω))
    (hη : IsMarkovKernel η), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ

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

Premises used: ProbabilityTheory.Kernel.exists_ae_eq_isMarkovKernel, ProbabilityTheory.Kernel.iIndep.ae_isProbabilityMeasure, ProbabilityTheory.Kernel
-- 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 η
inr : Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) η μ
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ

Tactic:
apply Indep.congr (Filter.EventuallyEq.symm η_eq)

Premises used: ProbabilityTheory.Kernel.Indep.congr, Filter.EventuallyEq.symm
-- 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 η
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) η μ

Tactic:
IndepSets.indep (iSup₂_le fun i _ => h_le i) (iSup₂_le fun i _ => h_le i) ?_ ?_
      (generateFrom_piiUnionInter_measurableSet m S).symm
      (generateFrom_piiUnionInter_measurableSet m T).symm ?_

Premises used: iSup₂_le, generateFrom_piiUnionInter_measurableSet, ProbabilityTheory.Kernel.IndepSets.indep, Eq.symm
-- 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 η
inr : IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) S)
inr₁ : IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) T)
inr₂ :
  IndepSets (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) S)
    (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) T) η μ
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) η μ

Tactic:
refine
    IndepSets.indep (iSup₂_le fun i _ => h_le i) (iSup₂_le fun i _ => h_le i) ?_ ?_
      (generateFrom_piiUnionInter_measurableSet m S).symm
      (generateFrom_piiUnionInter_measurableSet m T).symm ?_

Premises used: iSup₂_le, generateFrom_piiUnionInter_measurableSet, ProbabilityTheory.Kernel.IndepSets.indep, Eq.symm
-- 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:
isPiSystem_piiUnionInter _ (fun n => @isPiSystem_measurableSet Ω (m n)) _

Premises used: MeasurableSpace.isPiSystem_measurableSet, isPiSystem_piiUnionInter