How do I translate an infinite set in a subtype?

Stream: new members

[Ching-Tsun Chou]

Alas, I couldn't figure out how to prove the following painfully obvious proposition. Any ideas?

import Mathlib
example {X Y : Type} (f : X → Y) (s : Set X) (y : Y)
    (h : {x' : {x // x ∈ s} | f (↑x') = y}.Infinite) : {x | x ∈ s ∧ f x = y}.Infinite := by sorry

[Aaron Liu]

docs#Equiv.subtypeSubtypeEquivSubtypeInter

[Ching-Tsun Chou]

Thanks a lot!