α : Type u_2
l✝ : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
l : List α
f : α → β
x : α
⊢ countp (fun x_1 => x_1 == x) l ≤ countp ((fun x_1 => x_1 == f x) ∘ f) l
α : Type u_2
l✝ : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
l : List α
f : α → β
x : α
⊢ count x l ≤ count (f x) (map f l)
rw [count, count, countp_map]
no goals
α : Type u_2
l✝ : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
l : List α
f : α → β
x : α
⊢ countp (fun x_1 => x_1 == x) l ≤ countp ((fun x_1 => x_1 == f x) ∘ f) l
exact countp_mono_left <| by simp (config := {contextual := true})
no goals
α : Type u_2
l✝ : List α
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
l : List α
f : α → β
x : α
⊢ ∀ (x_1 : α), x_1 ∈ l → (x_1 == x) = true → ((fun x_2 => x_2 == f x) ∘ f) x_1 = true
simp (config := {contextual := true})