Theorem: List.splitOnListAux_acc (One.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
delim l : List α
acc : Array α
h : delim ≠ []
⊢ splitOnListAux delim l acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l #[] #[] h)
Tactic:
induction l using List.induction_by_length_on generalizing acc with
| h l ih =>
  unfold splitOnListAux
  split
  case h_1 heq =>
    simp [Array.ext_iff]
  case h_2 head tail =>
    split
    case h_1 heq =>
      rw [ih (acc:= Array.push acc head), ih (acc:= Array.push #[] head)]
      . simp only [Array.ext_iff, Array.modifyHead_data, modifyHead, Array.append_eq_append]
        cases (splitOnListAux delim tail #[] #[] h).data with
        | nil => simp only
        | cons => 
          simp only [cons.injEq, Array.ext_iff, Array.append_data, Array.push_data, append_assoc, singleton_append,
            Array.data_toArray, nil_append, and_self]
      . simp only [length_cons, Nat.lt_succ_self]
      . simp only [length_cons, Nat.lt_succ_self]
    case h_2 heq =>
      have h₁: (Array.push #[] acc) = (Array.push #[] acc) ++ #[] := by simp [Array.ext_iff]
      have h₂: (Array.push #[] #[]) = (Array.push #[] (#[]:Array α)) ++ #[] := by simp [Array.ext_iff]
      rw [h₁,h₂,List.splitOnListAux_r, List.splitOnListAux_r]
      simp [Array.ext_iff]
State after:
no goals

State before:
case h
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
l : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length l →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
acc : Array α
⊢ splitOnListAux delim l acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l #[] #[] h)
Tactic:
unfold splitOnListAux
State after:
case h
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
l : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length l →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
acc : Array α
⊢ (match _h₀ : l with
    | [] => Array.push #[] acc
    | head :: tail =>
      match h : getRest l delim with
      | none => splitOnListAux delim tail (Array.push acc head) #[] h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf l);
        splitOnListAux delim rest #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (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)

State before:
case h
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
l : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length l →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
acc : Array α
⊢ (match _h₀ : l with
    | [] => Array.push #[] acc
    | head :: tail =>
      match h : getRest l delim with
      | none => splitOnListAux delim tail (Array.push acc head) #[] h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf l);
        splitOnListAux delim rest #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (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)
Tactic:
split
State after:
case h.h_1
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
ih :
  ∀ (l₂ : List α),
    length l₂ < length [] →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
⊢ Array.push #[] acc = Array.modifyHead (Array.append acc) (Array.push #[] #[])

case h.h_2
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head✝ : α
tail✝ : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head✝ :: tail✝) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
⊢ (match h : getRest (head✝ :: tail✝) delim with
    | none => splitOnListAux delim tail✝ (Array.push acc head✝) #[] h
    | some rest =>
      let_fun x := (_ : sizeOf rest < sizeOf (head✝ :: tail✝));
      splitOnListAux delim rest #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (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)

State before:
α : Type u_1
heq : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
ih :
  ∀ (l₂ : List α),
    length l₂ < length [] →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
⊢ Array.push #[] acc = Array.modifyHead (Array.append acc) (Array.push #[] #[])
Tactic:
case h_1 heq =>
  simp [Array.ext_iff]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
⊢ (match h : getRest (head :: tail) delim with
    | none => splitOnListAux delim tail (Array.push acc head) #[] h
    | some rest =>
      let_fun x := (_ : sizeOf rest < sizeOf (head :: tail));
      splitOnListAux delim rest #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (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)
Tactic:
case h_2 head tail =>
  split
  case h_1 heq =>
    rw [ih (acc:= Array.push acc head), ih (acc:= Array.push #[] head)]
    . simp only [Array.ext_iff, Array.modifyHead_data, modifyHead, Array.append_eq_append]
      cases (splitOnListAux delim tail #[] #[] h).data with
      | nil => simp only
      | cons => 
        simp only [cons.injEq, Array.ext_iff, Array.append_data, Array.push_data, append_assoc, singleton_append,
          Array.data_toArray, nil_append, and_self]
    . simp only [length_cons, Nat.lt_succ_self]
    . simp only [length_cons, Nat.lt_succ_self]
  case h_2 heq =>
    have h₁: (Array.push #[] acc) = (Array.push #[] acc) ++ #[] := by simp [Array.ext_iff]
    have h₂: (Array.push #[] #[]) = (Array.push #[] (#[]:Array α)) ++ #[] := by simp [Array.ext_iff]
    rw [h₁,h₂,List.splitOnListAux_r, List.splitOnListAux_r]
    simp [Array.ext_iff]
State after:
no goals

State before:
α : Type u_1
heq : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
ih :
  ∀ (l₂ : List α),
    length l₂ < length [] →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
⊢ Array.push #[] acc = Array.modifyHead (Array.append acc) (Array.push #[] #[])
Tactic:
simp [Array.ext_iff]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
⊢ (match h : getRest (head :: tail) delim with
    | none => splitOnListAux delim tail (Array.push acc head) #[] h
    | some rest =>
      let_fun x := (_ : sizeOf rest < sizeOf (head :: tail));
      splitOnListAux delim rest #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (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)
Tactic:
split
State after:
case h_1
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq✝ : getRest (head :: tail) delim = none
⊢ splitOnListAux delim tail (Array.push acc head) #[] h =
    Array.modifyHead (Array.append acc) (splitOnListAux delim tail (Array.push #[] head) #[] h)

case h_2
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq✝ : getRest (head :: tail) delim = some rest✝
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    splitOnListAux delim rest✝ #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      splitOnListAux delim rest✝ #[] (Array.push #[] #[]) h)

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ splitOnListAux delim tail (Array.push acc head) #[] h =
    Array.modifyHead (Array.append acc) (splitOnListAux delim tail (Array.push #[] head) #[] h)
Tactic:
case h_1 heq =>
  rw [ih (acc:= Array.push acc head), ih (acc:= Array.push #[] head)]
  . simp only [Array.ext_iff, Array.modifyHead_data, modifyHead, Array.append_eq_append]
    cases (splitOnListAux delim tail #[] #[] h).data with
    | nil => simp only
    | cons => 
      simp only [cons.injEq, Array.ext_iff, Array.append_data, Array.push_data, append_assoc, singleton_append,
        Array.data_toArray, nil_append, and_self]
  . simp only [length_cons, Nat.lt_succ_self]
  . simp only [length_cons, Nat.lt_succ_self]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    splitOnListAux delim rest✝ #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      splitOnListAux delim rest✝ #[] (Array.push #[] #[]) h)
Tactic:
case h_2 heq =>
  have h₁: (Array.push #[] acc) = (Array.push #[] acc) ++ #[] := by simp [Array.ext_iff]
  have h₂: (Array.push #[] #[]) = (Array.push #[] (#[]:Array α)) ++ #[] := by simp [Array.ext_iff]
  rw [h₁,h₂,List.splitOnListAux_r, List.splitOnListAux_r]
  simp [Array.ext_iff]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ splitOnListAux delim tail (Array.push acc head) #[] h =
    Array.modifyHead (Array.append acc) (splitOnListAux delim tail (Array.push #[] head) #[] h)
Tactic:
rw [ih (acc:= Array.push acc head), ih (acc:= Array.push #[] head)]
State after:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ Array.modifyHead (Array.append (Array.push acc head)) (splitOnListAux delim tail #[] #[] h) =
    Array.modifyHead (Array.append acc)
      (Array.modifyHead (Array.append (Array.push #[] head)) (splitOnListAux delim tail #[] #[] h))

case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)

case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ Array.modifyHead (Array.append (Array.push acc head)) (splitOnListAux delim tail #[] #[] h) =
    Array.modifyHead (Array.append acc)
      (Array.modifyHead (Array.append (Array.push #[] head)) (splitOnListAux delim tail #[] #[] h))

case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)

case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)
Tactic:
. simp only [Array.ext_iff, Array.modifyHead_data, modifyHead, Array.append_eq_append]
  cases (splitOnListAux delim tail #[] #[] h).data with
  | nil => simp only
  | cons => 
    simp only [cons.injEq, Array.ext_iff, Array.append_data, Array.push_data, append_assoc, singleton_append,
      Array.data_toArray, nil_append, and_self]
State after:
case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)

case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)

State before:
case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)

case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)
Tactic:
. simp only [length_cons, Nat.lt_succ_self]
State after:
case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)

State before:
case a
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ length tail < length (head :: tail)
Tactic:
. simp only [length_cons, Nat.lt_succ_self]
State after:
no goals

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
⊢ (match [] with
    | [] => []
    | a :: l => (Array.push acc head ++ a) :: l) =
    match
      match [] with
      | [] => []
      | a :: l => (Array.push #[] head ++ a) :: l with
    | [] => []
    | a :: l => (acc ++ a) :: l
Tactic:
simp only
State after:
no goals

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
heq : getRest (head :: tail) delim = none
head✝ : Array α
tail✝ : List (Array α)
⊢ (match head✝ :: tail✝ with
    | [] => []
    | a :: l => (Array.push acc head ++ a) :: l) =
    match
      match head✝ :: tail✝ with
      | [] => []
      | a :: l => (Array.push #[] head ++ a) :: l with
    | [] => []
    | a :: l => (acc ++ a) :: l
Tactic:
simp only [cons.injEq, Array.ext_iff, Array.append_data, Array.push_data, append_assoc, singleton_append,
  Array.data_toArray, nil_append, and_self]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    splitOnListAux delim rest✝ #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      splitOnListAux delim rest✝ #[] (Array.push #[] #[]) h)
Tactic:
have h₁: (Array.push #[] acc) = (Array.push #[] acc) ++ #[] := by simp [Array.ext_iff]
State after:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
h₁ : Array.push #[] acc = Array.push #[] acc ++ #[]
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    splitOnListAux delim rest✝ #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      splitOnListAux delim rest✝ #[] (Array.push #[] #[]) h)

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
h₁ : Array.push #[] acc = Array.push #[] acc ++ #[]
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    splitOnListAux delim rest✝ #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      splitOnListAux delim rest✝ #[] (Array.push #[] #[]) h)
Tactic:
have h₂: (Array.push #[] #[]) = (Array.push #[] (#[]:Array α)) ++ #[] := by simp [Array.ext_iff]
State after:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
h₁ : Array.push #[] acc = Array.push #[] acc ++ #[]
h₂ : Array.push #[] #[] = Array.push #[] #[] ++ #[]
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    splitOnListAux delim rest✝ #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      splitOnListAux delim rest✝ #[] (Array.push #[] #[]) h)

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
h₁ : Array.push #[] acc = Array.push #[] acc ++ #[]
h₂ : Array.push #[] #[] = Array.push #[] #[] ++ #[]
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    splitOnListAux delim rest✝ #[] (Array.push #[] acc) h) =
    Array.modifyHead (Array.append acc)
      (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      splitOnListAux delim rest✝ #[] (Array.push #[] #[]) h)
Tactic:
rw [h₁,h₂,List.splitOnListAux_r, List.splitOnListAux_r]
State after:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
h₁ : Array.push #[] acc = Array.push #[] acc ++ #[]
h₂ : Array.push #[] #[] = Array.push #[] #[] ++ #[]
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    Array.push #[] acc ++ splitOnListAux delim rest✝ #[] #[] h) =
    Array.modifyHead (Array.append acc)
      (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      Array.push #[] #[] ++ splitOnListAux delim rest✝ #[] #[] h)

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
h₁ : Array.push #[] acc = Array.push #[] acc ++ #[]
h₂ : Array.push #[] #[] = Array.push #[] #[] ++ #[]
⊢ (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
    Array.push #[] acc ++ splitOnListAux delim rest✝ #[] #[] h) =
    Array.modifyHead (Array.append acc)
      (let_fun x := (_ : sizeOf rest✝ < sizeOf (head :: tail));
      Array.push #[] #[] ++ splitOnListAux delim rest✝ #[] #[] h)
Tactic:
simp [Array.ext_iff]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
⊢ Array.push #[] acc = Array.push #[] acc ++ #[]
Tactic:
simp [Array.ext_iff]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
delim : List α
h : delim ≠ []
acc : Array α
head : α
tail : List α
ih :
  ∀ (l₂ : List α),
    length l₂ < length (head :: tail) →
      ∀ (acc : Array α),
        splitOnListAux delim l₂ acc #[] h = Array.modifyHead (Array.append acc) (splitOnListAux delim l₂ #[] #[] h)
rest✝ : List α
heq : getRest (head :: tail) delim = some rest✝
h₁ : Array.push #[] acc = Array.push #[] acc ++ #[]
⊢ Array.push #[] #[] = Array.push #[] #[] ++ #[]
Tactic:
simp [Array.ext_iff]
State after:
no goals