dot notation and coe_to_Sort

Stream: general

[Sebastien Gouezel]

Currently, dot notation does not work for objects living in a subgroup, for instance Lp (in measure theory):

import measure_theory.l1_space
import measure_theory.lp_space

namespace measure_theory
open topological_space

variables {α : Type*} [measurable_space α] [normed_group α] [borel_space α]
[second_countable_topology α] {μ : measure α}

lemma Lp.foo (f : Lp α 1 μ) : integrable f μ := sorry

lemma bar (f : Lp α 1 μ) : integrable f μ := f.foo -- fails

end measure_theory

The reason is that when one writes f : Lp α 1 μ then f is not of the type Lp α 1 μ (this is a bundled subgroup), but of type ↥(Lp α 1 μ), with the little arrow indicating a coercion to Sort (here, a subtype of the space of almost everywhere defined functions). So, when one writes f.foo, Lean complains:

invalid field notation, 'foo' is not a valid "field" because environment does not contain 'coe_sort.foo'

And this is completely normal. But really frustrating. Is there a way to make Lean understand dot notation in this kind of context?