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
case cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
rearrange_mem : z ∈ cs ++ x :: (as ++ [y]) ↔ z ∈ cs ++ y :: x :: as
⊢ length
      (if z ∈ cs ++ x :: (as ++ [y]) then uniqueAux zs (cs ++ x :: (as ++ [y]))
      else uniqueAux zs (z :: (cs ++ x :: (as ++ [y])))) =
    length
      (if z ∈ cs ++ y :: x :: as then uniqueAux zs (cs ++ y :: x :: as) else uniqueAux zs (z :: (cs ++ y :: x :: as)))
no goals