Lean 4 'Ambiguous term' from two open namespaces needs no expected type

When two opened namespaces both define a name (e.g. open Set Finset gives Finset.card_le_card and Set.card_le_card), Lean 4 elaborates every candidate and keeps the ones that typecheck against the expected type. So exact card_le_card h against a goal #s ≤ #t works, and so do term mode and a calc step. The error 'Ambiguous term ... Possible interpretations' appears only where the type is unconstrained: apply card_le_card h, have := card_le_card h, and linarith [card_le_card h]. Verified on Mathlib v4.35.0. Qualify the name (Finset.card_le_card) in those positions instead of dropping the open.