Equational lemma generation for Array.insertionSort.swapLoop

[hargoniX]

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

The equational lemma generation for Array.insertionSort.swapLoop seems to be broken.

Steps to Reproduce

When using:

attribute [simp] Array.insertionSort.swapLoop

The compiler shows this error message:

tactic 'generalize' failed, result is not type correct
  ∀ (x : Nat) (x_1 : x = x),
    Array.insertionSort.swapLoop lt a x h =
      match x, x_1 with
      | 0, he => a
      | Nat.succ j', he =>
        let_fun h' := (_ : j' < Array.size a);
        if lt (Array.get a { val := x, isLt := h }) (Array.get a { val := j', isLt := h' }) = true then
          Array.insertionSort.swapLoop lt (Array.swap a { val := x, isLt := h } { val := j', isLt := h' }) j'
            (_ : j' < Array.size (Array.swap a { val := x, isLt := h } { val := j', isLt := h' }))
        else a
α : Type u_1
lt : α → α → Bool
a : Array α
j : Nat
h : j < Array.size a
⊢ Array.insertionSort.swapLoop lt a j h =
    match j, (_ : j = j) with
    | 0, he => a
    | Nat.succ j', he =>
      let_fun h' := (_ : j' < Array.size a);
      if lt (Array.get a { val := j, isLt := h }) (Array.get a { val := j', isLt := h' }) = true then
        Array.insertionSort.swapLoop lt (Array.swap a { val := j, isLt := h } { val := j', isLt := h' }) j'
          (_ : j' < Array.size (Array.swap a { val := j, isLt := h } { val := j', isLt := h' }))
      else a

Versions

Lean Version: Lean (version 4.0.0-nightly-2022-02-01, commit 9291f59, Release)
OS: Linux