cases acc with
| nil =>
  simp only [incrCounts, map, List.not_mem_nil, ite_false]
  apply ih
| cons a as =>
  simp only [incrCounts]
  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
α : 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))
acc : List (α × Nat)
⊢ length (foldl (fun acc v => incrCounts acc v) (incrCounts acc x) xs) =
    length (if x ∈ map Prod.fst acc then uniqueAux xs (map Prod.fst acc) else uniqueAux xs (x :: map Prod.fst acc))
no goals