Infoview is broken inside `let rec termination_by` with goal

Stream: general

[Aaron Hill]

In the following example (with a dummy function that doesn't actually terminate), clicking inside the first decreasing_by correctly shows a goal of x - 1 < x. However, the goal state in the second decreasing_by always shows the outer goal of True, and never actually shows x - 1 < x:

def my_rec (x: Nat) : Nat := my_rec (x - 1)
  decreasing_by {
    let something := 1
    sorry
  }

def outer: True := by
  let rec my_rec (x: Nat) : Nat := my_rec (x - 1)
  decreasing_by {
    let something := 1
    sorry
  }
  trivial

Is there any known workaround for this? I hit this for a let rec inside of a large theorem, which would be very difficult to refactor