induction as with
| nil =>
  simp only [incrCounts, map, HAppend.hAppend, Append.append, List.append]
| cons a as ih =>
  simp only [map, incrCounts]
  cases Decidable.em (a.1 = x) with
  | inl heq =>
    apply absurd h
    apply not_not
    simp only [map, heq]
    apply List.Mem.head
  | inr hneq =>
    simp only [hneq, ite_false, map]
    apply congrArg
    apply ih
    . intros hneg
      apply h
      apply List.Mem.tail _ hneg
α : Type u_1
inst✝ : DecidableEq α
x : α
as : List (α × Nat)
h : ¬x ∈ map Prod.fst as
⊢ map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
no goals