chooseCandidate_some_spec

formal source

 354  · simp [h]
 355  · simp [h]
 356
 357lemma chooseCandidate_some_spec {picked : Finset E.Event}
 358    {c : Candidate (ev:=ev) (E:=E) picked}
 359    (h : chooseCandidate (ev:=ev) (E:=E) picked = some c) :
 360    c.not_mem ∧ eligible (ev:=ev) picked c.event := by
 361  classical
 362  unfold chooseCandidate at h
 363  split_ifs at h with hExists
 364  · rcases h with ⟨⟩
 365    simp
 366  · cases h
 367
 368/-- Minimal index (in the fixed enumeration `enum`) where an event appears. -/
 369noncomputable def minIndex (e : E.Event) : ℕ :=
 370  Nat.find (enum_surjective (E:=E) e)
 371
 372lemma minIndex_spec (e : E.Event) : enum (E:=E) (minIndex (E:=E) e) = e := by
 373  classical
 374  unfold minIndex
 375  exact Nat.find_spec (enum_surjective (E:=E) e)
 376
 377lemma minIndex_min (e : E.Event) {n : ℕ} (h : enum (E:=E) n = e) :
 378    minIndex (E:=E) e ≤ n := by
 379  classical
 380  unfold minIndex
 381  exact Nat.find_min' (enum_surjective (E:=E) e) h
 382
 383/-- A canonical countable schedule derived from `minIndex`. Each event appears
 384    exactly once at its minimal enumeration index. -/
 385noncomputable def scheduleByMinIndex : CountableSchedule E.Event :=
 386{ postAt := fun n =>
 387    if h : ∃ e : E.Event, minIndex (E:=E) e = n then