internlm/Lean-Github huggingface dataset:
Theorem: List.isInfix_take_of_isInfix_append
Proof state before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) s ++
        (take (min (length l₂ - length s) (length l₁ - length l₃)) l₁ ++
          take (length l₂ - length s - (length l₁ - length l₃)) (drop (length l₁ - length l₃) l₁)) ++
      take (length l₂ - (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃))))) t =
    l₂
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Tactic:
have l2len : l₂.length = s.length + l₁.length + t.length - l₃.length := by
  apply Eq.symm
  rw [Nat.sub_eq_of_eq_add]
  exact hl
Proof state after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) s ++
        (take (min (length l₂ - length s) (length l₁ - length l₃)) l₁ ++
          take (length l₂ - length s - (length l₁ - length l₃)) (drop (length l₁ - length l₃) l₁)) ++
      take (length l₂ - (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃))))) t =
    l₂
l2len : length l₂ = length s + length l₁ + length t - length l₃
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Theorem: List.isInfix_take_of_isInfix_append
Proof state before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) s ++
        (take (min (length l₂ - length s) (length l₁ - length l₃)) l₁ ++
          take (length l₂ - length s - (length l₁ - length l₃)) (drop (length l₁ - length l₃) l₁)) ++
      take (length l₂ - (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃))))) t =
    l₂
l2len : length l₂ = length s + length l₁ + length t - length l₃
⊢ take (length l₁ - length l₃) l₁ <:+: l₂
Tactic:
rw [l2len, min_eq_right] at ih
Proof state after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length s + length l₁ + length t - length l₃) s ++
        (take (length l₁ - length l₃) l₁ ++
          take (length s + length l₁ + length t - length l₃ - length s - (length l₁ - length l₃))
            (drop (length l₁ - length l₃) l₁)) ++
      take
        (length s + length l₁ + length t - length l₃ -
          (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃)))))
        t =
    l₂
l2len : length l₂ = length s + length l₁ + length t - length l₃
⊢ take (length l₁ - length l₃) l₁ <:+: l₂

α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length s + length l₁ + length t - length l₃) s ++
        (take (min (length s + length l₁ + length t - length l₃ - length s) (length l₁ - length l₃)) l₁ ++
          take (length s + length l₁ + length t - length l₃ - length s - (length l₁ - length l₃))
            (drop (length l₁ - length l₃) l₁)) ++
      take
        (length s + length l₁ + length t - length l₃ -
          (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃)))))
        t =
    l₂
l2len : length l₂ = length s + length l₁ + length t - length l₃
⊢ length l₁ - length l₃ ≤ length s + length l₁ + length t - length l₃ - length s
Theorem: List.isInfix_take_of_isInfix_append
Proof state before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length s + length l₁ + length t - length l₃) s ++
        (take (length l₁ - length l₃) l₁ ++
          take (length s + length l₁ + length t - length l₃ - length s - (length l₁ - length l₃))
            (drop (length l₁ - length l₃) l₁)) ++
      take
        (length s + length l₁ + length t - length l₃ -
          (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃)))))
        t =
    l₂
l2len : length l₂ = length s + length l₁ + length t - length l₃
⊢ take (length l₁ - length l₃) l₁ <:+: l₂

α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length s + length l₁ + length t - length l₃) s ++
        (take (min (length s + length l₁ + length t - length l₃ - length s) (length l₁ - length l₃)) l₁ ++
          take (length s + length l₁ + length t - length l₃ - length s - (length l₁ - length l₃))
            (drop (length l₁ - length l₃) l₁)) ++
      take
        (length s + length l₁ + length t - length l₃ -
          (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃)))))
        t =
    l₂
l2len : length l₂ = length s + length l₁ + length t - length l₃
⊢ length l₁ - length l₃ ≤ length s + length l₁ + length t - length l₃ - length s
Tactic:
. rw [← ih]
  apply List.isInfix_append_right_of_isInfix
  apply List.isInfix_append_left_of_isInfix
  apply List.isInfix_append_right_of_isInfix
  apply List.isInfix_self
Proof state after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length s + length l₁ + length t - length l₃) s ++
        (take (min (length s + length l₁ + length t - length l₃ - length s) (length l₁ - length l₃)) l₁ ++
          take (length s + length l₁ + length t - length l₃ - length s - (length l₁ - length l₃))
            (drop (length l₁ - length l₃) l₁)) ++
      take
        (length s + length l₁ + length t - length l₃ -
          (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃)))))
        t =
    l₂
l2len : length l₂ = length s + length l₁ + length t - length l₃
⊢ length l₁ - length l₃ ≤ length s + length l₁ + length t - length l₃ - length s
Theorem: List.isInfix_take_of_isInfix_append
Proof state before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length s + length l₁ + length t - length l₃) s ++
        (take (min (length s + length l₁ + length t - length l₃ - length s) (length l₁ - length l₃)) l₁ ++
          take (length s + length l₁ + length t - length l₃ - length s - (length l₁ - length l₃))
            (drop (length l₁ - length l₃) l₁)) ++
      take
        (length s + length l₁ + length t - length l₃ -
          (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃)))))
        t =
    l₂
l2len : length l₂ = length s + length l₁ + length t - length l₃
⊢ length l₁ - length l₃ ≤ length s + length l₁ + length t - length l₃ - length s
Tactic:
. rw [Nat.sub_sub, add_comm l₃.length, ← Nat.sub_sub, add_assoc, add_comm, Nat.add_sub_cancel, add_comm]
  simp only [Nat.sub_le_sub_right, le_add_iff_nonneg_left, zero_le]
Proof state after:
no goals
Theorem: List.isInfix_take_of_isInfix_append
Proof state before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : s ++ l₁ ++ t = l₂ ++ l₃
⊢ length s + length l₁ + length t = length l₂ + length l₃
Tactic:
apply_fun @List.length α at ih
Proof state after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : length (s ++ l₁ ++ t) = length (l₂ ++ l₃)
⊢ length s + length l₁ + length t = length l₂ + length l₃
Theorem: List.isInfix_take_of_isInfix_append
Proof state before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : length (s ++ l₁ ++ t) = length (l₂ ++ l₃)
⊢ length s + length l₁ + length t = length l₂ + length l₃
Tactic:
simp only [List.length_append] at ih
Proof state after:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : length s + length l₁ + length t = length l₂ + length l₃
⊢ length s + length l₁ + length t = length l₂ + length l₃
Theorem: List.isInfix_take_of_isInfix_append
Proof state before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
ih : length s + length l₁ + length t = length l₂ + length l₃
⊢ length s + length l₁ + length t = length l₂ + length l₃
Tactic:
exact ih
Proof state after:
no goals
Theorem: List.isInfix_take_of_isInfix_append
Proof state before:
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) s ++
        (take (min (length l₂ - length s) (length l₁ - length l₃)) l₁ ++
          take (length l₂ - length s - (length l₁ - length l₃)) (drop (length l₁ - length l₃) l₁)) ++
      take (length l₂ - (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃))))) t =
    l₂
⊢ length l₂ = length s + length l₁ + length t - length l₃
Tactic:
apply Eq.symm
Proof state after:
case h
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) s ++
        (take (min (length l₂ - length s) (length l₁ - length l₃)) l₁ ++
          take (length l₂ - length s - (length l₁ - length l₃)) (drop (length l₁ - length l₃) l₁)) ++
      take (length l₂ - (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃))))) t =
    l₂
⊢ length s + length l₁ + length t - length l₃ = length l₂
Theorem: List.isInfix_take_of_isInfix_append
Proof state before:
case h
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) s ++
        (take (min (length l₂ - length s) (length l₁ - length l₃)) l₁ ++
          take (length l₂ - length s - (length l₁ - length l₃)) (drop (length l₁ - length l₃) l₁)) ++
      take (length l₂ - (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃))))) t =
    l₂
⊢ length s + length l₁ + length t - length l₃ = length l₂
Tactic:
rw [Nat.sub_eq_of_eq_add]
Proof state after:
case h
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) s ++
        (take (min (length l₂ - length s) (length l₁ - length l₃)) l₁ ++
          take (length l₂ - length s - (length l₁ - length l₃)) (drop (length l₁ - length l₃) l₁)) ++
      take (length l₂ - (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃))))) t =
    l₂
⊢ length s + length l₁ + length t = length l₂ + length l₃
Theorem: List.isInfix_take_of_isInfix_append
Proof state before:
case h
α : Type u_1
l₁ l₂ l₃ : List α
h : l₁ <:+: l₂ ++ l₃
s t : List α
hl : length s + length l₁ + length t = length l₂ + length l₃
l₁split : take (length l₁ - length l₃) l₁ ++ drop (length l₁ - length l₃) l₁ = l₁
ih :
  take (length l₂) s ++
        (take (min (length l₂ - length s) (length l₁ - length l₃)) l₁ ++
          take (length l₂ - length s - (length l₁ - length l₃)) (drop (length l₁ - length l₃) l₁)) ++
      take (length l₂ - (length s + (length l₁ - length l₃ + (length l₁ - (length l₁ - length l₃))))) t =
    l₂
⊢ length s + length l₁ + length t = length l₂ + length l₃
Tactic:
exact hl
Proof state after:
no goals
Theorem: List.singleton_isInfix_iff_mem
Proof state before:
α✝ : Type u_1
e : α✝
l : List α✝
⊢ [e] <:+: l ↔ e ∈ l
Tactic:
apply Iff.intro
Proof state after:
case mp
α✝ : Type u_1
e : α✝
l : List α✝
⊢ [e] <:+: l → e ∈ l

case mpr
α✝ : Type u_1
e : α✝
l : List α✝
⊢ e ∈ l → [e] <:+: l
Theorem: List.singleton_isInfix_iff_mem
Proof state before:
case mp
α✝ : Type u_1
e : α✝
l : List α✝
⊢ [e] <:+: l → e ∈ l

case mpr
α✝ : Type u_1
e : α✝
l : List α✝
⊢ e ∈ l → [e] <:+: l
Tactic:
. intro ⟨s,t,h⟩
  simp only [append_assoc, singleton_append, mem_append, find?, mem_cons, true_or, or_true, ← h]
Proof state after:
case mpr
α✝ : Type u_1
e : α✝
l : List α✝
⊢ e ∈ l → [e] <:+: l
Theorem: List.singleton_isInfix_iff_mem
Proof state before:
case mpr
α✝ : Type u_1
e : α✝
l : List α✝
⊢ e ∈ l → [e] <:+: l
Tactic:
. intro mem
  have ⟨s,t,h⟩ := List.mem_split mem
  exists s,t
  rw [h, append_assoc, singleton_append]
Proof state after:
no goals
Theorem: List.splitOnListAux_append
Proof state before:
case true
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : isInfixOf delim (l₁ ++ l₂) = true
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
rw [List.isInfixOf_ext] at heq
Proof state after:
case true
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Theorem: List.splitOnListAux_append
Proof state before:
case true
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
have ⟨s, lft, rgt⟩ := (List.isInfix_first_match _ _ heq h₂)
Proof state after:
case true
α : 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
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
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₂)
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
rw [List.take_append_of_le_length] at hinf <;> simp only [tsub_le_iff_right, ge_iff_le, le_add_iff_nonneg_right, zero_le, nonpos_iff_eq_zero]
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₁
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] 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₁
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] 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 ⟨t, hinf⟩ := isPrefix_trans hinf take_isPrefix
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₁
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] 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₁
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] 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 [← hinf]
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₁
⊢ 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₁
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₁
⊢ 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:
have hrw₁: s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂) := by simp only [append_assoc]
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₂)
⊢ 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₁
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₂)
⊢ 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:
have hrw₂: s ++ delim ++ t = s ++ delim ++ t := by simp only [append_assoc]
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
⊢ 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₁