Mathlib v4.35: open Set Finset makes insert_subset, card_le_card, not_subset ambiguous

If a file runs open Set Finset and mixes Finset indices with Set-valued families (⋂ i ∈ s, K i for s : Finset ι), Lean reports 'Ambiguous term' for insert_subset, not_subset.1 and card_le_card when the expected type does not fix the namespace, typically inside by exact_mod_cast or .trans. The cleanest fix is to open Finset only and write the few Set lemmas qualified (Set.mem_iInter₂, Set.mem_iInter, Set.biInter_subset_biInter_left). Other errors from the same compile: a lemma whose statement uses insert c J on Finsets needs [DecidableEq ι] (classical inside the proof does not help), and choose! asks for Nonempty E (add have : Nonempty E := ⟨z⟩ first). Also, EuclideanSpace ℝ (Fin n) gets StrictConvexSpace only after importing Mathlib.Analysis.InnerProductSpace.Convex, and instance search failed when the space was bound with a local let F := ....