Stating continuity of coe_fn

Stream: maths

[Moritz Doll]

I have problems stating the following property of coe_fn:

import topology.algebra.module.weak_dual
import linear_algebra.dual
import analysis.normed.normed_field

variables {𝕜 E : Type*}

variables [normed_field 𝕜] [add_comm_group E] [module 𝕜 E]

instance add_monoid_hom_class_alg_weak_dual :
  add_monoid_hom_class (weak_bilin (module.dual_pairing 𝕜 E)) E 𝕜 :=
module.add_monoid_hom_class 𝕜 E

variables (f : weak_bilin (module.dual_pairing 𝕜 E))

#check (f : (E → 𝕜)) -- works fine

lemma is_uniform_continuous_weak_coe :
  uniform_continuous (coe_fn : (weak_bilin (module.dual_pairing 𝕜 E)) → (E → 𝕜)) :=
begin
  sorry,
end

The last lemma fails with

failed to synthesize type class instance for
has_coe_to_fun (weak_bilin (module.dual_pairing 𝕜 E))
    (λ (ᾰ : weak_bilin (module.dual_pairing 𝕜 E)), E → 𝕜)

I know that it is usually better to not explicitly mention coe_fn, but here I see no other way to state the lemma.