norm_smul regression?

Stream: mathlib4

[David Loeffler]

The following used to work, but stopped working some time in the last 5 days:

example (r : ℂ) (s : (ℂ × ℂ) →L[ℂ] ℂ) : ‖r • s‖ = ‖r‖ * ‖s‖ := by
  rw [norm_smul]

The change seems to have come from #11331. @Matthew Ballard any thoughts how to get this working again?

[Sébastien Gouëzel]

What if you do rw [norm_smul _ _], filling in one of the underscores if necessary?

[David Loeffler]

rw [norm_smul _ _] does not work (and it also does not work if one of the blanks is filled in but not the other). Filling in both blanks, i.e. rw [norm_smul r s], does work; it also works to specify the types but not the values, i.e. rw [norm_smul (α := ℂ) (β := (ℂ × ℂ) →L[ℂ] ℂ)].

I also found that example (r : ℂ) (s : (ℂ × ℂ) →L[ℂ] ℂ) : ‖r • s‖ = ‖r‖ * ‖s‖ := norm_smul _ _ gives an error message:

  norm_smul r s
has type
  ‖@HSMul.hSMul ℂ (ℂ × ℂ →L[ℂ] ℂ) (ℂ × ℂ →L[ℂ] ℂ) (@instHSMul ℂ (ℂ × ℂ →L[ℂ] ℂ) SMulZeroClass.toSMul) r s‖ =
    ‖r‖ * ‖s‖ : Prop
but is expected to have type
  ‖@HSMul.hSMul ℂ (ℂ × ℂ →L[ℂ] ℂ) (ℂ × ℂ →L[ℂ] ℂ) (@instHSMul ℂ (ℂ × ℂ →L[ℂ] ℂ) ContinuousLinearMap.instSMul) r s‖ =
    ‖r‖ * ‖s‖ : Prop

(I have no idea what this means or even whether it's relevant, but I'm providing it in case others can get something out of it.)

[Eric Wieser]

rw [norm_smul (_ : ℂ) (_ : (ℂ × ℂ) →L[ℂ] ℂ)] is the least precise that I can still get to work

[Matthew Ballard]

I was going to suggest filling in both arguments but I see that’s already been found.