Theorem: List.splitOnListAux_ne_nil (One.lean)

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

State before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h : delim ≠ []
inst✝ : DecidableEq α
l : List α
⊢ (match _h₀ : l with
    | [] => Array.push r acc
    | head :: tail =>
      match h : getRest l delim with
      | none => splitOnListAux delim tail (Array.push acc head) r h
      | some rest =>
        let_fun x := (_ : sizeOf rest < sizeOf l);
        splitOnListAux delim rest #[] (Array.push r acc) h) ≠
    #[]
Tactic:
cases l with
| nil => simp only; intro contr; rw [Array.ext_iff] at contr; simp only [Array.push_data, Array.data_toArray, append_eq_nil, and_false] at contr
| cons head tail =>
  simp only
  match h: getRest (head::tail) delim with
  | none => 
    simp only
    have _ : length tail < Nat.succ (length tail) := by apply Nat.lt_succ_self
    apply List.splitOnListAux_ne_nil tail
  | some rest => 
    simp only
    have _ : length rest < Nat.succ (length tail) := by
      have h₂ := List.eq_append_of_getRest h
      replace h₂ := congr_arg List.length h₂
      simp at h₂
      rw[h₂]
      apply Nat.lt_add_of_pos_left
      apply Nat.zero_lt_of_ne_zero
      intro contr
      have contr₂ := List.length_eq_zero.1 contr
      contradiction
    apply List.splitOnListAux_ne_nil rest
State after:
no goals

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

State before:
case nil
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h : delim ≠ []
inst✝ : DecidableEq α
⊢ Array.push r acc ≠ #[]
Tactic:
intro contr
State after:
case nil
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h : delim ≠ []
inst✝ : DecidableEq α
contr : Array.push r acc = #[]
⊢ False

State before:
case nil
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h : delim ≠ []
inst✝ : DecidableEq α
contr : Array.push r acc = #[]
⊢ False
Tactic:
rw [Array.ext_iff] at contr
State after:
case nil
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h : delim ≠ []
inst✝ : DecidableEq α
contr : (Array.push r acc).data = #[].data
⊢ False

State before:
case nil
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h : delim ≠ []
inst✝ : DecidableEq α
contr : (Array.push r acc).data = #[].data
⊢ False
Tactic:
simp only [Array.push_data, Array.data_toArray, append_eq_nil, and_false] at contr
State after:
no goals

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

State before:
case cons
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h : delim ≠ []
inst✝ : DecidableEq α
head : α
tail : List α
⊢ (match h : getRest (head :: tail) delim with
    | none => splitOnListAux delim tail (Array.push acc head) r h
    | some rest => splitOnListAux delim rest #[] (Array.push r acc) h) ≠
    #[]
Tactic:
match h: getRest (head::tail) delim with
| none => 
  simp only
  have _ : length tail < Nat.succ (length tail) := by apply Nat.lt_succ_self
  apply List.splitOnListAux_ne_nil tail
| some rest => 
  simp only
  have _ : length rest < Nat.succ (length tail) := by
    have h₂ := List.eq_append_of_getRest h
    replace h₂ := congr_arg List.length h₂
    simp at h₂
    rw[h₂]
    apply Nat.lt_add_of_pos_left
    apply Nat.zero_lt_of_ne_zero
    intro contr
    have contr₂ := List.length_eq_zero.1 contr
    contradiction
  apply List.splitOnListAux_ne_nil rest
State after:
no goals

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

State before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail : List α
h : getRest (head :: tail) delim = none
⊢ splitOnListAux delim tail (Array.push acc head) r h✝ ≠ #[]
Tactic:
have _ : length tail < Nat.succ (length tail) := by apply Nat.lt_succ_self
State after:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail : List α
h : getRest (head :: tail) delim = none
x✝ : length tail < Nat.succ (length tail)
⊢ splitOnListAux delim tail (Array.push acc head) r h✝ ≠ #[]

State before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail : List α
h : getRest (head :: tail) delim = none
x✝ : length tail < Nat.succ (length tail)
⊢ splitOnListAux delim tail (Array.push acc head) r h✝ ≠ #[]
Tactic:
apply List.splitOnListAux_ne_nil tail
State after:
no goals

State before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail : List α
h : getRest (head :: tail) delim = none
⊢ length tail < Nat.succ (length tail)
Tactic:
apply Nat.lt_succ_self
State after:
no goals

State before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
⊢ (match h : some rest with
    | none => splitOnListAux delim tail (Array.push acc head) r h✝
    | some rest_1 => splitOnListAux delim rest_1 #[] (Array.push r acc) h✝) ≠
    #[]
Tactic:
simp only
State after:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
⊢ splitOnListAux delim rest #[] (Array.push r acc) h✝ ≠ #[]

State before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
⊢ splitOnListAux delim rest #[] (Array.push r acc) h✝ ≠ #[]
Tactic:
have _ : length rest < Nat.succ (length tail) := by
  have h₂ := List.eq_append_of_getRest h
  replace h₂ := congr_arg List.length h₂
  simp at h₂
  rw[h₂]
  apply Nat.lt_add_of_pos_left
  apply Nat.zero_lt_of_ne_zero
  intro contr
  have contr₂ := List.length_eq_zero.1 contr
  contradiction
State after:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
x✝ : length rest < Nat.succ (length tail)
⊢ splitOnListAux delim rest #[] (Array.push r acc) h✝ ≠ #[]

State before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
x✝ : length rest < Nat.succ (length tail)
⊢ splitOnListAux delim rest #[] (Array.push r acc) h✝ ≠ #[]
Tactic:
apply List.splitOnListAux_ne_nil rest
State after:
no goals

State before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
⊢ length rest < Nat.succ (length tail)
Tactic:
have h₂ := List.eq_append_of_getRest h
State after:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : head :: tail = delim ++ rest
⊢ length rest < Nat.succ (length tail)

State before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : head :: tail = delim ++ rest
⊢ length rest < Nat.succ (length tail)
Tactic:
replace h₂ := congr_arg List.length h₂
State after:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : length (head :: tail) = length (delim ++ rest)
⊢ length rest < Nat.succ (length tail)

State before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : length (head :: tail) = length (delim ++ rest)
⊢ length rest < Nat.succ (length tail)
Tactic:
simp at h₂
State after:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
⊢ length rest < Nat.succ (length tail)

State before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
⊢ length rest < Nat.succ (length tail)
Tactic:
rw[h₂]
State after:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
⊢ length rest < length delim + length rest

State before:
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
⊢ length rest < length delim + length rest
Tactic:
apply Nat.lt_add_of_pos_left
State after:
case h
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
⊢ 0 < length delim

State before:
case h
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
⊢ 0 < length delim
Tactic:
apply Nat.zero_lt_of_ne_zero
State after:
case h.h
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
⊢ length delim ≠ 0

State before:
case h.h
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
⊢ length delim ≠ 0
Tactic:
intro contr
State after:
case h.h
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
contr : length delim = 0
⊢ False

State before:
case h.h
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
contr : length delim = 0
⊢ False
Tactic:
have contr₂ := List.length_eq_zero.1 contr
State after:
case h.h
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
contr : length delim = 0
contr₂ : delim = []
⊢ False

State before:
case h.h
α : Type u_1
delim : List α
acc : Array α
r : Array (Array α)
h✝ : delim ≠ []
inst✝ : DecidableEq α
head : α
tail rest : List α
h : getRest (head :: tail) delim = some rest
h₂ : Nat.succ (length tail) = length delim + length rest
contr : length delim = 0
contr₂ : delim = []
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
delim : List α
_x✝ : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α
a✝⁴ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y _x✝ →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
acc : Array α
r✝ : (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α
a✝³ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := r✝ } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
r : Array (Array α)
h✝² : (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α
a✝² :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := h✝² } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
h✝¹ : delim ≠ []
inst✝¹ : (_ : DecidableEq α) ×' List α
a✝¹ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := { fst := h✝¹, snd := inst✝¹ } } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
inst✝ : DecidableEq α
l : List α
a✝ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := { fst := h✝¹, snd := { fst := inst✝, snd := l } } } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
head : α
tail : List α
x✝¹ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := { fst := h✝¹, snd := { fst := inst✝, snd := head :: tail } } } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
h✝ : l = head :: tail
rest : List α
h : getRest (head :: tail) delim = some rest
x✝ : length rest < Nat.succ (length tail)
⊢ (invImage
        (fun a =>
          PSigma.casesOn a fun acc snd =>
            PSigma.casesOn snd fun r snd =>
              PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
        instWellFoundedRelation).1
    { fst := #[],
      snd := { fst := Array.push r acc, snd := { fst := h✝¹, snd := { fst := fun a b => inst✝ a b, snd := rest } } } }
    { fst := acc, snd := { fst := r, snd := { fst := h✝¹, snd := { fst := inst✝, snd := head :: tail } } } }
Tactic:
try simp_wf; try decreasing_tactic
State after:
no goals

State before:
α : Type u_1
delim : List α
_x✝ : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α
a✝⁴ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y _x✝ →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
acc : Array α
r✝ : (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α
a✝³ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := r✝ } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
r : Array (Array α)
h✝² : (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α
a✝² :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := h✝² } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
h✝¹ : delim ≠ []
inst✝¹ : (_ : DecidableEq α) ×' List α
a✝¹ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := { fst := h✝¹, snd := inst✝¹ } } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
inst✝ : DecidableEq α
l : List α
a✝ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := { fst := h✝¹, snd := { fst := inst✝, snd := l } } } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
head : α
tail : List α
x✝¹ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := { fst := h✝¹, snd := { fst := inst✝, snd := head :: tail } } } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
h✝ : l = head :: tail
rest : List α
h : getRest (head :: tail) delim = some rest
x✝ : length rest < Nat.succ (length tail)
⊢ (invImage
        (fun a =>
          PSigma.casesOn a fun acc snd =>
            PSigma.casesOn snd fun r snd =>
              PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
        instWellFoundedRelation).1
    { fst := #[],
      snd := { fst := Array.push r acc, snd := { fst := h✝¹, snd := { fst := fun a b => inst✝ a b, snd := rest } } } }
    { fst := acc, snd := { fst := r, snd := { fst := h✝¹, snd := { fst := inst✝, snd := head :: tail } } } }
Tactic:
simp_wf
State after:
α : Type u_1
delim : List α
_x✝ : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α
a✝⁴ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y _x✝ →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
acc : Array α
r✝ : (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α
a✝³ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := r✝ } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
r : Array (Array α)
h✝² : (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α
a✝² :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := h✝² } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
h✝¹ : delim ≠ []
inst✝¹ : (_ : DecidableEq α) ×' List α
a✝¹ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := { fst := h✝¹, snd := inst✝¹ } } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
inst✝ : DecidableEq α
l : List α
a✝ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := { fst := h✝¹, snd := { fst := inst✝, snd := l } } } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
head : α
tail : List α
x✝¹ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := { fst := h✝¹, snd := { fst := inst✝, snd := head :: tail } } } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
h✝ : l = head :: tail
rest : List α
h : getRest (head :: tail) delim = some rest
x✝ : length rest < Nat.succ (length tail)
⊢ length rest < Nat.succ (length tail)

State before:
α : Type u_1
delim : List α
_x✝ : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α
a✝⁴ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y _x✝ →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
acc : Array α
r✝ : (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α
a✝³ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := r✝ } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
r : Array (Array α)
h✝² : (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α
a✝² :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := h✝² } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
h✝¹ : delim ≠ []
inst✝¹ : (_ : DecidableEq α) ×' List α
a✝¹ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := { fst := h✝¹, snd := inst✝¹ } } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
inst✝ : DecidableEq α
l : List α
a✝ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := { fst := h✝¹, snd := { fst := inst✝, snd := l } } } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
head : α
tail : List α
x✝¹ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := { fst := h✝¹, snd := { fst := inst✝, snd := head :: tail } } } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
h✝ : l = head :: tail
rest : List α
h : getRest (head :: tail) delim = some rest
x✝ : length rest < Nat.succ (length tail)
⊢ length rest < Nat.succ (length tail)
Tactic:
try decreasing_tactic
State after:
no goals

State before:
α : Type u_1
delim : List α
_x✝ : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α
a✝⁴ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y _x✝ →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
acc : Array α
r✝ : (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α
a✝³ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := r✝ } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
r : Array (Array α)
h✝² : (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α
a✝² :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := h✝² } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
h✝¹ : delim ≠ []
inst✝¹ : (_ : DecidableEq α) ×' List α
a✝¹ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := { fst := h✝¹, snd := inst✝¹ } } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
inst✝ : DecidableEq α
l : List α
a✝ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := { fst := h✝¹, snd := { fst := inst✝, snd := l } } } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
head : α
tail : List α
x✝¹ :
  ∀ (y : (_ : Array α) ×' (_ : Array (Array α)) ×' (_ : delim ≠ []) ×' (_ : DecidableEq α) ×' List α),
    (invImage
            (fun a =>
              PSigma.casesOn a fun acc snd =>
                PSigma.casesOn snd fun r snd =>
                  PSigma.casesOn snd fun h snd => PSigma.casesOn snd fun inst snd => length snd)
            instWellFoundedRelation).1
        y { fst := acc, snd := { fst := r, snd := { fst := h✝¹, snd := { fst := inst✝, snd := head :: tail } } } } →
      splitOnListAux delim y.2.2.2.2 y.1 y.2.1 (_ : delim ≠ []) ≠ #[]
h✝ : l = head :: tail
rest : List α
h : getRest (head :: tail) delim = some rest
x✝ : length rest < Nat.succ (length tail)
⊢ length rest < Nat.succ (length tail)
Tactic:
decreasing_tactic
State after:
no goals