Exists elementary Predictable Set

theorem exists_elementaryPredictableSet (hσ : IsStoppingTime 𝓕 σ) (hτ : IsStoppingTime 𝓕 τ)    {n : ℕ} (hτn : ∀ ω, τ ω ≤ n) :    ∃ S : ElementaryPredictableSet 𝓕, (S : Set (ℕ × Ω)) = stochIoc σ τ := by  refine ⟨{    setBot := ∅    I := (Finset.range n).image (fun i ↦ (i, i + 1))    set := fun p ↦ {ω | σ ω ≤ (p.1 : ℕ∞) ∧ (p.1 : ℕ∞) < τ ω}    le_of_mem_I p hp := ?_    measurableSet_setBot := @MeasurableSet.empty _ (𝓕 ⊥)    measurableSet_set p hp := ?_    pairwiseDisjoint p hp q hq hpq := ?_ }, ?_⟩  · simp only [Finset.mem_image, Finset.mem_range] at hp    obtain ⟨i, _, rfl⟩ := hp    exact Nat.le_succ i  · simp only [Finset.mem_image, Finset.mem_range] at hp    obtain ⟨i, _, rfl⟩ := hp    exact measurableSet_slice hσ hτ i  · simp only [Finset.coe_image, Finset.coe_range, Set.mem_image, Set.mem_Iio] at hp hq    obtain ⟨i, _, rfl⟩ := hp    obtain ⟨j, _, rfl⟩ := hq    have hij : i ≠ j := fun h ↦ hpq (by rw [h])    apply Set.disjoint_left.mpr    rintro ⟨t, ω⟩ ht ht'    simp only [Set.mem_prod, Set.mem_Ioc] at ht ht'    lia  · rw [ElementaryPredictableSet.toSet]    simp only [Set.prod_empty, Set.empty_union]    rw [Finset.set_biUnion_finset_image, eq_iUnion σ τ]    ext ⟨t, ω⟩    simp only [Set.mem_iUnion, Finset.mem_range, Set.mem_prod, Set.mem_Ioc, Set.mem_ofPred_eq]    constructor    · grind    · rintro ⟨i, ht, hσi, hiτ⟩      refine ⟨i, ?_, ht, hσi, hiτ⟩      suffices (i : ℕ∞) < n by norm_cast at this      grind