Zulip Chat Archive

Stream: new members

Topic: Cases on hidden argument

view this post on Zulip Andre Knispel (Aug 15 2020 at 09:50):

I'm having a hypothesis that uses dite, and I'm trying to reduce it by using cases, but I've only managed to get proofs that the condition holds or doesn't hold, but I couldn't reduce dite so far. I assume if I had @dite h d x y, cases d would work, but I don't have d in context right now (at least not conveniently). How would I reduce dite?

view this post on Zulip Kevin Buzzard (Aug 15 2020 at 09:54):

dif_pos and dif_neg for refined control and split_ifs for a blunt instrument

Last updated: May 10 2021 at 19:16 UTC