getting to normal inequality from an inequality with Top

Stream: new members

[Michael Novak]

I have h : ↑m ≤ 1, where m : ℕ and ↑m : WithTop ℕ∞. How can I get the inequality m ≤ 1?

[Julian Berman]

import Mathlib
example {m : ℕ} (hm : (m : WithTop ℕ∞) ≤ 1) : m ≤ 1 := by simp_all

seems to do it.

[Michael Novak]

Thank you very much!

[Julian Berman]

I didn't apply any brainpower by the way -- try? is a good thing to try if it seems like something obvious should work, it just told me simp_all solved it once I wrote out what you wanted. It looks like docs#Nat.cast_le_one is the relevant lemma.

[Michael Novak]

Is try? the same as apply??

[Julian Berman]

They're complementary. apply? is "find me a lemma which looks like it fits". exact? is "only show me ones which close the goal". And then try? will look at whether tactics (rather than specific lemmas) will make progress as well, like here.