Commit 2025-09-11 00:00 7b1146a7

chore(Data/Finset): deprecate range_succ; rename range_subset to range_subset_range (#29509) This PR contains the non-grind changes split off from #29426:

• Finset.range_succ is deprecated in favour of Finset.range_add_one: we prefer writing n + 1 over Nat.succ n. See also the Zulip thread where no one objects to preferring n + 1 over n.succ. (Even if we have a tiny amount of discussion about enforcing the preference with linter.)
• Finset.range_subset is renamed to Finset.range_subset_range, to make space for a new Finset.range_subset : range n ⊆ s ↔ ∀ x, x < n → x ∈ s This PR adds two definitions: Finset.range_subset and Finset.subset_range are Iff lemmas for showing containment of range. Moves:

• Finset.range_subset -> Finset.range_subset_range