Theorem: List.splitOnList_nonmatching (One.lean)

State before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l : List α
h₁ : ¬delim <:+: l
⊢ splitOnList delim l = [l]
Tactic:
unfold List.splitOnList
State after:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l : List α
h₁ : ¬delim <:+: l
⊢ (match delim with
    | [] => [l]
    | head :: tail =>
      Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) l #[] #[] (_ : ¬head :: tail = [])))) =
    [l]

State before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l : List α
h₁ : ¬delim <:+: l
⊢ (match delim with
    | [] => [l]
    | head :: tail =>
      Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) l #[] #[] (_ : ¬head :: tail = [])))) =
    [l]
Tactic:
cases delim with
| nil => simp only
| cons => 
  simp only
  rw [List.splitOnListAux_nonmatching]
  . simp only [Array.toList_eq, Array.map_data, map, Array.data_toArray]
  . exact h₁
State after:
no goals

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
l : List α
h₁ : ¬[] <:+: l
⊢ (match [] with
    | [] => [l]
    | head :: tail =>
      Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) l #[] #[] (_ : ¬head :: tail = [])))) =
    [l]
Tactic:
simp only
State after:
no goals

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
l : List α
head✝ : α
tail✝ : List α
h₁ : ¬head✝ :: tail✝ <:+: l
⊢ (match head✝ :: tail✝ with
    | [] => [l]
    | head :: tail =>
      Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) l #[] #[] (_ : ¬head :: tail = [])))) =
    [l]
Tactic:
simp only
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
l : List α
head✝ : α
tail✝ : List α
h₁ : ¬head✝ :: tail✝ <:+: l
⊢ Array.toList (Array.map Array.toList (splitOnListAux (head✝ :: tail✝) l #[] #[] (_ : ¬head✝ :: tail✝ = []))) = [l]

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
l : List α
head✝ : α
tail✝ : List α
h₁ : ¬head✝ :: tail✝ <:+: l
⊢ Array.toList (Array.map Array.toList (splitOnListAux (head✝ :: tail✝) l #[] #[] (_ : ¬head✝ :: tail✝ = []))) = [l]
Tactic:
rw [List.splitOnListAux_nonmatching]
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
l : List α
head✝ : α
tail✝ : List α
h₁ : ¬head✝ :: tail✝ <:+: l
⊢ Array.toList (Array.map Array.toList #[toArray l]) = [l]

case cons.h₁
α : Type u_1
inst✝ : DecidableEq α
l : List α
head✝ : α
tail✝ : List α
h₁ : ¬head✝ :: tail✝ <:+: l
⊢ ¬head✝ :: tail✝ <:+: l

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
l : List α
head✝ : α
tail✝ : List α
h₁ : ¬head✝ :: tail✝ <:+: l
⊢ Array.toList (Array.map Array.toList #[toArray l]) = [l]

case cons.h₁
α : Type u_1
inst✝ : DecidableEq α
l : List α
head✝ : α
tail✝ : List α
h₁ : ¬head✝ :: tail✝ <:+: l
⊢ ¬head✝ :: tail✝ <:+: l
Tactic:
. simp only [Array.toList_eq, Array.map_data, map, Array.data_toArray]
State after:
case cons.h₁
α : Type u_1
inst✝ : DecidableEq α
l : List α
head✝ : α
tail✝ : List α
h₁ : ¬head✝ :: tail✝ <:+: l
⊢ ¬head✝ :: tail✝ <:+: l

State before:
case cons.h₁
α : Type u_1
inst✝ : DecidableEq α
l : List α
head✝ : α
tail✝ : List α
h₁ : ¬head✝ :: tail✝ <:+: l
⊢ ¬head✝ :: tail✝ <:+: l
Tactic:
. exact h₁
State after:
no goals