awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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)) η
    μ
have inr : ∀ (t : Set Ω) (ht : Membership.mem (γ := Set (Set Ω)) (piiUnionInter (fun (k : ι) ↦ {s k}) S) t) (n : ι),
  generateFrom {s n} ≤ _mΩ
Tactic: refine
    IndepSets.indep'
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht))
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht)) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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Ω
⊢ Indep (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) S)) (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) T)) η
    μ
have inr₁ : ∀ (t : Set Ω) (ht : Membership.mem (γ := Set (Set Ω)) (piiUnionInter (fun (k : ι) ↦ {s k}) T) t) (n : ι),
  generateFrom {s n} ≤ _mΩ
Tactic: refine
    IndepSets.indep'
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht))
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht)) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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Ω
⊢ Indep (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) S)) (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) T)) η
    μ
have inr₂ : IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (k : ι) ↦ {s k}) S)
Tactic: refine
    IndepSets.indep'
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht))
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht)) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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)
⊢ Indep (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) S)) (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) T)) η
    μ
have inr₃ : IsPiSystem.{u_2} (α := Ω) (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)) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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)
⊢ Indep (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) S)) (generateFrom (piiUnionInter (fun (k : ι) ↦ {s k}) T)) η
    μ
have inr₄ : IndepSets (piiUnionInter (fun (k : ι) ↦ {s k}) S) (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)) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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
⊢ Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ μ
have inl : ∀ (hs : iIndepSet s κ 0),
  Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ 0
Tactic: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel hs.ae_isProbabilityMeasure hμ
  apply Indep.congr (Filter.EventuallyEq.symm η_eq)
  rw [← generateFrom_piiUnionInter_singleton_left, ← generateFrom_piiUnionInter_singleton_left]
  refine
    IndepSets.indep'
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht))
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht)) ?_ ?_ ?_
  · exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k
  · exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k
  · exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _
  · exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _
  · exact indepSets_piiUnionInter_of_disjoint (iIndep.iIndepSets (fun n => rfl) (hs.congr η_eq)) hST
Cleared hypotheses: μ, hs
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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
⊢ Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ μ
have inr : ∀ (hμ : μ ≠ 0), Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ μ
Tactic: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel hs.ae_isProbabilityMeasure hμ
  apply Indep.congr (Filter.EventuallyEq.symm η_eq)
  rw [← generateFrom_piiUnionInter_singleton_left, ← generateFrom_piiUnionInter_singleton_left]
  refine
    IndepSets.indep'
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht))
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht)) ?_ ?_ ?_
  · exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k
  · exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k
  · exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _
  · exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _
  · exact indepSets_piiUnionInter_of_disjoint (iIndep.iIndepSets (fun n => rfl) (hs.congr η_eq)) hST
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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 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}) κ μ
have inr₂ : ∀ (hμ : μ ≠ 0) (η : 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}) κ μ
Tactic: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel hs.ae_isProbabilityMeasure hμ
  apply Indep.congr (Filter.EventuallyEq.symm η_eq)
  rw [← generateFrom_piiUnionInter_singleton_left, ← generateFrom_piiUnionInter_singleton_left]
  refine
    IndepSets.indep'
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht))
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht)) ?_ ?_ ?_
  · exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k
  · exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k
  · exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _
  · exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _
  · exact indepSets_piiUnionInter_of_disjoint (iIndep.iIndepSets (fun n => rfl) (hs.congr η_eq)) hST
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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 inr₁ :
  ∀ (hμ : μ ≠ 0), Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ μ
inr₂ :
  ∀ (hμ : μ ≠ 0) (η : 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}) κ μ
have inr₃ : ∀ (hμ : μ ≠ 0) (η : 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}) η μ
Tactic: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel hs.ae_isProbabilityMeasure hμ
  apply Indep.congr (Filter.EventuallyEq.symm η_eq)
  rw [← generateFrom_piiUnionInter_singleton_left, ← generateFrom_piiUnionInter_singleton_left]
  refine
    IndepSets.indep'
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht))
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht)) ?_ ?_ ?_
  · exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k
  · exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k
  · exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _
  · exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _
  · exact indepSets_piiUnionInter_of_disjoint (iIndep.iIndepSets (fun n => rfl) (hs.congr η_eq)) hST
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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 inr₁ :
  ∀ (hμ : μ ≠ 0), Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ μ
inr₂ :
  ∀ (hμ : μ ≠ 0) (η : 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}) κ μ
inr₃ :
  ∀ (hμ : μ ≠ 0) (η : 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}) κ μ
have inr₄ : ∀ (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: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel hs.ae_isProbabilityMeasure hμ
  apply Indep.congr (Filter.EventuallyEq.symm η_eq)
  rw [← generateFrom_piiUnionInter_singleton_left, ← generateFrom_piiUnionInter_singleton_left]
  refine
    IndepSets.indep'
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht))
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht)) ?_ ?_ ?_
  · exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k
  · exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k
  · exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _
  · exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _
  · exact indepSets_piiUnionInter_of_disjoint (iIndep.iIndepSets (fun n => rfl) (hs.congr η_eq)) hST
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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 inr₁ :
  ∀ (hμ : μ ≠ 0), Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ μ
inr₂ :
  ∀ (hμ : μ ≠ 0) (η : 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}) κ μ
inr₃ :
  ∀ (hμ : μ ≠ 0) (η : 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}) η μ
inr₄ :
  ∀ (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))
      η μ
⊢ Indep (generateFrom {t : Set Ω | ∃ n ∈ S, s n = t}) (generateFrom {t : Set Ω | ∃ k ∈ T, s k = t}) κ μ
have inr₅ : ∀ (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: classical
  rcases eq_or_ne μ 0 with rfl | hμ
  · simp
  obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel hs.ae_isProbabilityMeasure hμ
  apply Indep.congr (Filter.EventuallyEq.symm η_eq)
  rw [← generateFrom_piiUnionInter_singleton_left, ← generateFrom_piiUnionInter_singleton_left]
  refine
    IndepSets.indep'
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht))
      (fun t ht => generateFrom_piiUnionInter_le _ ?_ _ _ (measurableSet_generateFrom ht)) ?_ ?_ ?_
  · exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k
  · exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k
  · exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _
  · exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _
  · exact indepSets_piiUnionInter_of_disjoint (iIndep.iIndepSets (fun n => rfl) (hs.congr η_eq)) hST
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
have inl : ∀ (h_indep : iIndep m κ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ 0
Tactic: rcases eq_or_ne μ 0 with rfl | hμ
Cleared hypotheses: μ, h_indep
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
have inr : ∀ (hμ : μ ≠ 0), Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
Tactic: rcases eq_or_ne μ 0 with rfl | hμ
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
have 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) κ μ
Tactic: obtain ⟨η, η_eq, hη⟩ : ∃ (η : Kernel α Ω), κ =ᵐ[μ] η ∧ IsMarkovKernel η :=
    exists_ae_eq_isMarkovKernel h_indep.ae_isProbabilityMeasure hμ
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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) κ μ
have inr : Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) η μ
Tactic: apply Indep.congr (Filter.EventuallyEq.symm η_eq)
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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) η μ
have inr : IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) S)
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 ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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)
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) η μ
have inr₁ : IsPiSystem.{u_2} (α := Ω) (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) T)
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 ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Kernel.Indep (goal)
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)
⊢ Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) η μ
have inr₂ : IndepSets (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) S)
  (piiUnionInter (fun (n : ι) ↦ {s : Set Ω | MeasurableSet s}) T) η μ
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 ?_