Expose term-level simp/dsimp normalization primitive

[mitschabaude]

Motivation

While implementing elaborate_circuit_with, we used Lean meta dsimp on an expression to normalize a generated term before assigning it. This is useful beyond tactics that close goals: sometimes we want to simplify a term, keep the simplified term, and optionally keep the equality proof relating it to the original term.

A possible surface API could look like:

let ⟨x', hx⟩ := dsimp_term x only [explicit_circuit_norm]
-- x' : same type as x
-- hx : x = x'

let ⟨y', hy⟩ := simp_term y only [foo, bar]
-- hy : y = y'

For the common definitional-normalization case, a projection is enough:

let x' := (dsimp_term x only [explicit_circuit_norm]).1

Proposed implementation

Add a term elaborator, likely starting with the conservative dsimp_term version.

Implementation sketch:

1. Elaborate the input term, preserving the expected type when available.
2. Parse simp-style arguments, or initially support only only [...] for a smaller MVP.
3. Build a Simp.Context/dsimp context from those arguments.
4. Run meta-level normalization on the elaborated expression:

let r ← dsimp e dsimpCtx
let e' := r.expr

5. Return a pair containing the normalized expression and a proof. For dsimp, mkEqRefl e is often enough after definitional reduction; for full simp, use the proof returned by simp.
6. Add an expected type hint or check the normalized expression against the original expected type. If full simp changes the type only propositionally, either reject that case initially or return a cast/proof shape that makes transport explicit.

Notes

dsimp_term is the safer first primitive because the output should remain definitionally compatible with the input type. simp_term is more general, but it needs a careful story for proof transport and cases where the simplified expression no longer checks at the expected type by definitional equality.