Eliminating coercions

Stream: new members

[Sandy Maguire]

I have the following context

nd: ℕ
x': ↑n ^ 2 = 2 * ↑d ^ 2
⊢ n ^ 2 = 2 * d ^ 2

where the coe on n and d are both at \R. how can i prove the goal from x'?

[Kevin Buzzard]

Try assumption_mod_cast.

[Sandy Maguire]

that does it. how could i have found this for myself?

[Kevin Buzzard]

Just keep asking.

[Kevin Buzzard]

The cast tactics are probably mentioned in the API documentation

[Sandy Maguire]

happy to continue asking, tho i feel like a bit of a burden!!

[Kevin Buzzard]

The one you need to know in this case is norm_cast at x'.

[Kevin Buzzard]

There's a relatively small number of techniques and if you keep trying to prove stuff then eventually you see them all

[Sandy Maguire]

that's helpful. thank you!

[Bryan Gin-ge Chen]

tactic#norm_cast mentions assumption_mod_cast and the other *_mod_cast tactics.

[Kevin Buzzard]

I used to think it was kind of hopeless trying to keep up with the new tactics, but actually over the last few months there are not so many new ones which have appeared, partly because we now have most of the ones we were desperate for (like assumption_mod_cast) and partly because I suspect the tactic writers are reluctant to work hard on Lean 3 now Lean 4 is here. Mathematically we're still missing a Groebner basis tactic, which I don't think anyone is working on ( :-( ), our omega tactic to solve stuff on nat is quite buggy, and some people want more general automation tactics because they're jealous of tactics in other provers. Gabriel was working on a hammer tactic but again I'm unclear about whether this will happen before Lean 4. Maybe just browsing the tactics in the API docs might be useful to you, I remember doing this quite a bit when I was learning.

[Patrick Massot]

Sandy, if you are serious about this you can also watch the full Lean for the curious mathematician series on Youtube (except the meta-programming part). This is not so long since most of the week were exercises sessions that are not recorded. This covers the norm_cast family of tactics.