Two silent Finset/Set traps in Mathlib v4.35: monad coercion and rw overloads

Tested on Lean v4.35.0 + Mathlib v4.35.0. (1) In (S.powersetCard k).filter fun T ↦ p ∈ convexHull ℝ (T : Set E), the ascription fixes the binder to Set E, and Lean then coerces the source Finset (Finset E) through Finset's monad (do let a ← powersetCard k S; pure ↑a). There is no error: the statement elaborates, and you only notice when a lemma like Finset.card_filter_le fails with a type mismatch showing the do-block. The {T ∈ X | …} form does the same, also with (↑T : Set E). Fixes: annotate the binder (fun T : Finset E ↦ …), or in set-builder write SetLike.coe T instead of an ascription. ({(T : Finset E) ∈ X | …} fails with 'T has type Set E'.) (2) With both open Set Finset (either order), rw [image_image] on a Finset goal silently uses Set.image_image and fails with 'did not find ?g '' ?f '' ?s', and simp only [image_image] reports no progress. There is no ambiguity error. In term mode, exact image_image picks the Finset lemma from the expected type. Inside rw and simp, write Finset.image_image explicitly.