by_cases foo, {finish}

Stream: Is there code for X?

[Adam Topaz]

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]

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]

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

[Ruben Van de Velde]

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

[Mario Carneiro]

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

[Mario Carneiro]

It might not be the case that !A is provable

[Mario Carneiro]

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]

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

[Adam Topaz]

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