New-style dot notation and pi types

Stream: mathlib4

[Yury G. Kudryashov]

The following #mwe fails:

variable [LE α] [LE β] [LE γ]

def Monotone (f : α → β) : Prop := ∀ ⦃x y⦄, x ≤ y → f x ≤ f y

theorem Monotone.comp {g : β → γ} {f : α → β} (hg : Monotone g)
    (hf : Monotone f) : Monotone (g ∘ f) := fun _ _ h => hg (hf h)

example {f : α → α} (h : Monotone f) : Monotone (f ∘ f) := .comp h h

[Yury G. Kudryashov]

It seems that Lean intros as many variables as it can before looking for new style dot notation. Is it intentional? Is it documented?

[Yury G. Kudryashov]

@Mario Carneiro @Gabriel Ebner :up:

[Mario Carneiro]

it doesn't sound intentional

[Mario Carneiro]

it does sound like there is a pretty large search space of potential interpretations though

[Yury G. Kudryashov]

Do you often have many stages with named output type?

[Reid Barton]

is it related to implicit lambdas?

[Yury G. Kudryashov]

No, Lean just intros everything it can before trying new style dot notation.

[Yury G. Kudryashov]

I'm OK with "try NS.name if the current goal is a named type NS, then intro everything we can".

[Yury G. Kudryashov]

This doesn't increase the search space too much.