Mathlib 2026: lemma names reused with a new statement (type error, no deprecation warning)

When Mathlib renames X to X' and then gives the freed name X a different statement, old code gets a type mismatch or 'Function expected' instead of a deprecation warning. Cases checked on v4.35.0: (1) ContinuousLinearMap.coe_comp is now ⇑(h ∘SL f) = h ∘ f (the old primed lemma; coe_comp' is a deprecated alias). The LinearMap-coercion version is now ContinuousLinearMap.toLinearMap_comp (2026-06). (2) Pi.lift_π is now Pi.lift (Pi.π f) = 𝟙 _. The old Pi.lift p ≫ Pi.π f b = p b is Pi.lift_comp_π, and simp still proves it (2026-09). (3) Order.isSuccLimit_iff is now the Preorder statement IsSuccLimit a ↔ ¬IsMin a ∧ IsSuccPrelimit a. The a ≠ ⊥ form is Order.isSuccLimit_iff_of_orderBot (2026-04). (4) Finset.prod_le_prod, prod_lt_prod, prod_lt_prod_of_nonempty and finprod_le_finprod are now ordered-monoid lemmas, and the nonnegative-semiring versions carry a ₀ suffix (PR #39692, 2026-09). Over ℝ the old call fails with 'Function expected' or MulLeftMono ℝ. (5) MonoidHom.restrict now takes a Set.MapsTo proof; domain restriction is MonoidHom.domRestrict (2026-07). Related: MvPolynomial.coeff was deleted outright, so use p.coeff m. How to find more: in rename/deprecate commits, look for a declaration that is removed and re-added under the same name with a different statement, where the old statement reappears under a new name.