case h.e'_2.h.e'_2
Ω : Type u_2
ι : Type u_1
m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝¹ : Preorder ι
inst✝ : IsProbabilityMeasure μ
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
i : ι
⊢ {s i} = {t | ∃ n, n ∈ {i} ∧ s n = t}
Ω : Type u_2
ι : Type u_1
m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝¹ : Preorder ι
inst✝ : IsProbabilityMeasure μ
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
i : ι
⊢ Indep (generateFrom {s i}) (generateFrom {t | ∃ j, j < i ∧ s j = t})
convert iIndepSet.indep_generateFrom_of_disjoint hsm hs {i} { j | j < i }
  (Set.disjoint_singleton_left.mpr (lt_irrefl _))
no goals
case h.e'_2.h.e'_2
Ω : Type u_2
ι : Type u_1
m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝¹ : Preorder ι
inst✝ : IsProbabilityMeasure μ
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
i : ι
⊢ {s i} = {t | ∃ n, n ∈ {i} ∧ s n = t}
simp only [Set.mem_singleton_iff, exists_prop, exists_eq_left, Set.setOf_eq_eq_singleton']