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