lemma
proved
tactic proof
chooseCandidate_some_spec
show as:
view Lean formalization →
formal statement (Lean)
357lemma chooseCandidate_some_spec {picked : Finset E.Event}
358 {c : Candidate (ev:=ev) (E:=E) picked}
proof body
Tactic-mode proof.
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. -/