cases Decidable.em (x ∈ map Prod.fst as) with
| inl hin =>
  have : x ∈ a.1 :: map Prod.fst as := List.Mem.tail _ hin
  simp only [this, ite_true, map, uniqueAux]
  apply congrArg
  apply congrArg
  apply congrArg
  exact map_fst_incrCounts_eq_map_fst x as hin
| inr hout =>
  have : ¬ (x ∈ a.1 :: map Prod.fst as) := by
    intros hneg; cases hneg; repeat contradiction
  simp only [this, ite_false, map]
  rw [map_fst_incrCounts_eq_cons_fst _ _ hout]
  apply List.length_uniqueAux_congr_append_cons_acc _ _ _ _ []
case cons.cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
hfalse : ¬a.fst = x
⊢ length (uniqueAux xs (map Prod.fst ((a.fst, a.snd) :: incrCounts as x))) =
    length
      (if x ∈ a.fst :: map Prod.fst as then uniqueAux xs (a.fst :: map Prod.fst as)
      else uniqueAux xs (x :: a.fst :: map Prod.fst as))
no goals