Lean is unable to infer ordered_smul instance from pi.ordered_smul'

[apurvnakade]

Lean is unable to automatically infer ordered_smul instance for fin n → ℝ from docs#ordered_smul'. This in turns leads to issues with defining the docs#convex_cone.positive in these vector spaces.

Zulip thread

mwe

import algebra.order.module
import data.real.basic

example : ordered_smul ℝ ℝ := infer_instance
noncomputable example : linear_ordered_field ℝ := infer_instance
example : mul_action_with_zero ℝ ℝ := infer_instance
example : ordered_add_comm_group ℝ := infer_instance

example : ordered_smul ℝ (fin 2 → ℝ) := infer_instance -- fails
example : ordered_smul ℝ (fin 2 → ℝ) := @pi.ordered_smul' ℝ _ (fin 2) ℝ _ _ _ -- works

Possible reasons suggested in the Zulip thread:

1. docs#pi.ordered_smul is true more generally without needing linear_ordered_field. (This is most certainly true. But it is not clear if this is the reason for the bug.)
2. docs#ordered_smul should only assume docs#has_smul, not docs#smul_with_zero.

[apurvnakade]

Closed by #16131