> However if the prove relies on a bug like that, you'll be able to 'simplify' the proof a lot and you'll be able to proof contradictions.

I don't think this is true in general.

It's an issue I've already run into in personal work. I want to do a proof that involves some cases. It happens to the best of us.

In lean, the structure of a situation like this is that your single branch with a goal divides into multiple branches, all sharing the same original goal but including one additional premise that defines the branch.

Sometimes I know that for whatever reason one case I have to deal with is impossible. The most correct way to show that is to prove False and then apply False.elim. This is the equivalent, in a human proof, of saying "I don't have to address this situation, because it can never arise".

But it can be true that the premise defining the impossible case makes it very easy to "prove" the goal directly. And that's allowed too. The proof will still be just as valid if you map a logical path from a premise that can never be true to an inevitable consequence of that premise. But it's less informative and it lowers the quality of the proof. You may do it anyway because it's easier. This is the equivalent of saying "I don't know whether this situation can ever come up or not, but if it does I do know how to address it".

It would be nice to do the explicit proof by contradiction whenever possible. But in the general case it may be very far from obvious that a contradiction is possible.

I read your comment as claiming that if you can prove "false premise => goal", you can also prove "false premise => explicit contradiction", and I don't think this makes sense as a practical test. It's true in some sense, but discovering the proof of an explicit contradiction may be many orders of magnitude harder than discovering the proof of the goal. And in particular, I don't think it is necessarily the case that you will be able to prove a contradiction by simplifying the proof. You may need to add significant complexity.