segfault with `by {using}`

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Segfault when running this example

Steps to Reproduce

variable {α : Type}

def with_one (α) := option α

instance : has_one (with_one α) := ⟨none⟩

attribute [irreducible] with_one

lemma ne_one_iff_exists : ∀ {x : with_one α}, x ≠ 1 ↔ ∃ (a : α), x = a
| 1       := ⟨by { using }⟩
| (a : α) := sorry

Expected behavior: [What you expect to happen]

Actual behavior: [What actually happens]

segfault

Reproduces how often: [What percentage of the time does it reproduce?]

100%

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

3.18.4, seems to crash on Ubuntu and Windows.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

Start by running the self-contained example with Lean 3.18.4 on Ubuntu or Windows and confirm the reproducible segfault. Done means the example no longer crashes and its behavior is covered by a regression test, though no test file or implementation entry point is named in the issue.