internlm/Lean-Github huggingface dataset:
Theorem: List.splitOnListAux_append
Proof state before:
case true.inl
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
⊢ splitOnListAux delim (s ++ delim ++ t ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim (s ++ delim ++ t) #[] #[] h₂)

case true.inl
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : s ++ delim <+: take (length l₁) (l₁ ++ l₂)
⊢ length l₁ ≤ length l₁
Tactic:
rw [hrw₁, hrw₂, splitOnListAux_progress rgt, splitOnListAux_progress rgt]
Proof state after:
case true.inl
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
⊢ #[toArray s] ++ splitOnListAux delim (t ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (#[toArray s] ++ splitOnListAux delim t #[] #[] h₂)

case true.inl
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : s ++ delim <+: take (length l₁) (l₁ ++ l₂)
⊢ length l₁ ≤ length l₁
Theorem: List.splitOnListAux_append
Proof state before:
case true.inl
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
⊢ #[toArray s] ++ splitOnListAux delim (t ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (#[toArray s] ++ splitOnListAux delim t #[] #[] h₂)

case true.inl
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : s ++ delim <+: take (length l₁) (l₁ ++ l₂)
⊢ length l₁ ≤ length l₁
Tactic:
have _ : length t < length l₁ := by
  apply_fun @List.length α at hinf
  rw [← hinf, length_append, length_append]
  apply Nat.lt_add_of_pos_left
  apply Nat.add_pos_right
  apply List.length_pos_of_ne_nil h₂
Proof state after:
case true.inl
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
x✝ : length t < length l₁
⊢ #[toArray s] ++ splitOnListAux delim (t ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (#[toArray s] ++ splitOnListAux delim t #[] #[] h₂)

case true.inl
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : s ++ delim <+: take (length l₁) (l₁ ++ l₂)
⊢ length l₁ ≤ length l₁
Theorem: List.splitOnListAux_append
Proof state before:
case true.inl
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
x✝ : length t < length l₁
⊢ #[toArray s] ++ splitOnListAux delim (t ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (#[toArray s] ++ splitOnListAux delim t #[] #[] h₂)

case true.inl
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : s ++ delim <+: take (length l₁) (l₁ ++ l₂)
⊢ length l₁ ≤ length l₁
Tactic:
rw [List.splitOnListAux_append t]
Proof state after:
case true.inl
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
x✝ : length t < length l₁
⊢ #[toArray s] ++ Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim t #[] #[] h₂) =
    Array.modifyLast (fun x => x ++ toArray l₂) (#[toArray s] ++ splitOnListAux delim t #[] #[] h₂)

case true.inl.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
x✝ : length t < length l₁
⊢ ¬delim <:+: lastN (length delim - 1) t ++ l₂

case true.inl
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : s ++ delim <+: take (length l₁) (l₁ ++ l₂)
⊢ length l₁ ≤ length l₁
Theorem: List.splitOnListAux_append
Proof state before:
case true.inl
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
x✝ : length t < length l₁
⊢ #[toArray s] ++ Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim t #[] #[] h₂) =
    Array.modifyLast (fun x => x ++ toArray l₂) (#[toArray s] ++ splitOnListAux delim t #[] #[] h₂)

case true.inl.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
x✝ : length t < length l₁
⊢ ¬delim <:+: lastN (length delim - 1) t ++ l₂

case true.inl
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : s ++ delim <+: take (length l₁) (l₁ ++ l₂)
⊢ length l₁ ≤ length l₁
Tactic:
. apply Array.ext'
  simp only [Array.append_data, Array.data_toArray, Array.modifyLast_data, singleton_append]
  cases h₃: (splitOnListAux delim t #[] #[] h₂).data with
  | nil => 
    exfalso
    apply @splitOnListAux_ne_nil α delim #[] #[] h₂ _ t
    apply Array.ext'
    simp only [h₃, Array.data_toArray]
  | cons head tail=> conv => right; rw [List.modifyLast_cons (List.cons_ne_nil head tail)]
Proof state after:
case true.inl.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
x✝ : length t < length l₁
⊢ ¬delim <:+: lastN (length delim - 1) t ++ l₂

case true.inl
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : s ++ delim <+: take (length l₁) (l₁ ++ l₂)
⊢ length l₁ ≤ length l₁
Theorem: List.splitOnListAux_append
Proof state before:
case true.inl.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
x✝ : length t < length l₁
⊢ ¬delim <:+: lastN (length delim - 1) t ++ l₂

case true.inl
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : s ++ delim <+: take (length l₁) (l₁ ++ l₂)
⊢ length l₁ ≤ length l₁
Tactic:
. rw [← hinf] at h
  intro contr
  apply h
  unfold lastN
  unfold lastN at contr
  rw [List.drop_append_eq_append_drop,List.drop_append_eq_append_drop]
  simp only [append_assoc, length_append, tsub_le_iff_right, ge_iff_le, add_le_add_iff_left]
  apply List.isInfix_append_left_of_isInfix
  apply List.isInfix_append_left_of_isInfix
  convert contr using 3
  rw [ Nat.add_comm (length delim), ← Nat.add_assoc, Nat.add_sub_assoc, Nat.sub_sub_self, ←Nat.sub_sub,
    Nat.add_comm (length s), Nat.add_assoc, Nat.add_comm (length s), ← Nat.add_assoc, Nat.add_sub_assoc, Nat.sub_self,
    Nat.add_zero]
  . rw [Nat.sub_sub_eq_add_sub_of_le]
    apply Nat.succ_le.2
    simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, h₂, not_false_iff, length_pos_of_ne_nil]
  . simp only [le_refl]
  . apply Nat.succ_le.2
    simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, h₂, not_false_iff, length_pos_of_ne_nil]
  . simp only [tsub_le_iff_right, ge_iff_le, le_add_iff_nonneg_right]
Proof state after:
case true.inl
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : s ++ delim <+: take (length l₁) (l₁ ++ l₂)
⊢ length l₁ ≤ length l₁
Theorem: List.splitOnListAux_append
Proof state before:
case true.inl
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf : s ++ delim <+: take (length l₁) (l₁ ++ l₂)
⊢ length l₁ ≤ length l₁
Tactic:
. apply le_refl
Proof state after:
no goals
Theorem: List.splitOnListAux_append
Proof state before:
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
⊢ s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
Tactic:
simp only [append_assoc]
Proof state after:
no goals
Theorem: List.splitOnListAux_append
Proof state before:
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
⊢ s ++ delim ++ t = s ++ delim ++ t
Tactic:
simp only [append_assoc]
Proof state after:
no goals
Theorem: List.splitOnListAux_append
Proof state before:
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
⊢ length t < length l₁
Tactic:
apply_fun @List.length α at hinf
Proof state after:
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
hinf : length (s ++ delim ++ t) = length l₁
⊢ length t < length l₁
Theorem: List.splitOnListAux_append
Proof state before:
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
hinf : length (s ++ delim ++ t) = length l₁
⊢ length t < length l₁
Tactic:
rw [← hinf, length_append, length_append]
Proof state after:
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
hinf : length (s ++ delim ++ t) = length l₁
⊢ length t < length s + length delim + length t
Theorem: List.splitOnListAux_append
Proof state before:
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
hinf : length (s ++ delim ++ t) = length l₁
⊢ length t < length s + length delim + length t
Tactic:
apply Nat.lt_add_of_pos_left
Proof state after:
case h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
hinf : length (s ++ delim ++ t) = length l₁
⊢ 0 < length s + length delim
Theorem: List.splitOnListAux_append
Proof state before:
case h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
hinf : length (s ++ delim ++ t) = length l₁
⊢ 0 < length s + length delim
Tactic:
apply Nat.add_pos_right
Proof state after:
case h.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
hinf : length (s ++ delim ++ t) = length l₁
⊢ 0 < length delim
Theorem: List.splitOnListAux_append
Proof state before:
case h.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
hinf : length (s ++ delim ++ t) = length l₁
⊢ 0 < length delim
Tactic:
apply List.length_pos_of_ne_nil h₂
Proof state after:
no goals
Theorem: List.splitOnListAux_append
Proof state before:
case true.inl.h.nil
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
x✝ : length t < length l₁
h₃ : (splitOnListAux delim t #[] #[] h₂).data = []
⊢ toArray s :: modifyLast (fun x => x ++ toArray l₂) [] = modifyLast (fun x => x ++ toArray l₂) [toArray s]
Tactic:
exfalso
Proof state after:
case true.inl.h.nil.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
x✝ : length t < length l₁
h₃ : (splitOnListAux delim t #[] #[] h₂).data = []
⊢ False
Theorem: List.splitOnListAux_append
Proof state before:
case true.inl.h.nil.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
x✝ : length t < length l₁
h₃ : (splitOnListAux delim t #[] #[] h₂).data = []
⊢ False
Tactic:
apply @splitOnListAux_ne_nil α delim #[] #[] h₂ _ t
Proof state after:
case true.inl.h.nil.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
x✝ : length t < length l₁
h₃ : (splitOnListAux delim t #[] #[] h₂).data = []
⊢ splitOnListAux delim t #[] #[] h₂ = #[]
Theorem: List.splitOnListAux_append
Proof state before:
case true.inl.h.nil.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
x✝ : length t < length l₁
h₃ : (splitOnListAux delim t #[] #[] h₂).data = []
⊢ splitOnListAux delim t #[] #[] h₂ = #[]
Tactic:
apply Array.ext'
Proof state after:
case true.inl.h.nil.h.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
x✝ : length t < length l₁
h₃ : (splitOnListAux delim t #[] #[] h₂).data = []
⊢ (splitOnListAux delim t #[] #[] h₂).data = #[].data
Theorem: List.splitOnListAux_append
Proof state before:
case true.inl.h.nil.h.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
x✝ : length t < length l₁
h₃ : (splitOnListAux delim t #[] #[] h₂).data = []
⊢ (splitOnListAux delim t #[] #[] h₂).data = #[].data
Tactic:
simp only [h₃, Array.data_toArray]
Proof state after:
no goals
Theorem: List.splitOnListAux_append
Proof state before:
case true.inl.h.cons
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : s ++ delim <+: take (length l₁) l₁
t : List α
hinf : s ++ delim ++ t = l₁
hrw₁ : s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂)
hrw₂ : s ++ delim ++ t = s ++ delim ++ t
x✝ : length t < length l₁
head : Array α
tail : List (Array α)
h₃ : (splitOnListAux delim t #[] #[] h₂).data = head :: tail
⊢ toArray s :: modifyLast (fun x => x ++ toArray l₂) (head :: tail) =
    modifyLast (fun x => x ++ toArray l₂) (toArray s :: head :: tail)
Tactic:
conv => right; rw [List.modifyLast_cons (List.cons_ne_nil head tail)]
Proof state after:
no goals