Mathlib v4.36.0-rc2 deprecations: FunLike.coe_* for SimpleFunc/BCF, Subgroup.derivedSeries, Iic_false

Upgrading from v4.35.0 to v4.36.0-rc2, tested on both. About 330 new deprecations are dated 2026-10-13 to 10-27. Batches besides the *_nonzero → *_ne_zero rename: (1) Per-type coercion lemmas become generic. MeasureTheory.SimpleFunc.coe_add and BoundedContinuousFunction.coe_add say 'Use FunLike.coe_add', and BoundedContinuousFunction.add_apply says 'Use add_apply'. That covers 24 deprecations in SimpleFunc.lean, 22 in ContinuousMap/Bounded/Basic.lean and 12 in ZeroAtInfty.lean. The generic forms only work on rc2. On v4.35.0, rw [FunLike.coe_add] fails for BoundedContinuousFunction, SimpleFunc and ZeroAtInftyContinuousMap ('failed to synthesize IsAddApply (BoundedContinuousFunction α ℝ) α ℝ'), and rw [add_apply] fails for BoundedContinuousFunction. (2) Root derivedSeries and derivedSeries_zero → Subgroup.derivedSeries, Subgroup.derivedSeries_zero (11 in Solvable.lean). (3) Set.Iic_False/Ioi_True etc. → lowercase Set.Iic_false, Set.Ioi_true. (4) ZMod.coe_int_mul_inv_eq_one → ZMod.intCast_mul_inv_eq_one (same statement). (5) 30 ENNReal.tsum_* lemmas → root CompleteLattice lemmas (separate note). The old names still work on rc2 with a warning, so keep them in code that must build on both versions. simp closes (f + g) x = f x + g x for BoundedContinuousFunction on both.