Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The case name is unnecessarily long when deconstructing many parts.

Context

Example:

example (h : ∃ a b c d e f g : ℕ, False ∨ False) : False := by
  obtain ⟨a, b, c, d, e, f, g, h | h⟩ := h
  · sorry
  · sorry

The goals are now labelled case intro.intro.intro.intro.intro.intro.intro.inl and case intro.intro.intro.intro.intro.intro.intro.inr.

This happens surprisingly often to me, particularly when I deconstruct many existentials: I just had a case where it was named intro.intro.intro.intro.mk.mk.intro.intro.inr.twice where inr.twice is the only meaningful part of the label.

Steps to Reproduce

1. Code as above

Expected behavior:
Desirable behaviour here would be that when deconstructing an inductive which has exactly one constructor, nothing is appended to the case name. In this case, the goals would be labelled case inl and case inr.

Actual behavior:
The goals are labelled case intro.intro.intro.intro.intro.intro.intro.inl and case intro.intro.intro.intro.intro.intro.intro.inr.

Versions

Using live.lean-lang.org:
Lean 4.16.0-rc1
Target: x86_64-unknown-linux-gnu

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.