Theorem: Queue.merge_mem₂
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝¹ : ¬isEmpty queue₁ = true
h✝ : ¬isEmpty queue₂ = true
⊢ event ∈
    {
      events :=
        merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
            (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
          merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
            (Array.split queue₂.events fun x => decide (time x = bound)).snd,
      sorted :=
        (_ :
          Sorted
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                  (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                  (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
      bounded :=
        (_ :
          ∀ {event : ε},
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                some event →
              bound ≤ time event) }
Tactic:
by_cases time event = bound
Proof state after:
case inl
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝² : ¬isEmpty queue₁ = true
h✝¹ : ¬isEmpty queue₂ = true
h✝ : time event = bound
⊢ event ∈
    {
      events :=
        merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
            (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
          merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
            (Array.split queue₂.events fun x => decide (time x = bound)).snd,
      sorted :=
        (_ :
          Sorted
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                  (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                  (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
      bounded :=
        (_ :
          ∀ {event : ε},
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                some event →
              bound ≤ time event) }

case inr
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝² : ¬isEmpty queue₁ = true
h✝¹ : ¬isEmpty queue₂ = true
h✝ : ¬time event = bound
⊢ event ∈
    {
      events :=
        merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
            (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
          merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
            (Array.split queue₂.events fun x => decide (time x = bound)).snd,
      sorted :=
        (_ :
          Sorted
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                  (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                  (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
      bounded :=
        (_ :
          ∀ {event : ε},
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                some event →
              bound ≤ time event) }