 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
 388      some (Classical.choose h)
 389    else none
 390, nodup := by
 391    intro n₁ n₂ e h₁ h₂
 392    classical
 393    unfold scheduleByMinIndex at h₁ h₂
 394    simp only at h₁ h₂
 395    rcases Classical.decEq (∃ e, minIndex (E:=E) e = n₁) with hdec₁ | hdec₁
 396    · simp [scheduleByMinIndex._match_1, hdec₁] at h₁
 397    · rcases h₁
 398    rcases Classical.decEq (∃ e, minIndex (E:=E) e = n₂) with hdec₂ | hdec₂
 399    · simp [scheduleByMinIndex._match_1, hdec₂] at h₂
 400    · rcases h₂
 401    -- In the `some` branches on both sides
 402    have hsome₁ : ∃ e, minIndex (E:=E) e = n₁ := by
 403      by_contra H; simp [scheduleByMinIndex._match_1, H] at h₁
 404    have hsome₂ : ∃ e, minIndex (E:=E) e = n₂ := by
 405      by_contra H; simp [scheduleByMinIndex._match_1, H] at h₂
 406    let e₁ := Classical.choose hsome₁
 407    let e₂ := Classical.choose hsome₂
 408    have he₁ : minIndex (E:=E) e₁ = n₁ := (Classical.choose_spec hsome₁)
 409    have he₂ : minIndex (E:=E) e₂ = n₂ := (Classical.choose_spec hsome₂)
 410    -- The `some` payloads must coincide with `e`
 411    have : e₁ = e := by
 412      have : some e₁ = some e := by simpa [scheduleByMinIndex._match_1, he₁] using h₁
 413      exact by cases this; rfl
 414    have : e₂ = e := by
 415      have : some e₂ = some e := by simpa [scheduleByMinIndex._match_1, he₂] using h₂

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.