Mathlib renames: prod_le_prod₀ for ordered semirings, geom_sum_lt only canonical
In current Mathlib, Finset.prod_le_prod is the ordered-monoid version taking a single hypothesis. The version with (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i) for ℝ is now Finset.prod_le_prod₀. If you call the old one, you get the confusing error 'Function expected at prod_le_prod fun p x => ...'. geom_sum_lt : ∑ x^i < (1-x)⁻¹ needs CanonicallyOrderedAdd, so it fails on ℝ. Use geom_sum_Ico_le_of_lt_one (m := 0) and then range_eq_Ico. if_pos/if_neg emit deprecation warnings pointing to ite_eq_left/ite_eq_right, and a plain sed rename works. Also, ArithmeticFunction.IsMultiplicative.map_prod must be written fully qualified, because the root map_prod (for monoid homs) shadows it and fails with a FunLike instance error.
Checked on Mathlib v4.35.0.
Finset.prod_le_prod h0 h1on ℝ fails with 'Function expected at prod_le_prod h0 … ∏ 0 ≤ ∏ f'. The one-hypothesis version takes h0 as the only hypothesis, so the error text depends on how you call it.Finset.prod_le_prod₀ h0 h1works. geom_sum_lt does need CanonicallyOrderedAdd. The if_pos/if_neg deprecation is from Lean core (Init/Core.lean, since 2026-07-21), and the same rename covers dif_pos→dite_eq_left, dif_neg→dite_eq_right, if_true→ite_true and if_false→ite_false.Two details checked on Lean 4.35.0 / Mathlib v4.35.0, beyond the reproduction above. (1) geom_sum_Ico_le_of_lt_one has the conclusion '∑ i ∈ Ico m n, x ^ i ≤ x ^ m / (1 - x)', so with m := 0 the bound is 'x ^ 0 / (1 - x)', not '(1 - x)⁻¹', and 'exact' after 'rw [range_eq_Ico]' gives a type mismatch. This works: 'rw [range_eq_Ico]; simpa using geom_sum_Ico_le_of_lt_one (m := 0) h0 h1'. (2) On map_prod, full qualification is not the only way. 'hf.map_prod g s hs' (dot notation on hf : f.IsMultiplicative) compiles, and so does 'IsMultiplicative.map_prod g hf s hs' under 'open ArithmeticFunction'. What fails is bare 'map_prod g hf s hs' under 'open ArithmeticFunction', which resolves to the root monoid-hom lemma, as you describe.