Improve default field tactics by unfolding local circuit definitions

[mitschabaude]

Several circuit metadata fields rely on default tactics, but those defaults often fail when the circuit body is hidden behind a local main definition. During the SubcircuitsLawful spike, adding a narrow local unfold step:

try dsimp only [main]
simp only [circuit_norm]

made the default proof work for most circuits that previously needed explicit subcircuitsLawful fields. The number of remaining explicit proofs was surprisingly small and mostly limited to genuinely special cases, such as finite if trees, recursive circuits, or circuits whose proof needs unfolding of additional named helper mains.

We should investigate applying the same idea to other default fields, especially:

• localLength_eq
• output_eq
• subcircuitsConsistent
• defaults in ExplicitCircuit / ExplicitCircuits

The goal is not to make the defaults aggressive proof search. They should stay predictable and structural: unfold locally named circuit definitions such as main, then normalize with circuit_norm, and stop. This is similar in spirit to what circuit_proof_start already does for proof goals.

Things to check:

• Whether try dsimp only [main] is sufficient in structure default-field contexts, or whether we should use a quoted/unhygienic identifier approach like the tactic code.
• Which existing explicit field proofs become unnecessary after adding local unfolding.
• Whether this causes timeout/regression in large circuits.
• Whether the behavior should live as a shared tactic/helper instead of being duplicated across default field proofs.

Success criterion: fewer boilerplate explicit metadata proofs, no broad conjunction-splitting defaults, and full lake build still passing.

[mitschabaude]

Additional note from the GFC interaction-aware refactor: this should also cover named elaborated-circuit definitions behind projections, not just a local main definition.

Example shape:

def someElaboratedCircuit ... : ElaboratedCircuit F Input Output where
  main := ...
  ...

def someCircuit : GeneralFormalCircuit F Input Output where
  __ := someElaboratedCircuit ...
  ...

Default field goals are already phrased in terms of projected fields like main; the issue is that the named elaborated-circuit definition may not be unfolded by simp only [circuit_norm] / dsimp only [main]. This affects channel metadata defaults now, but the same improvement would be useful for many circuit proof defaults and ordinary circuit proofs.

This is a general proof-automation improvement, not something that has to be solved in the current PR slice.