MVarId.assertAfter incorrectly upgrades recursive auxDecl to kind "default".

[dwrensha]

import Lean

open Lean Elab.Tactic Lean.Meta

syntax (name := assertTrival) "assert_trivial ": tactic

elab_rules : tactic
  | `(tactic| assert_trivial) => withMainContext do
  let fvarIds := (← getLCtx).getFVarIds
  guard (fvarIds.size > 0)
  let fvarId := fvarIds[0]!
  let ty ← elabTerm (← `(True)) none
  let e ← elabTerm (← `(True.intro)) none
  let _ ← liftMetaTactic fun mvarId =>  do
     let result ← mvarId.assertAfter fvarId (Name.mkSimple "inserted_by_assert_trivial") ty e
     pure [result.mvarId]
  pure ()

variable {p : Prop}

theorem foo : p :=
by assert_trivial
   sorry

/-
  at the `sorry`, the context is:

    p : Prop
    inserted_by_assert_trivial : True
    foo : p
    ⊢ p

That `foo` hypothesis should not be there.
-/

$ lean --version
Lean (version 4.0.0-nightly-2022-12-13, commit 88c8cd5cf29a, Release)

[dwrensha]

We hit this behavior in mathlib4: leanprover-community/mathlib4#1061