Theorem: Queue.nextTime_isSome_iff_not_isEmpty (Runtime/Utilities/Queue.lean)

State before:
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
⊢ Option.isSome (nextTime queue) = true ↔ ¬isEmpty queue = true
Tactic:
rw [Queue.isEmpty, ←Array.getElem?_zero_isSome_iff_not_isEmpty]
State after:
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
⊢ Option.isSome (nextTime queue) = true ↔ Option.isSome queue.events[0]? = true

State before:
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
⊢ Option.isSome (nextTime queue) = true ↔ Option.isSome queue.events[0]? = true
Tactic:
simp [nextTime]
State after:
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
⊢ Option.isSome
        (match queue[0]? with
        | none => none
        | some nextEvent => some { val := time nextEvent.val, property := (_ : bound ≤ time nextEvent.val) }) =
      true ↔
    Option.isSome queue.events[0]? = true

State before:
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
⊢ Option.isSome
        (match queue[0]? with
        | none => none
        | some nextEvent => some { val := time nextEvent.val, property := (_ : bound ≤ time nextEvent.val) }) =
      true ↔
    Option.isSome queue.events[0]? = true
Tactic:
constructor <;> split <;> simp_all [Option.isSome]
State after:
case mp.h_2
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
x✝ : Option { e // bound ≤ time e }
nextEvent✝ : { e // bound ≤ time e }
heq✝ : queue[0]? = some nextEvent✝
⊢ (match queue.events[0]? with
    | some val => true
    | none => false) =
    true