Fail to show termination in presence of ▸

[mik-jozef]

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

In the following code (sorry, tried to make it even smaller, but couldn't), a "failed to prove
termination" error shows up in the definition of variable asdf, despite that the
statement proving well-foundedness of the call is directly above in hereIAm.

The error disappears when the line containing aaLtA is commented out,
or extracted to another function, which provides a workaround.

As probably a separate issue, when I try to inline asdf, Lean won't even notice
the variable hereIAm (it won't be shown among other defined variables in
the error description).

open Classical

def least (s: T → Prop) (nonempty: { t: T // s t }): T := sorry

structure WellOrder where
  T: Type
  lt: T → T → Prop
  wf: WellFounded lt

instance (w: WellOrder): WellFoundedRelation w.T where
  rel := w.lt
  wf := w.wf

namespace WellOrder
  @[reducible] def succ.lt (w: WellOrder): (a b: Option w.T) → Prop
    | none, _ => False
    | some _, none => True
    | some a, some b => w.lt a b
  
  def succ (w: WellOrder): WellOrder :=
    {
      T := Option w.T,
      lt := succ.lt w,
      wf := sorry
    }
  
  noncomputable def Morphism.initial.helper
    {wa wb: WellOrder}
    (aSucc: wa.succ.T)
    (fA: wa.T)
  :
    wb.T
  :=
    -- If I inline this, Lean won't even notice the variable
    -- `hereIAm` at all.
    let asdf (aa: { aa: wa.T // wa.succ.lt (some aa) aSucc }) :=
      let hereIAm: wa.succ.lt (some aa.val) aSucc := aa.property
      initial.helper (some aa)
    
    if hEq: some fA = aSucc then
      least
        (fun b =>
          ∀ aa: { aa: wa.T // wa.succ.lt (some aa) aSucc },
            (asdf aa) aa.val ≠ b)
        ⟨
          sorry,
          fun aa eq =>
            -- If the next line is commented out, or extracted
            -- to a separate function, the error disappears.
            let aaLtA: wa.lt aa fA := hEq.symm ▸ aa.property
            sorry
        ⟩
      else sorry
    termination_by initial.helper a fA => a
end WellOrder

Steps to Reproduce

0. Paste the above code to VS Code.

Expected behavior: Termination is proven.

Actual behavior: An error shows up.

Reproduces how often: Always.

Versions

Both Lean 4 stable and nightly
Lean (version 4.0.0-nightly-2022-09-14, commit fccb60f, Release),
Lean (version 4.0.0, commit 7dbfaf9, Release)

Ubuntu 22.04.1 LTS