Theorem: List.splitOnListAux_ne_nil
Proof 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
Proof 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)