Theorem: QueueData.isEmptyToList (Advent/Queue.lean)

State before:
α : Type u_1
q : QueueData α
⊢ isEmpty q = true ↔ toList q = []
Tactic:
simp [isEmpty, toList, List.isEmpty]
State after:
α : Type u_1
q : QueueData α
⊢ (match init with
        | [] => true
        | head :: tail => false) =
        true ∧
      (match tail with
        | [] => true
        | head :: tail => false) =
        true ↔
    init ++ List.reverse tail = []

State before:
α : Type u_1
q : QueueData α
⊢ (match init with
        | [] => true
        | head :: tail => false) =
        true ∧
      (match tail with
        | [] => true
        | head :: tail => false) =
        true ↔
    init ++ List.reverse tail = []
Tactic:
cases q.init <;> cases q.tail <;> simp
State after:
case nil.cons
α : Type u_1
q : QueueData α
head✝ : α
tail✝ : List α
⊢ ¬List.reverse tail✝ ++ [head✝] = []

State before:
α : Type u_1
q : QueueData α
h : α
t : List α
⊢ ¬List.reverse t ++ [h] = []
Tactic:
case cons h t => 
simp
intro p
apply nonEmptyAppend p
State after:
no goals

State before:
α : Type u_1
q : QueueData α
h : α
t : List α
⊢ ¬List.reverse t ++ [h] = []
Tactic:
intro p
State after:
α : Type u_1
q : QueueData α
h : α
t : List α
p : List.reverse t ++ [h] = []
⊢ False

State before:
α : Type u_1
q : QueueData α
h : α
t : List α
p : List.reverse t ++ [h] = []
⊢ False
Tactic:
apply nonEmptyAppend p
State after:
no goals