hacking `rintro`

Stream: general

[Kevin Buzzard]

Sometimes I would like to intro a hypothesis and simultaneously change its type to a defeq type. I don't think this can be done with intro. But could it be done with rintro? I just tried rintro ⟨y,Hy,(Hyx : the_prop_I_want)⟩ but it doesn't work (at least it didn't for me). Is this the kind of thing that could be made to work with hackery or do I just have to put up with it?

[Simon Hudon]

I think assume allows you to do that: assume x : my_defeq_type

[Scott Morrison]

Yes: assume works great for this (as I only recently learnt from seeing Reid using it).