feat: restrict simpa using h close to reducible transparency

[kim-em]

This PR makes simpa using h require the simplified h and the simplified goal to match at reducible transparency, rather than at the ambient (default/semireducible) transparency used previously. This makes simpa using h more predictable: it no longer succeeds via incidental β/δ-reduction at the closing step, so adding new simp lemmas is less likely to silently break unrelated simpa calls.

The new behaviour is gated by a backward-compat option backward.simpa.using.reducibleClose (defaulting to true); set it to false per-call, per-section, or globally to restore the previous behaviour. Two existing in-tree tests (getElemV.lean, scopeCacheProofs.lean) relied on the old behaviour; they are annotated with the option and an explanatory comment so the breakage is visible.

The change wraps only the precondition isDefEq check inside Lean.Elab.Tactic.Simpa.evalSimpa. The downstream metavariable-assignment check (MVarId.checkedAssign → checkTypesAndAssign) still escalates transparency internally, but the reducible-transparency precondition strictly dominates it, so the escalation is benign.

This addresses Jovan's point (1) of the proposal in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.20code.20quality.3A.20simpa, narrowing what simpa can do without the broader behaviour change of also using h as a simp lemma. The PR is branched from nightly-with-mathlib so Mathlib breakage data can be gathered via the existing nightly-testing infrastructure.

🤖 Prepared with Claude Code