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.
  • Reduced the issue to a self-contained, reproducible test case.

Description

PANIC at Lean.Meta.whnfEasyCases Lean.Meta.WHNF:305:22: unreachable code has been reached

Steps to Reproduce

variable (R : α → α → Prop)

inductive List.Pairwise : List α → Prop
  | nil : Pairwise []
  | cons : ∀ {a : α} {l : List α}, (∀ {a} (_ : a' ∈ l), R a a') → Pairwise l → Pairwise (a :: l)

theorem and_assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
  ⟨fun ⟨⟨ha, hb⟩, hc⟩ => ⟨ha, hb, hc⟩, fun ⟨ha, hb, hc⟩ => ⟨⟨ha, hb⟩, hc⟩⟩

theorem and_left_comm : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) := by
  rw [← and_assoc, ← and_assoc, @And.comm a b]
  exact Iff.rfl

theorem pairwise_append {l₁ l₂ : List α} :
    (l₁ ++ l₂).Pairwise R ↔ l₁.Pairwise R ∧ l₂.Pairwise R ∧ ∀ {a} (_ : a ∈ l₁), ∀ {b} (_ : b ∈ l₂), R a b := by
  induction l₁ <;> simp [*, and_left_comm]

Expected behavior: [What you expect to happen]

Failure with unsolved goals. (I can restore a proper proof if that is better for a test case.)

Actual behavior: [What actually happens]

PANIC at Lean.Meta.whnfEasyCases Lean.Meta.WHNF:305:22: unreachable code has been reached

Versions

Lean (version 4.0.0-nightly-2022-11-16, commit 98922b8, Release)

Additional Information

This is getting in the way of bumping Std4 (and then mathlib4).