Theorem: List.splitOnListAux_delim (One.lean)

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

State before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
delim l : List α
h : delim ≠ []
⊢ (match _h₀ : delim ++ l with
    | [] => Array.push r acc
    | head :: tail =>
      match h : getRest (delim ++ l) delim with
      | none => splitOnListAux delim tail (Array.push acc head) r h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf (delim ++ l));
        splitOnListAux delim rest #[] (Array.push r acc) h) =
    r ++ #[acc] ++ splitOnListAux delim l #[] #[] h
Tactic:
have ⟨head, tail, heq⟩ :=List.exists_cons_of_ne_nil h
State after:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
delim l : List α
h : delim ≠ []
head : α
tail : List α
heq : delim = head :: tail
⊢ (match _h₀ : delim ++ l with
    | [] => Array.push r acc
    | head :: tail =>
      match h : getRest (delim ++ l) delim with
      | none => splitOnListAux delim tail (Array.push acc head) r h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf (delim ++ l));
        splitOnListAux delim rest #[] (Array.push r acc) h) =
    r ++ #[acc] ++ splitOnListAux delim l #[] #[] h

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

State before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
⊢ (match _h₀ : head :: tail ++ l with
    | [] => Array.push r acc
    | head_1 :: tail_1 =>
      match h : getRest (head :: tail ++ l) (head :: tail) with
      | none => splitOnListAux (head :: tail) tail_1 (Array.push acc head_1) r h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf (head :: tail ++ l));
        splitOnListAux (head :: tail) rest #[] (Array.push r acc) h) =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Tactic:
simp only [cons_append]
State after:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
⊢ (match h : getRest (head :: (tail ++ l)) (head :: tail) with
    | none => splitOnListAux (head :: tail) (tail ++ l) (Array.push acc head) r h
    | some rest => splitOnListAux (head :: tail) rest #[] (Array.push r acc) h) =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h

State before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
⊢ (match h : getRest (head :: (tail ++ l)) (head :: tail) with
    | none => splitOnListAux (head :: tail) (tail ++ l) (Array.push acc head) r h
    | some rest => splitOnListAux (head :: tail) rest #[] (Array.push r acc) h) =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Tactic:
split
State after:
case h_1
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
heq✝ : getRest (head :: (tail ++ l)) (head :: tail) = none
⊢ splitOnListAux (head :: tail) (tail ++ l) (Array.push acc head) r h =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h

case h_2
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest✝ : List α
heq✝ : getRest (head :: (tail ++ l)) (head :: tail) = some rest✝
⊢ splitOnListAux (head :: tail) rest✝ #[] (Array.push r acc) h =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h

State before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
heq : getRest (head :: (tail ++ l)) (head :: tail) = none
⊢ splitOnListAux (head :: tail) (tail ++ l) (Array.push acc head) r h =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Tactic:
case h_1 heq =>
  unfold getRest at heq
  simp at heq
State after:
no goals

State before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
⊢ splitOnListAux (head :: tail) rest #[] (Array.push r acc) h = r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Tactic:
case h_2 rest heq =>
  have h₂ : (Array.push r acc) = r ++ #[acc] ++ #[] := by simp only [Array.ext_iff, Array.push_data, Array.append_data, Array.data_toArray, append_nil]
  rw [h₂, List.splitOnListAux_r]
  congr
  have h₃ := List.eq_append_of_getRest heq
  simp_all only [ne_eq, not_false_iff, cons_append, cons.injEq, append_cancel_left_eq, true_and]
State after:
no goals

State before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
heq : getRest (head :: (tail ++ l)) (head :: tail) = none
⊢ splitOnListAux (head :: tail) (tail ++ l) (Array.push acc head) r h =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Tactic:
unfold getRest at heq
State after:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
heq : (if head = head then getRest (tail ++ l) tail else none) = none
⊢ splitOnListAux (head :: tail) (tail ++ l) (Array.push acc head) r h =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h

State before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
heq : (if head = head then getRest (tail ++ l) tail else none) = none
⊢ splitOnListAux (head :: tail) (tail ++ l) (Array.push acc head) r h =
    r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Tactic:
simp at heq
State after:
no goals

State before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
⊢ splitOnListAux (head :: tail) rest #[] (Array.push r acc) h = r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Tactic:
have h₂ : (Array.push r acc) = r ++ #[acc] ++ #[] := by simp only [Array.ext_iff, Array.push_data, Array.append_data, Array.data_toArray, append_nil]
State after:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
h₂ : Array.push r acc = r ++ #[acc] ++ #[]
⊢ splitOnListAux (head :: tail) rest #[] (Array.push r acc) h = r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h

State before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
h₂ : Array.push r acc = r ++ #[acc] ++ #[]
⊢ splitOnListAux (head :: tail) rest #[] (Array.push r acc) h = r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Tactic:
rw [h₂, List.splitOnListAux_r]
State after:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
h₂ : Array.push r acc = r ++ #[acc] ++ #[]
⊢ r ++ #[acc] ++ splitOnListAux (head :: tail) rest #[] #[] h = r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h

State before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
h₂ : Array.push r acc = r ++ #[acc] ++ #[]
⊢ r ++ #[acc] ++ splitOnListAux (head :: tail) rest #[] #[] h = r ++ #[acc] ++ splitOnListAux (head :: tail) l #[] #[] h
Tactic:
congr
State after:
case e_a.e_l
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
h₂ : Array.push r acc = r ++ #[acc] ++ #[]
⊢ rest = l

State before:
case e_a.e_l
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
h₂ : Array.push r acc = r ++ #[acc] ++ #[]
⊢ rest = l
Tactic:
have h₃ := List.eq_append_of_getRest heq
State after:
case e_a.e_l
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
h₂ : Array.push r acc = r ++ #[acc] ++ #[]
h₃ : head :: (tail ++ l) = head :: tail ++ rest
⊢ rest = l

State before:
case e_a.e_l
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
h₂ : Array.push r acc = r ++ #[acc] ++ #[]
h₃ : head :: (tail ++ l) = head :: tail ++ rest
⊢ rest = l
Tactic:
simp_all only [ne_eq, not_false_iff, cons_append, cons.injEq, append_cancel_left_eq, true_and]
State after:
no goals

State before:
α : Type u_1
acc : Array α
r : Array (Array α)
inst✝ : DecidableEq α
l : List α
head : α
tail : List α
h : head :: tail ≠ []
rest : List α
heq : getRest (head :: (tail ++ l)) (head :: tail) = some rest
⊢ Array.push r acc = r ++ #[acc] ++ #[]
Tactic:
simp only [Array.ext_iff, Array.push_data, Array.append_data, Array.data_toArray, append_nil]
State after:
no goals