Fishy instance finding

Stream: general

[Yaël Dillies]

I found there's something funny going on with continuous_linear_map.map_smul.
The following code throws an error asking for semiring (E →L[ℝ] ℝ)

import tactic
import data.real.basic
import algebra.module.linear_map
import analysis.convex.topology

variables {E : Type*} [normed_group E] [normed_space ℝ E]

lemma triv (l : E →L[ℝ] ℝ) (a : ℝ) (x : E) :
  l (a • x) = a • l x :=
by rw l.map_smul

while this works fine:

lemma triv (l : E →L[ℝ] ℝ) (a : ℝ) (x : E) :
  l (a • x) = a • l x :=
by rw l.map_smul _

l.map_smul_of_tower and l.map_smul' too throw peculiar instance requirements. I don't know if it's related, but I found that

theorem continuous_linear_map.map_smul {R : Type u_1} [semiring R] {M : Type u_2}
  [topological_space M] [add_comm_monoid M] {M₂ : Type u_3} [topological_space M₂]
  [add_comm_monoid M₂] [semimodule R M] [semimodule R M₂] (c : R) (f : M →L[R] M₂) (x : M) :
⇑f (c • x) = c • ⇑f x

had a weird argument order given the dot notation. I would have expected f to come before c.

[Shing Tak Lam]

I've only tried it on your example, but it seems like changing the order of c and f in continuous_linear_map.map_smul makes it work without needing the _.