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