cases Decidable.em (a.1 = x) with
| inl htrue =>
  simp only [htrue, ite_true, incrCounts, map]
  rw [if_pos]
  . apply ih
  . exact List.Mem.head _
| inr hfalse =>
  simp only [hfalse, ite_false, incrCounts, map]
  rw [ih]
  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
α : 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)
⊢ length
      (foldl (fun acc v => incrCounts acc v)
        (if a.fst = x then (a.fst, a.snd + 1) :: as else (a.fst, a.snd) :: incrCounts as x) xs) =
    length
      (if x ∈ map Prod.fst (a :: as) then uniqueAux xs (map Prod.fst (a :: as))
      else uniqueAux xs (x :: map Prod.fst (a :: as)))
no goals