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

State before:
α : Type u_1
q : QueueData α
⊢ toList q = [] ↔ pull q = none
Tactic:
simp [toList, pull]
State after:
α : Type u_1
q : QueueData α
⊢ init ++ List.reverse tail = [] ↔
    (match init with
      | x :: xs => some (x, { init := xs, tail := tail })
      | [] =>
        match List.reverse tail with
        | x :: xs => some (x, { init := xs, tail := [] })
        | [] => none) =
      none

State before:
α : Type u_1
q : QueueData α
⊢ init ++ List.reverse tail = [] ↔
    (match init with
      | x :: xs => some (x, { init := xs, tail := tail })
      | [] =>
        match List.reverse tail with
        | x :: xs => some (x, { init := xs, tail := [] })
        | [] => none) =
      none
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✝] = [] ↔
    (match List.reverse tail✝ ++ [head✝] with
      | x :: xs => some (x, { init := xs, tail := [] })
      | [] => none) =
      none

State before:
α : Type u_1
q : QueueData α
h : α
t : List α
⊢ List.reverse t ++ [h] = [] ↔
    (match List.reverse t ++ [h] with
      | x :: xs => some (x, { init := xs, tail := [] })
      | [] => none) =
      none
Tactic:
case cons h t => 
constructor
generalize t.reverse = rt
. intro q
  let u := nonEmptyAppend q
  contradiction
. generalize up: List.reverse t ++ [h] = u
  intro q
  cases u <;> simp at q <;> simp
State after:
no goals

State before:
α : Type u_1
q : QueueData α
h : α
t : List α
⊢ List.reverse t ++ [h] = [] ↔
    (match List.reverse t ++ [h] with
      | x :: xs => some (x, { init := xs, tail := [] })
      | [] => none) =
      none
Tactic:
constructor
State after:
case mp
α : Type u_1
q : QueueData α
h : α
t : List α
⊢ List.reverse t ++ [h] = [] →
    (match List.reverse t ++ [h] with
      | x :: xs => some (x, { init := xs, tail := [] })
      | [] => none) =
      none

case mpr
α : Type u_1
q : QueueData α
h : α
t : List α
⊢ (match List.reverse t ++ [h] with
      | x :: xs => some (x, { init := xs, tail := [] })
      | [] => none) =
      none →
    List.reverse t ++ [h] = []

State before:
case mp
α : Type u_1
q : QueueData α
h : α
t : List α
⊢ List.reverse t ++ [h] = [] →
    (match List.reverse t ++ [h] with
      | x :: xs => some (x, { init := xs, tail := [] })
      | [] => none) =
      none

case mpr
α : Type u_1
q : QueueData α
h : α
t : List α
⊢ (match List.reverse t ++ [h] with
      | x :: xs => some (x, { init := xs, tail := [] })
      | [] => none) =
      none →
    List.reverse t ++ [h] = []
Tactic:
generalize t.reverse = rt
State after:
case mp
α : Type u_1
q : QueueData α
h : α
t rt : List α
⊢ rt ++ [h] = [] →
    (match rt ++ [h] with
      | x :: xs => some (x, { init := xs, tail := [] })
      | [] => none) =
      none

case mpr
α : Type u_1
q : QueueData α
h : α
t : List α
⊢ (match List.reverse t ++ [h] with
      | x :: xs => some (x, { init := xs, tail := [] })
      | [] => none) =
      none →
    List.reverse t ++ [h] = []

State before:
case mp
α : Type u_1
q : QueueData α
h : α
t rt : List α
⊢ rt ++ [h] = [] →
    (match rt ++ [h] with
      | x :: xs => some (x, { init := xs, tail := [] })
      | [] => none) =
      none

case mpr
α : Type u_1
q : QueueData α
h : α
t : List α
⊢ (match List.reverse t ++ [h] with
      | x :: xs => some (x, { init := xs, tail := [] })
      | [] => none) =
      none →
    List.reverse t ++ [h] = []
Tactic:
. intro q
  let u := nonEmptyAppend q
  contradiction
State after:
case mpr
α : Type u_1
q : QueueData α
h : α
t : List α
⊢ (match List.reverse t ++ [h] with
      | x :: xs => some (x, { init := xs, tail := [] })
      | [] => none) =
      none →
    List.reverse t ++ [h] = []

State before:
case mpr
α : Type u_1
q : QueueData α
h : α
t : List α
⊢ (match List.reverse t ++ [h] with
      | x :: xs => some (x, { init := xs, tail := [] })
      | [] => none) =
      none →
    List.reverse t ++ [h] = []
Tactic:
. generalize up: List.reverse t ++ [h] = u
  intro q
  cases u <;> simp at q <;> simp
State after:
no goals