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

State before:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
⊢ nextTime queue = some next → ∃ event, queue[0]? = some event ∧ time event.val ≥ next.val
Tactic:
intro h
State after:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
h : nextTime queue = some next
⊢ ∃ event, queue[0]? = some event ∧ time event.val ≥ next.val

State before:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
h : nextTime queue = some next
⊢ ∃ event, queue[0]? = some event ∧ time event.val ≥ next.val
Tactic:
unfold nextTime at h
State after:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
h :
  (match queue[0]? with
    | none => none
    | some nextEvent => some { val := time nextEvent.val, property := (_ : bound ≤ time nextEvent.val) }) =
    some next
⊢ ∃ event, queue[0]? = some event ∧ time event.val ≥ next.val

State before:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
h :
  (match queue[0]? with
    | none => none
    | some nextEvent => some { val := time nextEvent.val, property := (_ : bound ≤ time nextEvent.val) }) =
    some next
⊢ ∃ event, queue[0]? = some event ∧ time event.val ≥ next.val
Tactic:
split at h <;> simp at h
State after:
case h_2
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
x✝ : Option { e // bound ≤ time e }
nextEvent✝ : { e // bound ≤ time e }
heq✝ : queue[0]? = some nextEvent✝
h : { val := time nextEvent✝.val, property := (_ : bound ≤ time nextEvent✝.val) } = next
⊢ ∃ event, queue[0]? = some event ∧ time event.val ≥ next.val

State before:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
x✝ : Option { e // bound ≤ time e }
event : { e // bound ≤ time e }
h' : queue[0]? = some event
h : { val := time event.val, property := (_ : bound ≤ time event.val) } = next
⊢ ∃ event, queue[0]? = some event ∧ time event.val ≥ next.val
Tactic:
case _ event h' =>
  exists event
  apply And.intro h'
  simp [←h]
State after:
no goals

State before:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
x✝ : Option { e // bound ≤ time e }
event : { e // bound ≤ time e }
h' : queue[0]? = some event
h : { val := time event.val, property := (_ : bound ≤ time event.val) } = next
⊢ ∃ event, queue[0]? = some event ∧ time event.val ≥ next.val
Tactic:
exists event
State after:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
x✝ : Option { e // bound ≤ time e }
event : { e // bound ≤ time e }
h' : queue[0]? = some event
h : { val := time event.val, property := (_ : bound ≤ time event.val) } = next
⊢ queue[0]? = some event ∧ time event.val ≥ next.val

State before:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
x✝ : Option { e // bound ≤ time e }
event : { e // bound ≤ time e }
h' : queue[0]? = some event
h : { val := time event.val, property := (_ : bound ≤ time event.val) } = next
⊢ queue[0]? = some event ∧ time event.val ≥ next.val
Tactic:
apply And.intro h'
State after:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
x✝ : Option { e // bound ≤ time e }
event : { e // bound ≤ time e }
h' : queue[0]? = some event
h : { val := time event.val, property := (_ : bound ≤ time event.val) } = next
⊢ time event.val ≥ next.val

State before:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
x✝ : Option { e // bound ≤ time e }
event : { e // bound ≤ time e }
h' : queue[0]? = some event
h : { val := time event.val, property := (_ : bound ≤ time event.val) } = next
⊢ time event.val ≥ next.val
Tactic:
simp [←h]
State after:
no goals