Stray `.` in goal view

Stream: general

[Eric Wieser]

What's going on here?

import data.finset.basic

theorem foo (m: ℕ) : ∀ {X Y : finset (fin m → ℕ)},
  X ∈ ({∅} : set (finset (fin m → ℕ))) → Y ⊆ X → Y ∈ ({∅} : set (finset (fin m → ℕ)))
| X Y rfl := sorry -- Y ⊆ .∅ → Y ∈ {∅}

What's the .∅ coming from?

[Mario Carneiro]

That's most likely a remnant of the inaccessible pattern in place of X

[Eric Wieser]

It goes away if I put by before sorry

[Eric Wieser]

But not if I use id sorry

[Mario Carneiro]

Here's an example of using an inaccessible pattern:

theorem foo (m: ℕ) : ∀ {X Y : finset (fin m → ℕ)},
  X ∈ ({∅} : set (finset (fin m → ℕ))) → Y ⊆ X → Y ∈ ({∅} : set (finset (fin m → ℕ)))
| .(∅) Y rfl := sorry -- Y ⊆ .∅ → Y ∈ {∅}

[Mario Carneiro]

this looks like a side effect of the way the printing of the expected type works