Theorem: List.splitOnList_progress (One.lean)

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

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

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

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

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

case cons.h₁
α : Type u_1
inst✝ : DecidableEq α
front rest : List α
head : α
tail : List α
h₁ : ¬head :: tail <:+: front ++ dropLast (head :: tail)
⊢ ¬head :: tail <:+: front ++ dropLast (head :: tail)

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

case cons.h₁
α : Type u_1
inst✝ : DecidableEq α
front rest : List α
head : α
tail : List α
h₁ : ¬head :: tail <:+: front ++ dropLast (head :: tail)
⊢ ¬head :: tail <:+: front ++ dropLast (head :: tail)
Tactic:
simp only [Array.toList_eq, Array.map_data, Array.append_data, Array.data_toArray, singleton_append]
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
front rest : List α
head : α
tail : List α
h₁ : ¬head :: tail <:+: front ++ dropLast (head :: tail)
⊢ map Array.toList (toArray front :: (splitOnListAux (head :: tail) rest #[] #[] (_ : ¬head :: tail = [])).data) =
    front :: map Array.toList (splitOnListAux (head :: tail) rest #[] #[] (_ : ¬head :: tail = [])).data

case cons.h₁
α : Type u_1
inst✝ : DecidableEq α
front rest : List α
head : α
tail : List α
h₁ : ¬head :: tail <:+: front ++ dropLast (head :: tail)
⊢ ¬head :: tail <:+: front ++ dropLast (head :: tail)

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

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

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