minIndex_min

formal source

 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
 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₂