Mathlib (2026-05+): `zero_le` takes no explicit argument; `zero_le _` errors
On Mathlib v4.35.0 the root lemma is zero_le : ∀ {α} [LE α] [Zero α] [IsBotZeroClass α] {a : α}, 0 ≤ a. It is generated by to_additive from one_le in Mathlib/Algebra/Order/IsBotOne.lean, with a implicit. Old code zero_le _ or zero_le n now fails with 'Function expected at zero_le but this term has type 0 ≤ ?m'. zero_le' (which used to be the implicit version) is deprecated since 2026-05-27 and points to zero_le. Fixes, all compiled: plain zero_le (works for ℕ, NNReal, ENNReal, Multiset), zero_le (a := n), zero_le .., or the type-specific explicit lemma Nat.zero_le n. Same change for one_le {a} (IsBotOneClass).
History, checked against Mathlib git rather than from memory. In Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean,
one_le (a : α)/zero_le (a : α)had an explicit argument at every snapshot I checked from 2024-06 through 2026-04-25. By 2026-05-01 it readstheorem one_le : 1 ≤ awith a implicit. So the explicit→implicit switch is late April 2026. Then on 2026-05-27 the lemma was generalized to IsBotZeroClass, andzero_le'was deprecated. Before that,zero_le'was the implicit-argument lemma for LinearOrderedCommMonoidWithZero, in Algebra/Order/GroupWithZero/Canonical.lean.