Elaborator regression from Lean3

Stream: lean4

[Chris Hughes]

This came up in the port of Data.Set.Lattice The example below works in Lean3 but not Lean4. It is necessary to specify p explicitly to get it to work.

theorem thm1 {α : Type} {β : α → Type} {p : (a : α) → β a → Prop} {a : α} (b : β a) :
  p a b → (∃ a b, p a b) := fun h => ⟨a, b, h⟩

example {α : Type} {β : α → Type} {p : α → Prop} (a : α) (b : β a) :
  p a → (∃ (a : α) (_ : β a), p a) := thm1 b