default instance ignored in intro

Stream: mathlib4

[Dan Velleman]

Consider the following examples:

import Mathlib.Data.Set.Basic

attribute [default_instance] Set.instSingletonSet

example (a b : Nat) (h1 : a = b) : {a} ⊆ {b} := by
  intro (x : Nat)
  intro (h2 : x ∈ ({a} : Set Nat))
  rewrite [h1] at h2
  exact h2

example (a b : Nat) (h1 : a = b) : {a} ⊆ {b} := by
  intro (x : Nat)
  intro (h2 : x ∈ {a})
  rewrite [h1] at h2
  exact h2

The first example works. In the second, there's an error on the second intro:

type mismatch at `intro h2`has type
  x ∈ {a} : Prop
but is expected to have type
  x ∈ ?m.546 : Prop

It seems that the default instance attribute is being ignored in the intro tactic. Why?

Note also that the error message seems a bit muddled.