grind depending on Classical.choice

Stream: lean4

[Paul Mure]

I noticed that grind always depends on Classical.choice even for trivial proofs. Why is that?

[Henrik Böving]

One fundamental reason is that it relies on proof by contradiction which is (in full generality) derived from choice in Lean. Tactics built in core do not put in additional engineering effort to not use axioms in special cases where they do not need them.