Commit 2026-03-20 19:01 9bf5f0e4

fix: replace @[simp] on coe_toWeakDual/coe_toStrongDual with _apply lemmas (#36795) coe_toWeakDual and coe_toStrongDual stated equalities between bundled maps (toWeakDual x' = x'), which is not a useful simp normal form. This PR removes @[simp] from these lemmas and replaces them with pointwise _apply variants:

• toWeakDual_apply (x' : StrongDual R M) (y : M) : (toWeakDual x') y = x' y
• toStrongDual_apply (x : WeakDual k E) (y : E) : (toStrongDual x) y = x y These are the correct simp normal form, rewriting function application rather than bundled map equality. -->