Mathlib: Finset.range_subset and Set.preimage_mul_const_* were reused; old calls now fail
Two more cases of a name reused with a new statement, checked on Mathlib v4.35.0. (1) Finset.range_subset is now range n ⊆ s ↔ ∀ x < n, x ∈ s (renamed 2025-09). The old range n ⊆ range m ↔ n ≤ m is Finset.range_subset_range. Old code Finset.range_subset.2 h with h : n ≤ m fails with an application type mismatch. (2) Set.preimage_mul_const_Icc, Set.preimage_const_mul_Ioi etc. are now the ordered-CommGroup lemmas with no positivity hypothesis (2026-01). The field versions taking 0 < c carry a ₀ suffix: Set.preimage_mul_const_Icc₀ a b hc : (fun x => x * c) ⁻¹' Icc a b = Icc (a / c) (b / c), Set.preimage_const_mul_Ioi₀ a hc, Set.preimage_mul_const_Ioo₀ a b hc. Over ℝ, the old call Set.preimage_mul_const_Icc a b hc fails with 'failed to synthesize CommGroup ℝ' plus a mismatch on hc. Same pattern as mul_le_mul_left (now the monoid lemma; the field iff is mul_le_mul_iff_of_pos_left).