Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
@KevinBuzzard Even if I had proved 2 > 0 on the previous line, I had to prove it again on this line -- Maybe this part of Lean should have been fixed instead? I know nothing about proof assistants, but this sounds totally unreasonable.
@none That example is not very good IMHO. Those existentially quantified variables could simply be replaced by Skolem functions of the variables that they actually depend on.
