internlm/Lean-Github huggingface dataset:
Theorem: correctLeft
Proof state before:
case intro
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
i : Nat
ilt : Nat.succ i < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej :
  List.get t { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } =
    List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
left✝ : (List.all t fun x => x != h) = true
tdiff : differs t = true
td : DifferentList t := correctLeft t tdiff
u : i = j
⊢ i = j
Tactic:
assumption
Proof state after:
no goals
Theorem: correctRight
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
dl : DifferentList xs
⊢ differs xs = true
Tactic:
cases xs <;> simp [differs]
Proof state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
dl : DifferentList (head✝ :: tail✝)
⊢ (List.all tail✝ fun x => x != head✝) = true ∧ differs tail✝ = true
Theorem: correctRight
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ (List.all t fun x => x != h) = true ∧ differs t = true
Tactic:
case cons h t =>
simp [differs] 
constructor
. apply DifListHead dl
. apply correctRight
  apply DifListTail _ dl
Proof state after:
no goals
Theorem: correctRight
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ (List.all t fun x => x != h) = true ∧ differs t = true
Tactic:
constructor
Proof state after:
case left
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ (List.all t fun x => x != h) = true

case right
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ differs t = true
Theorem: correctRight
Proof state before:
case left
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ (List.all t fun x => x != h) = true

case right
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ differs t = true
Tactic:
. apply DifListHead dl
Proof state after:
case right
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ differs t = true
Theorem: correctRight
Proof state before:
case right
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
dl : DifferentList (h :: t)
⊢ differs t = true
Tactic:
. apply correctRight
  apply DifListTail _ dl
Proof state after:
no goals
Theorem: differsIsCorect
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ differs xs = true ↔ DifferentList xs
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ differs xs = true → DifferentList xs

case mpr
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ DifferentList xs → differs xs = true
Theorem: differsIsCorect
Proof state before:
case mp
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ differs xs = true → DifferentList xs

case mpr
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ DifferentList xs → differs xs = true
Tactic:
apply correctLeft
Proof state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ DifferentList xs → differs xs = true
Theorem: differsIsCorect
Proof state before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ DifferentList xs → differs xs = true
Tactic:
apply correctRight
Proof state after:
no goals
Theorem: shuffleCancelable
Proof state before:
n : Nat
i : Fin (n + 2)
⊢ shuffleIndex (shuffleIndex i) = i
Tactic:
cases i with | mk v lt => 
cases v with
| zero => simp [shuffleIndex] 
| succ v1 => cases v1 <;> simp [shuffleIndex]
Proof state after:
no goals
Theorem: shuffleCancelable
Proof state before:
case mk
n v : Nat
lt : v < n + 2
⊢ shuffleIndex (shuffleIndex { val := v, isLt := lt }) = { val := v, isLt := lt }
Tactic:
cases v with
| zero => simp [shuffleIndex] 
| succ v1 => cases v1 <;> simp [shuffleIndex]
Proof state after:
no goals
Theorem: shuffleCancelable
Proof state before:
case mk.zero
n : Nat
lt : Nat.zero < n + 2
⊢ shuffleIndex (shuffleIndex { val := Nat.zero, isLt := lt }) = { val := Nat.zero, isLt := lt }
Tactic:
simp [shuffleIndex]
Proof state after:
no goals
Theorem: shuffleCancelable
Proof state before:
case mk.succ
n v1 : Nat
lt : Nat.succ v1 < n + 2
⊢ shuffleIndex (shuffleIndex { val := Nat.succ v1, isLt := lt }) = { val := Nat.succ v1, isLt := lt }
Tactic:
cases v1 <;> simp [shuffleIndex]
Proof state after:
no goals
Theorem: shuffledGet
Proof state before:
α : Type u_1
x y : α
xs : List α
i : Fin (List.length xs + 2)
⊢ List.get (x :: y :: xs) i = List.get (y :: x :: xs) (shuffleIndex i)
Tactic:
cases i with | mk v vlt => 
cases v 
. simp [List.get]
. case succ v1 => cases v1 <;> simp [List.get]
Proof state after:
no goals
Theorem: shuffledGet
Proof state before:
case mk
α : Type u_1
x y : α
xs : List α
v : Nat
vlt : v < List.length xs + 2
⊢ List.get (x :: y :: xs) { val := v, isLt := vlt } = List.get (y :: x :: xs) (shuffleIndex { val := v, isLt := vlt })
Tactic:
cases v
Proof state after:
case mk.zero
α : Type u_1
x y : α
xs : List α
vlt : Nat.zero < List.length xs + 2
⊢ List.get (x :: y :: xs) { val := Nat.zero, isLt := vlt } =
    List.get (y :: x :: xs) (shuffleIndex { val := Nat.zero, isLt := vlt })

case mk.succ
α : Type u_1
x y : α
xs : List α
n✝ : Nat
vlt : Nat.succ n✝ < List.length xs + 2
⊢ List.get (x :: y :: xs) { val := Nat.succ n✝, isLt := vlt } =
    List.get (y :: x :: xs) (shuffleIndex { val := Nat.succ n✝, isLt := vlt })
Theorem: shuffledGet
Proof state before:
case mk.zero
α : Type u_1
x y : α
xs : List α
vlt : Nat.zero < List.length xs + 2
⊢ List.get (x :: y :: xs) { val := Nat.zero, isLt := vlt } =
    List.get (y :: x :: xs) (shuffleIndex { val := Nat.zero, isLt := vlt })

case mk.succ
α : Type u_1
x y : α
xs : List α
n✝ : Nat
vlt : Nat.succ n✝ < List.length xs + 2
⊢ List.get (x :: y :: xs) { val := Nat.succ n✝, isLt := vlt } =
    List.get (y :: x :: xs) (shuffleIndex { val := Nat.succ n✝, isLt := vlt })
Tactic:
. simp [List.get]
Proof state after:
case mk.succ
α : Type u_1
x y : α
xs : List α
n✝ : Nat
vlt : Nat.succ n✝ < List.length xs + 2
⊢ List.get (x :: y :: xs) { val := Nat.succ n✝, isLt := vlt } =
    List.get (y :: x :: xs) (shuffleIndex { val := Nat.succ n✝, isLt := vlt })
Theorem: shuffledGet
Proof state before:
case mk.succ
α : Type u_1
x y : α
xs : List α
n✝ : Nat
vlt : Nat.succ n✝ < List.length xs + 2
⊢ List.get (x :: y :: xs) { val := Nat.succ n✝, isLt := vlt } =
    List.get (y :: x :: xs) (shuffleIndex { val := Nat.succ n✝, isLt := vlt })
Tactic:
. case succ v1 => cases v1 <;> simp [List.get]
Proof state after:
no goals
Theorem: shuffledGet
Proof state before:
α : Type u_1
x y : α
xs : List α
v1 : Nat
vlt : Nat.succ v1 < List.length xs + 2
⊢ List.get (x :: y :: xs) { val := Nat.succ v1, isLt := vlt } =
    List.get (y :: x :: xs) (shuffleIndex { val := Nat.succ v1, isLt := vlt })
Tactic:
cases v1 <;> simp [List.get]
Proof state after:
no goals
Theorem: DoubleSys.doubleLe
Proof state before:
b a : Nat
⊢ b > 0 → a < b * 2 → ¬a < b → b * 2 - 1 - a < b
Tactic:
intros u p q
Proof state after:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
⊢ b * 2 - 1 - a < b
Theorem: DoubleSys.doubleLe
Proof state before:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
⊢ b * 2 - 1 - a < b
Tactic:
rw [<-Nat.sub_add_eq]
Proof state after:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
⊢ b * 2 - (1 + a) < b
Theorem: DoubleSys.doubleLe
Proof state before:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
⊢ b * 2 - (1 + a) < b
Tactic:
have p₂: b = b * 2 - b := by 
  rw [Nat.mul_add b 1 1]
  simp
Proof state after:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b * 2 - (1 + a) < b
Theorem: DoubleSys.doubleLe
Proof state before:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b * 2 - (1 + a) < b
Tactic:
conv => rhs; rw [p₂]
Proof state after:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b * 2 - (1 + a) < b * 2 - b
Theorem: DoubleSys.doubleLe
Proof state before:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b * 2 - (1 + a) < b * 2 - b
Tactic:
apply Nat.sub_lt_sub_left
Proof state after:
case a
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b < b * 2

case a
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b < 1 + a
Theorem: DoubleSys.doubleLe
Proof state before:
case a
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b < b * 2

case a
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b < 1 + a
Tactic:
. apply Nat.lt_add_of_pos_left
  simp
  assumption
Proof state after:
case a
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b < 1 + a
Theorem: DoubleSys.doubleLe
Proof state before:
case a
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b < 1 + a
Tactic:
. apply Nat.lt_of_not_le
  intro p
  apply q
  apply Nat.lt_of_succ_le
  rw [Nat.add_comm] at p
  assumption
Proof state after:
no goals
Theorem: DoubleSys.doubleLe
Proof state before:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
⊢ b = b * 2 - b
Tactic:
rw [Nat.mul_add b 1 1]
Proof state after:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
⊢ b = b * 1 + b * 1 - b
Theorem: DoubleSys.doubleLe
Proof state before:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
⊢ b = b * 1 + b * 1 - b
Tactic:
simp
Proof state after:
no goals
Theorem: QueueData.nonEmptyAppend
Proof state before:
α : Type u_1
xs ys : List α
x : α
p : xs ++ x :: ys = []
⊢ False
Tactic:
cases xs <;> simp at p
Proof state after:
no goals
Theorem: QueueData.isEmptyToList
Proof state before:
α : Type u_1
q : QueueData α
⊢ isEmpty q = true ↔ toList q = []
Tactic:
simp [isEmpty, toList, List.isEmpty]
Proof 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 = []
Theorem: QueueData.isEmptyToList
Proof 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
Proof state after:
case nil.cons
α : Type u_1
q : QueueData α
head✝ : α
tail✝ : List α
⊢ ¬List.reverse tail✝ ++ [head✝] = []
Theorem: QueueData.isEmptyToList
Proof 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
Proof state after:
no goals
Theorem: QueueData.isEmptyToList
Proof state before:
α : Type u_1
q : QueueData α
h : α
t : List α
⊢ ¬List.reverse t ++ [h] = []
Tactic:
intro p
Proof state after:
α : Type u_1
q : QueueData α
h : α
t : List α
p : List.reverse t ++ [h] = []
⊢ False
Theorem: QueueData.isEmptyToList
Proof state before:
α : Type u_1
q : QueueData α
h : α
t : List α
p : List.reverse t ++ [h] = []
⊢ False
Tactic:
apply nonEmptyAppend p
Proof state after:
no goals
Theorem: QueueData.emptyPull
Proof state before:
α : Type u_1
q : QueueData α
⊢ toList q = [] ↔ pull q = none
Tactic:
simp [toList, pull]
Proof 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
Theorem: QueueData.emptyPull
Proof 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
Proof 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
Theorem: QueueData.emptyPull
Proof 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
Proof state after:
no goals
Theorem: QueueData.emptyPull
Proof 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
Proof 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] = []
Theorem: QueueData.emptyPull
Proof 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
Proof 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] = []
Theorem: QueueData.emptyPull
Proof 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
Proof 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] = []
Theorem: QueueData.emptyPull
Proof 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
Proof state after:
no goals
Theorem: QueueData.nonEmptyPull
Proof state before:
α : Type u_1
q : QueueData α
x : α
xs : List α
⊢ toList q = x :: xs ↔ ∃ qt, toList qt = xs ∧ pull q = some (x, qt)
Tactic:
simp [toList, pull]
Proof state after:
α : Type u_1
q : QueueData α
x : α
xs : List α
⊢ init ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match init with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match List.reverse tail with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)
Theorem: QueueData.nonEmptyPull
Proof state before:
α : Type u_1
q : QueueData α
x : α
xs : List α
⊢ init ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match init with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match List.reverse tail with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)
Tactic:
cases q.init
Proof state after:
case nil
α : Type u_1
q : QueueData α
x : α
xs : List α
⊢ [] ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match [] with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match List.reverse tail with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)

case cons
α : Type u_1
q : QueueData α
x : α
xs : List α
head✝ : α
tail✝ : List α
⊢ head✝ :: tail✝ ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match head✝ :: tail✝ with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match List.reverse tail with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)
Theorem: QueueData.nonEmptyPull
Proof state before:
case nil
α : Type u_1
q : QueueData α
x : α
xs : List α
⊢ [] ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match [] with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match List.reverse tail with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)

case cons
α : Type u_1
q : QueueData α
x : α
xs : List α
head✝ : α
tail✝ : List α
⊢ head✝ :: tail✝ ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match head✝ :: tail✝ with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match List.reverse tail with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)
Tactic:
generalize p : q.tail.reverse = tr
Proof state after:
case nil
α : Type u_1
q : QueueData α
x : α
xs tr : List α
p : List.reverse tail = tr
⊢ [] ++ tr = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match [] with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match tr with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)

case cons
α : Type u_1
q : QueueData α
x : α
xs : List α
head✝ : α
tail✝ : List α
⊢ head✝ :: tail✝ ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match head✝ :: tail✝ with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match List.reverse tail with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)
Theorem: QueueData.nonEmptyPull
Proof state before:
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
⊢ h = x ∧ t = xs ↔ ∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = qt
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
⊢ h = x ∧ t = xs → ∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = qt

case mpr
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
⊢ (∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = qt) → h = x ∧ t = xs
Theorem: QueueData.nonEmptyPull
Proof state before:
case mp
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
⊢ h = x ∧ t = xs → ∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = qt

case mpr
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
⊢ (∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = qt) → h = x ∧ t = xs
Tactic:
. intro p1 
  exists ⟨ t , []⟩
  simp [*]
Proof state after:
case mpr
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
⊢ (∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = qt) → h = x ∧ t = xs
Theorem: QueueData.nonEmptyPull
Proof state before:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
⊢ h = x ∧ t = xs
Tactic:
simp [*]
Proof state after:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
⊢ t = xs
Theorem: QueueData.nonEmptyPull
Proof state before:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
⊢ t = xs
Tactic:
let p2 := p1.right.right
Proof state after:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1.right.right
⊢ t = xs
Theorem: QueueData.nonEmptyPull
Proof state before:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1.right.right
⊢ t = xs
Tactic:
simp at p1
Proof state after:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : qi ++ List.reverse qt = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1.right.right
⊢ t = xs
Theorem: QueueData.nonEmptyPull
Proof state before:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : qi ++ List.reverse qt = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1.right.right
p3 : (fun x => init) { init := t, tail := [] } = (fun x => init) { init := qi, tail := qt } :=
  congrArg (fun x => init) p2
p4 : (fun x => tail) { init := t, tail := [] } = (fun x => tail) { init := qi, tail := qt } :=
  congrArg (fun x => tail) p2
⊢ t = xs
Tactic:
simp at p3 p4
Proof state after:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : qi ++ List.reverse qt = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1.right.right
p3 : t = qi := congrArg (fun x => init) p2
p4 : [] = qt := congrArg (fun x => tail) p2
⊢ t = xs