induction xs generalizing cs with
| nil =>
  simp [uniqueAux]
  rw [←Nat.add_one,
      Nat.add_assoc,
      Nat.add_comm (length cs),
      ←Nat.add_assoc]
| cons z zs ih =>
  have rearrange_mem :
    (z ∈ cs ++ x :: (as ++ [y])) ↔ (z ∈ cs ++ y :: x :: as) := by
    apply Iff.intro
    . intros h
      cases mem_append_iff.mpr h with
      | inl hcs => exact List.mem_append_front _ _ _ hcs
      | inr hcons =>
        apply List.mem_append_back
        rw [←cons_append] at hcons
        cases mem_append_iff.mpr hcons with
        | inl hxas => exact List.Mem.tail _ hxas
        | inr hy =>
          cases hy with
          | tail _ _ => contradiction
          | head _ => exact List.Mem.head _
    . intros h
      cases mem_append_iff.mpr h with
      | inl hcs => exact List.mem_append_front _ _ _ hcs
      | inr hcons =>
        apply List.mem_append_back
        cases hcons with
        | head _ =>
          apply List.Mem.tail
          apply List.mem_append_back
          apply (List.mem_singleton_iff y y).mpr rfl
        | tail _ hcons' =>
          rw [←cons_append]
          exact List.mem_append_front _ _ _ hcons'
  simp only [uniqueAux]
  cases Decidable.em (z ∈ cs ++ x :: (as ++ [y])) with
  | inl hin =>
    simp only [hin, rearrange_mem.mp hin, ite_true]
    apply ih
  | inr hout =>
    simp only [hout, rearrange_mem.not_iff_not_of_iff.mp hout, ite_false]
    have rw_help (stuff) : (z :: (cs ++ stuff)) = ((z :: cs) ++ stuff) := rfl
    rw [rw_help, rw_help]
    apply ih
α : Type u_1
inst✝ : DecidableEq α
x y : α
as xs cs : List α
⊢ length (uniqueAux xs (cs ++ x :: (as ++ [y]))) = length (uniqueAux xs (cs ++ y :: x :: as))
no goals