induction la with
| nil => simp
| cons a la IH =>
  simp only [mem_cons, exists_eq_or_imp, decide_or]
  refine trans (s:=LE.le) countP_or_le_add ?_
  rewrite [length_cons, Nat.succ_eq_one_add]
  refine Nat.add_le_add ?_ IH
  refine countP_le_one_of_unique_nodup ?_ hnodup
  intro b₁ b₂ hb₁ hb₂
  cases of_decide_eq_true hb₁
  cases of_decide_eq_true hb₂
  rfl
α : Type u
β : Type v
inst✝ : DecidableEq β
la : List α
lb : List β
hnodup : Nodup lb
f : α → β
⊢ countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
no goals