internlm/Lean-Github huggingface dataset:
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 ++ rest) = take (length delim) (delim ++ rest₂)
⊢ delim <+: hd :: tl ++ dropLast delim
Tactic:
rw [List.take_append_of_le_length] at h₃
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) = take (length delim) (delim ++ rest₂)
⊢ 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 ++ rest) = take (length delim) (delim ++ rest₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
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) = take (length delim) (delim ++ rest₂)
⊢ 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 ++ rest) = take (length delim) (delim ++ rest₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
Tactic:
simp at h₃
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
⊢ 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 ++ rest) = take (length delim) (delim ++ rest₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
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
⊢ 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 ++ rest) = take (length delim) (delim ++ rest₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
Tactic:
conv => left; rw [← h₃]
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
⊢ take (length delim) (hd :: (tl ++ 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 ++ rest) = take (length delim) (delim ++ rest₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
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)) <+: 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 ++ rest) = take (length delim) (delim ++ rest₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
Tactic:
simp only [length_take, length_cons, length_append, min_le_iff, ge_iff_le, cons_append]
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
⊢ take (length delim) (hd :: (tl ++ 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 ++ rest) = take (length delim) (delim ++ rest₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
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)) <+: 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 ++ rest) = take (length delim) (delim ++ rest₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
Tactic:
apply List.isPrefix_take.1
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
⊢ take (length delim) (hd :: (tl ++ delim)) <+:
    take (length (take (length delim) (hd :: (tl ++ 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 ++ rest) = take (length delim) (delim ++ rest₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
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 (take (length delim) (hd :: (tl ++ 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 ++ rest) = take (length delim) (delim ++ rest₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
Tactic:
simp only [length_take, length_cons, length_append, min_le_iff, ge_iff_le]
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
⊢ take (length delim) (hd :: (tl ++ delim)) <+:
    take (min (length delim) (Nat.succ (length tl + 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 ++ rest) = take (length delim) (delim ++ rest₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
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 (min (length delim) (Nat.succ (length tl + 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 ++ rest) = take (length delim) (delim ++ rest₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
Tactic:
rw [min_eq_left]
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
⊢ 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)
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
⊢ 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:
. simp only [Nat.succ_eq_add_one, Nat.le_add_one_iff, le_add_iff_nonneg_left, zero_le, ge_iff_le,
    nonpos_iff_eq_zero, true_or]
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 ++ rest) = take (length delim) (delim ++ rest₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
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 ++ rest) = take (length delim) (delim ++ rest₂)
⊢ length delim ≤ length (hd :: tl ++ delim)
Tactic:
. simp only [cons_append, length_cons, length_append, le_add_iff_nonneg_left, zero_le, ge_iff_le,
    nonpos_iff_eq_zero, Nat.le_succ_of_le]
Proof state after:
no goals
Theorem: List.splitOnListAux_progress
Proof state before:
α : 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))
Tactic:
rw [← List.cons_append, ← List.cons_append,
List.take_append_eq_append_take, List.take_append_eq_append_take]
Proof state after:
α : 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) ++ take (length delim - length (hd :: tl)) delim =
    take (length delim) (hd :: tl) ++ take (length delim - length (hd :: tl)) (dropLast delim)
Theorem: List.splitOnListAux_progress
Proof state before:
α : 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) ++ take (length delim - length (hd :: tl)) delim =
    take (length delim) (hd :: tl) ++ take (length delim - length (hd :: tl)) (dropLast delim)
Tactic:
rw [List.dropLast_eq_take, List.take_take, min_eq_left]
Proof state after:
α : 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 - length (hd :: tl) ≤ Nat.pred (length delim)
Theorem: List.splitOnListAux_progress
Proof state before:
α : 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 - length (hd :: tl) ≤ Nat.pred (length delim)
Tactic:
simp only [length_cons, tsub_le_iff_right, ge_iff_le]
Proof state after:
α : 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.pred (length delim) + Nat.succ (length tl)