more auxDecl problems

Stream: lean4

[David Renshaw]

Here's another issue I've run into that seems kind of similar to https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/tactic.20'cases'.20failed.20nested.20error/near/315681420.

import Mathlib.Logic.Basic
import Mathlib.Tactic.Relation.Symm

variable {p : Prop}
variable (h : p ↔ p)

theorem foo : p :=
by symm at h -- (incorrectly) introduces a recursive hypothesis `foo : p`.
   assumption -- no error here

/-
all goals are closed, and we get an error:

  fail to show termination for
    foo
  with errors
  structural recursion cannot be used

  well-founded recursion cannot be used, 'foo' does not take any (non-fixed) arguments
-/

I expect this to give me an error at assumption. Instead, we get the above-shown error about structural recursion.

(I've reported this as https://github.com/leanprover-community/mathlib4/issues/1061.)

[David Renshaw]

(I'm reporting this in the lean4 stream instead of the mathlib4 stream, because my impression is that the bug is in the replace function, which looks like it's just a copy of the function replaceLocalDeclCore from Lean 4 core.)