Clearly finite bounded set, but how can prove finiteness?

Stream: general

[SnO2WMaN]

import Mathlib.Data.Finite.Defs

example : Set.Finite { Nat.toFloat x | x ≤ 2 } := by sorry;

This might be very oblivious, but I didn't find good way to prove. How can prove? and I hope that tauto_set will solve like this trivial problems...

[Zhang Qinchuan]

You can write your set as Nat.toFloat '' Set.Icc 0 2, then it is trivial:

import Mathlib

example : Set.Finite <| Nat.toFloat '' Set.Icc 0 2 := by
  exact Set.toFinite ..

[SnO2WMaN]

It works, I didn't import Mathlib.Order.Interval.Finset.Nat. Thanks.