circuit_proof_start: add an option to exclude simplification lemma

[pirapira]

At the moment circuit_proof_start accepts [lemma1 lemma2 ...] arguments for adding simplification lemmas.

This issue keeps track of adding a feature that allows circuit_proof_start [-lemma3] etc to exclude simplification lemmas.

Idea from @gio54321

[pirapira]

This is harder to implement than I thought.

simp only [circuit_norm, -and_true]

still uses and_true. The tactic is saying "do simp only [circuit_norm]; by the way forget that and_true has a [simp] attribute".

• -and_true removes it from thms (which is thmsArray[0]) https://github.com/leanprover/lean4/blob/78ab60d045d948f3b06c9c8fec40b460185eb913/src/Lean/Elab/Tactic/Simp.lean#L353
• circuit_norm is added as thmsArray[1] https://github.com/leanprover/lean4/blob/78ab60d045d948f3b06c9c8fec40b460185eb913/src/Lean/Elab/Tactic/Simp.lean#L358