help wanted porting Algebra.Order.Module

Stream: mathlib4

[Casavaca]

https://github.com/leanprover-community/mathlib4/pull/1573

simpNF linter failed to simp on left hand side of another file Mathlib.Algebra.Order.SMul:

@[simp]
theorem lowerBounds_smul_of_pos (hc : 0 < c) : lowerBounds (c • s) = c • lowerBounds s :=
  (OrderIso.smulLeft _ hc).lowerBounds_image
#align lower_bounds_smul_of_pos lowerBounds_smul_of_pos

example (hc : 0 < c) : lowerBounds (c • s) > 0 := by
        simp only [lowerBounds_smul_of_pos] -- Does not change the goal. But `rw [...]` Does

[Johan Commelin]

What are the types of c and s?

[Casavaca]

s : Set M
c : 𝕜