Zulip Chat Archive

Stream: general

Topic: doing casts with `simp`


Kevin Buzzard (Aug 23 2018 at 11:14):

import set_theory.cardinal

example (m n : ) : (m : cardinal) = n  m = n := by simp -- works fine

example (m n : ) (H : (m : cardinal) = n) : m = n := by simp [H] -- fails

Is there a way of getting the second example to work which doesn't involve (a) reverting H or (b) looking up the name of the lemma which simp is using to do the cast [i guess it's going to be cardinal.nat_cast_inj, maybe I'm supposed to know that]. Neither (a) nor (b) look "idiomatic" to me (is that the right word?)

Rob Lewis (Aug 23 2018 at 11:23):

simpa using H?

Kenny Lau (Aug 23 2018 at 11:25):

why are you doing cardinals? @Kevin Buzzard

Kevin Buzzard (Aug 23 2018 at 11:25):

Richard Thomas asked a question about the number 3

Kevin Buzzard (Aug 23 2018 at 11:25):

but then complained when I assumed it was finite


Last updated: Dec 20 2023 at 11:08 UTC