push_neg takes non-intuitionistic step

Stream: new members

[Michael Beeson]

h6: ¬¬(Nc M (Φ M (𝕋 M m)) = two ∨ Nc M (Φ M (𝕋 M m)) = three)

Then push_neg at h6 removes the double negation, instead of just pushing one negation. Up until now, I have never seen
push_neg take an intuitionistically incorrect step. Now I need to be triple-vigilant to check the axioms used in my proofs.
Too bad about this as offhand I do not know how to push just the one negation.

[Ruben Van de Velde]

Perhaps the documentation should be clearer on that

[Johan Commelin]

@Michael Beeson I am afraid that you are fighting uphill, because mathlib is very decidably classical. Supporting intuitionistism is not on one of our priorities, and hence we also don't point out every occurence of classical or intuitionistic arguments.

[Yakov Pechersky]

Maybe use the lemmas that do the rewriting instead of push_neg?