Theorem: List.splitOnListAux_append (One.lean)

State before:
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
cases heq: List.isInfixOf delim (l₁ ++ l₂) with
| true =>
  rw [List.isInfixOf_ext] at heq
  have ⟨s, lft, rgt⟩ := (List.isInfix_first_match _ _ heq h₂)
  cases List.append_isPrefix_split lft (length l₁) with
  | inl hinf => 
    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]
    have ⟨t, hinf⟩ := isPrefix_trans hinf take_isPrefix
    rw [← hinf]
    have hrw₁: s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂) := by simp only [append_assoc]
    have hrw₂: s ++ delim ++ t = s ++ delim ++ t := by simp only [append_assoc]
    rw [hrw₁, hrw₂, splitOnListAux_progress rgt, splitOnListAux_progress rgt]
    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₂
      
    rw [List.splitOnListAux_append t]
    . 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)]
    . 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]
    . apply le_refl
  | inr hinf =>
    have hzero: length l₁ + 1 - length delim - length l₁ = 0 := by
      simp only [tsub_le_iff_right, ge_iff_le, add_le_add_iff_left, zero_le, nonpos_iff_eq_zero,
        tsub_eq_zero_iff_le]
      apply Nat.succ_le_of_lt
      simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, h₂, not_false_iff, length_pos_of_ne_nil]
    rw [List.drop_append_eq_append_drop, hzero, drop] at hinf
    have ⟨t, hinf⟩ := hinf
    unfold lastN at h
    exfalso
    apply h
    exists drop (length l₁ + 1 - length delim) s, t
    convert hinf using 3
    rw [Nat.sub_sub_eq_add_sub_of_le]
    apply Nat.succ_le_of_lt
    apply Nat.zero_lt_of_ne_zero
    simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, length_eq_zero, h₂, not_false_iff]
| false =>
  rw [← Bool.not_eq_true, isInfixOf_ext] at heq
  have not_in_l₁: ¬ delim <:+: l₁  :=  by
    intro contr;
    apply heq
    apply List.isInfix_append_right_of_isInfix contr
  rw [splitOnListAux_nonmatching _ heq, splitOnListAux_nonmatching _ not_in_l₁]
  apply Array.ext'
  simp only [Array.data_toArray, Array.modifyLast_data, modifyLast_singleton, cons.injEq, and_true]
  apply Array.ext'
  simp only [Array.data_toArray, Array.append_data]
State after:
no goals

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
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₂)

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₂)
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₂)

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₂
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₂)
Tactic:
cases List.append_isPrefix_split lft (length l₁) with
| inl hinf => 
  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]
  have ⟨t, hinf⟩ := isPrefix_trans hinf take_isPrefix
  rw [← hinf]
  have hrw₁: s ++ delim ++ t ++ l₂ = s ++ delim ++ (t ++ l₂) := by simp only [append_assoc]
  have hrw₂: s ++ delim ++ t = s ++ delim ++ t := by simp only [append_assoc]
  rw [hrw₁, hrw₂, splitOnListAux_progress rgt, splitOnListAux_progress rgt]
  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₂
    
  rw [List.splitOnListAux_append t]
  . 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)]
  . 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]
  . apply le_refl
| inr hinf =>
  have hzero: length l₁ + 1 - length delim - length l₁ = 0 := by
    simp only [tsub_le_iff_right, ge_iff_le, add_le_add_iff_left, zero_le, nonpos_iff_eq_zero,
      tsub_eq_zero_iff_le]
    apply Nat.succ_le_of_lt
    simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, h₂, not_false_iff, length_pos_of_ne_nil]
  rw [List.drop_append_eq_append_drop, hzero, drop] at hinf
  have ⟨t, hinf⟩ := hinf
  unfold lastN at h
  exfalso
  apply h
  exists drop (length l₁ + 1 - length delim) s, t
  convert hinf using 3
  rw [Nat.sub_sub_eq_add_sub_of_le]
  apply Nat.succ_le_of_lt
  apply Nat.zero_lt_of_ne_zero
  simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, length_eq_zero, h₂, not_false_iff]
State after:
no goals

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]
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₁

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
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₁

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]
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₁

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]
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₁

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]
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₁

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]
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₁

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₂
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₁

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]
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₁

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)]
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₁

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]
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₁

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
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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
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₁

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]
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

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
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

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
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

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₂
State after:
no goals

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
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

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
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₂ = #[]

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'
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

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]
State after:
no goals

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)]
State after:
no goals

State before:
case true.inr
α : 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 : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) (l₁ ++ l₂)
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
have hzero: length l₁ + 1 - length delim - length l₁ = 0 := by
  simp only [tsub_le_iff_right, ge_iff_le, add_le_add_iff_left, zero_le, nonpos_iff_eq_zero,
    tsub_eq_zero_iff_le]
  apply Nat.succ_le_of_lt
  simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, h₂, not_false_iff, length_pos_of_ne_nil]
State after:
case true.inr
α : 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 : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) (l₁ ++ l₂)
hzero : length l₁ + 1 - length delim - length l₁ = 0
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)

State before:
case true.inr
α : 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 : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) (l₁ ++ l₂)
hzero : length l₁ + 1 - length delim - length l₁ = 0
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
rw [List.drop_append_eq_append_drop, hzero, drop] at hinf
State after:
case true.inr
α : 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 : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)

State before:
case true.inr
α : 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 : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
have ⟨t, hinf⟩ := hinf
State after:
case true.inr
α : 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✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)

State before:
case true.inr
α : 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✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
unfold lastN at h
State after:
case true.inr
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)

State before:
case true.inr
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
exfalso
State after:
case true.inr.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ False

State before:
case true.inr.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ False
Tactic:
apply h
State after:
case true.inr.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂

State before:
case true.inr.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
Tactic:
exists drop (length l₁ + 1 - length delim) s, t
State after:
case true.inr.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ - (length delim - 1)) l₁ ++ l₂

State before:
case true.inr.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ - (length delim - 1)) l₁ ++ l₂
Tactic:
convert hinf using 3
State after:
case e_a.e_a.e_a
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ length l₁ - (length delim - 1) = length l₁ + 1 - length delim

State before:
case e_a.e_a.e_a
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ length l₁ - (length delim - 1) = length l₁ + 1 - length delim
Tactic:
rw [Nat.sub_sub_eq_add_sub_of_le]
State after:
case e_a.e_a.e_a
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ 1 ≤ length delim

State before:
case e_a.e_a.e_a
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ 1 ≤ length delim
Tactic:
apply Nat.succ_le_of_lt
State after:
case e_a.e_a.e_a.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ 0 < length delim

State before:
case e_a.e_a.e_a.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ 0 < length delim
Tactic:
apply Nat.zero_lt_of_ne_zero
State after:
case e_a.e_a.e_a.h.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ length delim ≠ 0

State before:
case e_a.e_a.e_a.h.h
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: drop (length l₁ - (length delim - 1)) l₁ ++ l₂
heq : delim <:+: l₁ ++ l₂
s : List α
lft : s ++ delim <+: l₁ ++ l₂
rgt : ¬delim <:+: s ++ dropLast delim
hinf✝ : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) l₁ ++ l₂
hzero : length l₁ + 1 - length delim - length l₁ = 0
t : List α
hinf : drop (length l₁ + 1 - length delim) s ++ delim ++ t = drop (length l₁ + 1 - length delim) l₁ ++ l₂
⊢ length delim ≠ 0
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, length_eq_zero, h₂, not_false_iff]
State after:
no goals

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 : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) (l₁ ++ l₂)
⊢ length l₁ + 1 - length delim - length l₁ = 0
Tactic:
simp only [tsub_le_iff_right, ge_iff_le, add_le_add_iff_left, zero_le, nonpos_iff_eq_zero,
  tsub_eq_zero_iff_le]
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 : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) (l₁ ++ l₂)
⊢ 1 ≤ length delim

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 : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) (l₁ ++ l₂)
⊢ 1 ≤ length delim
Tactic:
apply Nat.succ_le_of_lt
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 : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) (l₁ ++ l₂)
⊢ 0 < length delim

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 : drop (length l₁ + 1 - length delim) s ++ delim <+: drop (length l₁ + 1 - length delim) (l₁ ++ l₂)
⊢ 0 < length delim
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, h₂, not_false_iff, length_pos_of_ne_nil]
State after:
no goals

State before:
case false
α : 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₂) = false
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
rw [← Bool.not_eq_true, isInfixOf_ext] at heq
State after:
case false
α : 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₂)

State before:
case false
α : 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 not_in_l₁: ¬ delim <:+: l₁  :=  by
  intro contr;
  apply heq
  apply List.isInfix_append_right_of_isInfix contr
State after:
case false
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
not_in_l₁ : ¬delim <:+: l₁
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)

State before:
case false
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
not_in_l₁ : ¬delim <:+: l₁
⊢ splitOnListAux delim (l₁ ++ l₂) #[] #[] h₂ =
    Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux delim l₁ #[] #[] h₂)
Tactic:
rw [splitOnListAux_nonmatching _ heq, splitOnListAux_nonmatching _ not_in_l₁]
State after:
case false
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
not_in_l₁ : ¬delim <:+: l₁
⊢ #[toArray (l₁ ++ l₂)] = Array.modifyLast (fun x => x ++ toArray l₂) #[toArray l₁]

State before:
case false
α : Type u_1
delim : List α
h₂ : delim ≠ []
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
heq : ¬delim <:+: l₁ ++ l₂
not_in_l₁ : ¬delim <:+: l₁
⊢ #[toArray (l₁ ++ l₂)] = Array.modifyLast (fun x => x ++ toArray l₂) #[toArray l₁]
Tactic:
apply Array.ext'
State after:
case false.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₂
not_in_l₁ : ¬delim <:+: l₁
⊢ #[toArray (l₁ ++ l₂)].data = (Array.modifyLast (fun x => x ++ toArray l₂) #[toArray l₁]).data

State before:
case false.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₂
not_in_l₁ : ¬delim <:+: l₁
⊢ #[toArray (l₁ ++ l₂)].data = (Array.modifyLast (fun x => x ++ toArray l₂) #[toArray l₁]).data
Tactic:
simp only [Array.data_toArray, Array.modifyLast_data, modifyLast_singleton, cons.injEq, and_true]
State after:
case false.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₂
not_in_l₁ : ¬delim <:+: l₁
⊢ toArray (l₁ ++ l₂) = toArray l₁ ++ toArray l₂

State before:
case false.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₂
not_in_l₁ : ¬delim <:+: l₁
⊢ toArray (l₁ ++ l₂) = toArray l₁ ++ toArray l₂
Tactic:
apply Array.ext'
State after:
case false.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₂
not_in_l₁ : ¬delim <:+: l₁
⊢ (toArray (l₁ ++ l₂)).data = (toArray l₁ ++ toArray l₂).data

State before:
case false.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₂
not_in_l₁ : ¬delim <:+: l₁
⊢ (toArray (l₁ ++ l₂)).data = (toArray l₁ ++ toArray l₂).data
Tactic:
simp only [Array.data_toArray, Array.append_data]
State after:
no goals

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₂
⊢ ¬delim <:+: l₁
Tactic:
intro contr
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₂
contr : delim <:+: l₁
⊢ False

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₂
contr : delim <:+: l₁
⊢ False
Tactic:
apply heq
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₂
contr : delim <:+: l₁
⊢ delim <:+: l₁ ++ l₂

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₂
contr : delim <:+: l₁
⊢ delim <:+: l₁ ++ l₂
Tactic:
apply List.isInfix_append_right_of_isInfix contr
State after:
no goals