Theorem: List.splitOnListAux_nonmatching (One.lean)

State before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l : List α
h₁ : ¬delim <:+: l
h : delim ≠ []
⊢ splitOnListAux delim l #[] #[] h = #[toArray l]
Tactic:
unfold splitOnListAux
State after:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l : List α
h₁ : ¬delim <:+: l
h : delim ≠ []
⊢ (match _h₀ : l with
    | [] => Array.push #[] #[]
    | head :: tail =>
      match h : getRest l delim with
      | none => splitOnListAux delim tail (Array.push #[] head) #[] h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf l);
        splitOnListAux delim rest #[] (Array.push #[] #[]) h) =
    #[toArray l]

State before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l : List α
h₁ : ¬delim <:+: l
h : delim ≠ []
⊢ (match _h₀ : l with
    | [] => Array.push #[] #[]
    | head :: tail =>
      match h : getRest l delim with
      | none => splitOnListAux delim tail (Array.push #[] head) #[] h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf l);
        splitOnListAux delim rest #[] (Array.push #[] #[]) h) =
    #[toArray l]
Tactic:
split
State after:
case h_1
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
h₁ : ¬delim <:+: []
⊢ Array.push #[] #[] = #[#[]]

case h_2
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head✝ : α
tail✝ : List α
h₁ : ¬delim <:+: head✝ :: tail✝
⊢ (match h : getRest (head✝ :: tail✝) delim with
    | none => splitOnListAux delim tail✝ (Array.push #[] head✝) #[] h
    | some rest =>
      let_fun x := (_ : sizeOf rest < sizeOf (head✝ :: tail✝));
      splitOnListAux delim rest #[] (Array.push #[] #[]) h) =
    #[toArray (head✝ :: tail✝)]

State before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
h₁ : ¬delim <:+: []
⊢ Array.push #[] #[] = #[#[]]
Tactic:
case h_1 =>
  simp only [Array.ext_iff, Array.push_data, Array.data_toArray, nil_append]
State after:
no goals

State before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
⊢ (match h : getRest (head :: tail) delim with
    | none => splitOnListAux delim tail (Array.push #[] head) #[] h
    | some rest =>
      let_fun x := (_ : sizeOf rest < sizeOf (head :: tail));
      splitOnListAux delim rest #[] (Array.push #[] #[]) h) =
    #[toArray (head :: tail)]
Tactic:
case h_2 head tail =>
  split
  case h_1 heq =>
    rw [List.splitOnListAux_acc, List.splitOnListAux_nonmatching tail]
    . simp only [Array.ext_iff, Array.modifyHead_data, modifyHead, Array.data_toArray, Array.append_eq_append,
        cons.injEq, Array.append_data, Array.push_data, nil_append, singleton_append, and_self]
    . intro contr
      apply h₁
      exact List.isInfix_cons contr
  case h_2 head tail heq =>
    simp only [List.eq_append_of_getRest heq, isInfix_append_left, not_true] at h₁
State after:
no goals

State before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
h₁ : ¬delim <:+: []
⊢ Array.push #[] #[] = #[#[]]
Tactic:
simp only [Array.ext_iff, Array.push_data, Array.data_toArray, nil_append]
State after:
no goals

State before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
⊢ (match h : getRest (head :: tail) delim with
    | none => splitOnListAux delim tail (Array.push #[] head) #[] h
    | some rest =>
      let_fun x := (_ : sizeOf rest < sizeOf (head :: tail));
      splitOnListAux delim rest #[] (Array.push #[] #[]) h) =
    #[toArray (head :: tail)]
Tactic:
split
State after:
case h_1
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
heq✝ : getRest (head :: tail) delim = none
⊢ splitOnListAux delim tail (Array.push #[] head) #[] h = #[toArray (head :: tail)]

case h_2
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
rest✝ : List α
heq✝ : getRest (head :: tail) delim = some rest✝
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    splitOnListAux delim rest✝ #[] (Array.push #[] #[]) h) =
    #[toArray (head :: tail)]

State before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
heq : getRest (head :: tail) delim = none
⊢ splitOnListAux delim tail (Array.push #[] head) #[] h = #[toArray (head :: tail)]
Tactic:
case h_1 heq =>
  rw [List.splitOnListAux_acc, List.splitOnListAux_nonmatching tail]
  . simp only [Array.ext_iff, Array.modifyHead_data, modifyHead, Array.data_toArray, Array.append_eq_append,
      cons.injEq, Array.append_data, Array.push_data, nil_append, singleton_append, and_self]
  . intro contr
    apply h₁
    exact List.isInfix_cons contr
State after:
no goals

State before:
α : Type u_1
delim : List α
head✝ : DecidableEq α
h : delim ≠ []
head : α
tail✝ : List α
h₁ : ¬delim <:+: head :: tail✝
tail : List α
heq : getRest (head :: tail✝) delim = some tail
⊢ (let_fun x := (_ : sizeOf tail < sizeOf (head :: tail✝));
    splitOnListAux delim tail #[] (Array.push #[] #[]) h) =
    #[toArray (head :: tail✝)]
Tactic:
case h_2 head tail heq =>
  simp only [List.eq_append_of_getRest heq, isInfix_append_left, not_true] at h₁
State after:
no goals

State before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
heq : getRest (head :: tail) delim = none
⊢ splitOnListAux delim tail (Array.push #[] head) #[] h = #[toArray (head :: tail)]
Tactic:
rw [List.splitOnListAux_acc, List.splitOnListAux_nonmatching tail]
State after:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
heq : getRest (head :: tail) delim = none
⊢ Array.modifyHead (Array.append (Array.push #[] head)) #[toArray tail] = #[toArray (head :: tail)]

case h₁
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
heq : getRest (head :: tail) delim = none
⊢ ¬delim <:+: tail

State before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
heq : getRest (head :: tail) delim = none
⊢ Array.modifyHead (Array.append (Array.push #[] head)) #[toArray tail] = #[toArray (head :: tail)]

case h₁
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
heq : getRest (head :: tail) delim = none
⊢ ¬delim <:+: tail
Tactic:
. simp only [Array.ext_iff, Array.modifyHead_data, modifyHead, Array.data_toArray, Array.append_eq_append,
    cons.injEq, Array.append_data, Array.push_data, nil_append, singleton_append, and_self]
State after:
case h₁
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
heq : getRest (head :: tail) delim = none
⊢ ¬delim <:+: tail

State before:
case h₁
α : Type u_1
delim : List α
inst✝ : DecidableEq α
h : delim ≠ []
head : α
tail : List α
h₁ : ¬delim <:+: head :: tail
heq : getRest (head :: tail) delim = none
⊢ ¬delim <:+: tail
Tactic:
. intro contr
  apply h₁
  exact List.isInfix_cons contr
State after:
no goals

State before:
α : Type u_1
delim : List α
head✝ : DecidableEq α
h : delim ≠ []
head : α
tail✝ : List α
h₁ : ¬delim <:+: head :: tail✝
tail : List α
heq : getRest (head :: tail✝) delim = some tail
⊢ (let_fun x := (_ : sizeOf tail < sizeOf (head :: tail✝));
    splitOnListAux delim tail #[] (Array.push #[] #[]) h) =
    #[toArray (head :: tail✝)]
Tactic:
simp only [List.eq_append_of_getRest heq, isInfix_append_left, not_true] at h₁
State after:
no goals