Theorem: List.splitOnList_append (One.lean)

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

State before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
⊢ (match delim with
    | [] => [l₁ ++ l₂]
    | head :: tail =>
      Array.toList
        (Array.map Array.toList (splitOnListAux (head :: tail) (l₁ ++ l₂) #[] #[] (_ : ¬head :: tail = [])))) =
    modifyLast (fun x => x ++ l₂)
      (match delim with
      | [] => [l₁]
      | head :: tail =>
        Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) l₁ #[] #[] (_ : ¬head :: tail = []))))
Tactic:
match delim with
| [] => simp only [modifyLast_singleton]
| hd::tl => 
  simp only [Array.toList_eq, Array.map_data]
  rw [List.splitOnListAux_append _ _ h]
  rw [← map_modifyLast]
  . rw [Array.modifyLast_data]
  . unfold Function.Semiconj
    simp only [Array.toList_eq, Array.append_data, Array.data_toArray, forall_const]
State after:
no goals

State before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬[] <:+: lastN (length [] - 1) l₁ ++ l₂
⊢ (match [] with
    | [] => [l₁ ++ l₂]
    | head :: tail =>
      Array.toList
        (Array.map Array.toList (splitOnListAux (head :: tail) (l₁ ++ l₂) #[] #[] (_ : ¬head :: tail = [])))) =
    modifyLast (fun x => x ++ l₂)
      (match [] with
      | [] => [l₁]
      | head :: tail =>
        Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) l₁ #[] #[] (_ : ¬head :: tail = []))))
Tactic:
simp only [modifyLast_singleton]
State after:
no goals

State before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ (match hd :: tl with
    | [] => [l₁ ++ l₂]
    | head :: tail =>
      Array.toList
        (Array.map Array.toList (splitOnListAux (head :: tail) (l₁ ++ l₂) #[] #[] (_ : ¬head :: tail = [])))) =
    modifyLast (fun x => x ++ l₂)
      (match hd :: tl with
      | [] => [l₁]
      | head :: tail =>
        Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) l₁ #[] #[] (_ : ¬head :: tail = []))))
Tactic:
simp only [Array.toList_eq, Array.map_data]
State after:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ map Array.toList (splitOnListAux (hd :: tl) (l₁ ++ l₂) #[] #[] (_ : ¬hd :: tl = [])).data =
    modifyLast (fun x => x ++ l₂) (map Array.toList (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = [])).data)

State before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ map Array.toList (splitOnListAux (hd :: tl) (l₁ ++ l₂) #[] #[] (_ : ¬hd :: tl = [])).data =
    modifyLast (fun x => x ++ l₂) (map Array.toList (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = [])).data)
Tactic:
rw [List.splitOnListAux_append _ _ h]
State after:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ map Array.toList
      (Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = []))).data =
    modifyLast (fun x => x ++ l₂) (map Array.toList (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = [])).data)

State before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ map Array.toList
      (Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = []))).data =
    modifyLast (fun x => x ++ l₂) (map Array.toList (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = [])).data)
Tactic:
rw [← map_modifyLast]
State after:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ map Array.toList
      (Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = []))).data =
    map Array.toList (modifyLast ?m.340731 (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = [])).data)

α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ Function.Semiconj Array.toList ?m.340731 fun x => x ++ l₂

α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ Array α → Array α

State before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ map Array.toList
      (Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = []))).data =
    map Array.toList (modifyLast ?m.340731 (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = [])).data)

α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ Function.Semiconj Array.toList ?m.340731 fun x => x ++ l₂

α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ Array α → Array α
Tactic:
. rw [Array.modifyLast_data]
State after:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ Function.Semiconj Array.toList (fun x => x ++ toArray l₂) fun x => x ++ l₂

State before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ Function.Semiconj Array.toList (fun x => x ++ toArray l₂) fun x => x ++ l₂
Tactic:
. unfold Function.Semiconj
  simp only [Array.toList_eq, Array.append_data, Array.data_toArray, forall_const]
State after:
no goals