Generate From eq predictable

theorem generateFrom_eq_predictable [(Filter.atTop : Filter ι).IsCountablyGenerated] :    MeasurableSpace.generateFrom {↑S | S : ElementaryPredictableSet 𝓕} = 𝓕.predictable := by  apply le_antisymm  · apply MeasurableSpace.generateFrom_le    rintro _ ⟨S, rfl⟩    exact S.measurableSet_predictable  · apply measurableSpace_le_predictable_of_measurableSet    · intro B₀ hB₀      apply MeasurableSpace.measurableSet_generateFrom      use singletonBotProd hB₀, coe_singletonBotProd hB₀    · intro t B hB      obtain ⟨seq, _, tendsto⟩ := Filter.exists_seq_monotone_tendsto_atTop_atTop ι      have : Set.Ioi t = ⋃ n : ℕ, Set.Ioc t (seq n) := by        ext s        suffices ∃ n, s ≤ seq n by simpa using fun _ ↦ this        rw [Filter.tendsto_atTop_atTop] at tendsto        obtain ⟨n, h⟩ := tendsto s        exact ⟨n, h n le_rfl⟩      rw [this, Set.iUnion_prod_const]      refine MeasurableSet.iUnion fun n ↦ MeasurableSpace.measurableSet_generateFrom ?_      use IocProd t (seq n) hB, coe_IocProd _ _ hB