## Stream: Is there code for X?

### Topic: by_cases foo, {finish}

#### Adam Topaz (Feb 18 2021 at 18:35):

When writing proofs on paper it is very common to write something like this: We may assume that $x \neq 0$ since the $x = 0$ follows easily, etc.

I can simulate this using

by_cases h : x = 0, { finish },
etc


This isn't bad, but I wonder whether we have a nicer way to do this that more closely resembles what I might write on paper.

#### Kevin Buzzard (Feb 18 2021 at 21:37):

You could probably write a can_assume tactic which just throws the kitchen sink at the negation of what you assumed (perhaps after simplifying \not (x != 0) to x = 0 etc)

#### Mario Carneiro (Feb 18 2021 at 21:41):

I would do have : x = 0 := by by_contra; kitchen_sink

#### Ruben Van de Velde (Feb 18 2021 at 21:43):

Followed by "hold on, this isn't actually that trivial"?

#### Mario Carneiro (Feb 18 2021 at 21:43):

actually, I guess the pattern here is that you want to assume !A in goal P assuming A -> P

#### Mario Carneiro (Feb 18 2021 at 21:44):

It might not be the case that !A is provable

#### Mario Carneiro (Feb 18 2021 at 21:44):

That said, given all the spaces where you have to say things I don't think you can improve on the structure provided by by_cases

#### Eric Wieser (Feb 18 2021 at 22:30):

tactic#nontriviality is a special case of what you're asking for I think

#### Adam Topaz (Feb 18 2021 at 22:31):

Yeah, that's the "We may assume our ring is nontrivial, because the result is trivially true for the trivial ring" tactic.

Last updated: May 17 2021 at 15:13 UTC