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₂
⊢ 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]
Proof state after:
no goals