Theorem: List.splitOnListAux_progress
Proof state before:
case h.h
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
hd : α
tl : List α
ih :
  ¬delim <:+: tl ++ dropLast delim →
    splitOnListAux delim (tl ++ delim ++ rest) #[] #[] h₂ = #[toArray tl] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: hd :: tl ++ dropLast delim
head : α
tail : List α
heq : hd :: tl ++ delim ++ rest = head :: tail
rest₂ : List α
heq₂ : getRest (hd :: tl ++ delim ++ rest) delim = some rest₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ take (length delim) (hd :: (tl ++ delim)) <+: take (length delim) (hd :: (tl ++ dropLast delim))

case h.h
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
hd : α
tl : List α
ih :
  ¬delim <:+: tl ++ dropLast delim →
    splitOnListAux delim (tl ++ delim ++ rest) #[] #[] h₂ = #[toArray tl] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: hd :: tl ++ dropLast delim
head : α
tail : List α
heq : hd :: tl ++ delim ++ rest = head :: tail
rest₂ : List α
heq₂ : getRest (hd :: tl ++ delim ++ rest) delim = some rest₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ length delim ≤ Nat.succ (length tl + length delim)

case h.h
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
hd : α
tl : List α
ih :
  ¬delim <:+: tl ++ dropLast delim →
    splitOnListAux delim (tl ++ delim ++ rest) #[] #[] h₂ = #[toArray tl] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: hd :: tl ++ dropLast delim
head : α
tail : List α
heq : hd :: tl ++ delim ++ rest = head :: tail
rest₂ : List α
heq₂ : getRest (hd :: tl ++ delim ++ rest) delim = some rest₂
h₃ : take (length delim) (hd :: tl ++ delim ++ rest) = take (length delim) (delim ++ rest₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
Tactic:
. have h₄: take (length delim) (hd :: (tl ++ delim)) = take (length delim) (hd :: (tl ++ delim.dropLast)) := by
    rw [← List.cons_append, ← List.cons_append,
    List.take_append_eq_append_take, List.take_append_eq_append_take]
    rw [List.dropLast_eq_take, List.take_take, min_eq_left]
    simp only [length_cons, tsub_le_iff_right, ge_iff_le]
    calc
      length delim ≤  Nat.pred (length delim) + 1 := by simp only [Nat.pred_eq_sub_one, tsub_le_iff_right, ge_iff_le, le_refl, Nat.le_add_of_sub_le]
      _ ≤  Nat.pred (length delim) + Nat.succ (length tl) := by simp only [Nat.succ_eq_add_one, add_le_add_iff_left, le_add_iff_nonneg_left, zero_le, ge_iff_le,
        nonpos_iff_eq_zero]
  rw [h₄]
  simp only [isPrefix_self]
Proof state after:
case h.h
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
hd : α
tl : List α
ih :
  ¬delim <:+: tl ++ dropLast delim →
    splitOnListAux delim (tl ++ delim ++ rest) #[] #[] h₂ = #[toArray tl] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: hd :: tl ++ dropLast delim
head : α
tail : List α
heq : hd :: tl ++ delim ++ rest = head :: tail
rest₂ : List α
heq₂ : getRest (hd :: tl ++ delim ++ rest) delim = some rest₂
h₃ : take (length delim) (hd :: (tl ++ delim)) = delim
⊢ length delim ≤ Nat.succ (length tl + length delim)

case h.h
α : Type u_1
inst✝ : DecidableEq α
delim rest : List α
h₂ : delim ≠ []
hd : α
tl : List α
ih :
  ¬delim <:+: tl ++ dropLast delim →
    splitOnListAux delim (tl ++ delim ++ rest) #[] #[] h₂ = #[toArray tl] ++ splitOnListAux delim rest #[] #[] h₂
h₁ : ¬delim <:+: hd :: tl ++ dropLast delim
head : α
tail : List α
heq : hd :: tl ++ delim ++ rest = head :: tail
rest₂ : List α
heq₂ : getRest (hd :: tl ++ delim ++ rest) delim = some rest₂
h₃ : take (length delim) (hd :: tl ++ delim ++ rest) = take (length delim) (delim ++ rest₂)
⊢ length delim ≤ length (hd :: tl ++ delim)