Error in 2nd subst example

[ketilwright]

This generates "compile" errors

namespace Hidden
theorem subst {α : Type u} {a b : α} {p : α → Prop} (h₁ : Eq a b) (h₂ : p a) : p b :=
  match h₁ with
  | rfl => h₂
end Hidden

I suspect what's meant is

theorem subst {α : Type u} {a b : α} {p : α → Prop} (h₁ : Eq a b) (h₂ : p a) : p b :=
  match h₁ with
  | .refl => h₂

Or perhaps:

theorem subst {α : Type u} {a b : α} {p : α → Prop} (h₁ : Eq a b) (h₂ : p a) : p b :=
  match h₁ with
  | Hidden.Eq.refl => h₂

"rfl" is probably a typo. Without a prepended . or Hidden.Eq. on refl there are warnings in the infoview:

Local variable 'refl' resembles constructor 'Hidden.Eq.refl' - write '.refl' (with a dot) or 'Hidden.Eq.refl' to use the constructor.
note: this linter can be disabled with set_option linter.constructorNameAsVariable false