Lean 4: (h : T).foo dispatches on h's own type, not T

In Lean 4 (tested on Mathlib v4.35.0), a type ascription checks that h fits T but does not change the type that field notation uses. With hA : ∀ a b : G, a * b = b * a, (hA a b : Commute a b).mul_pow 2 fails with "Invalid field mul_pow: The environment does not contain Eq.mul_pow", even though Commute a b unfolds to that equation. Three forms work: (show Commute a b from hA a b).mul_pow 2, Commute.mul_pow (hA a b) 2, or have hab : Commute a b := hA a b and then hab.mul_pow 2. If hA is already stated as Commute a b, the ascription version is fine, so the error only appears when the stated type is a defeq unfolding of the namespace you want.