Incorrect InfoTree for applications

Consider the following snippet (adapted from https://github.com/leanprover/lean4/issues/3462):

set_option trace.Elab.info true

example (n : Nat) : n = n := match n wit

This produces the following InfoTree:

• command @ ⟨3, 0⟩-⟨3, 40⟩ @ Lean.Elab.Command.elabDeclaration
      • Nat : Type @ ⟨3, 13⟩-⟨3, 16⟩ @ Lean.Elab.Term.elabIdent
        • [id] Nat : some Sort.{?_uniq.1} @ ⟨3, 13⟩-⟨3, 16⟩
        • Nat : Type @ ⟨3, 13⟩-⟨3, 16⟩
      • n (isBinder := true) : Nat @ ⟨3, 9⟩-⟨3, 10⟩
      • n = n : Prop @ ⟨3, 20⟩-⟨3, 25⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
        • Macro expansion
          n = n
          ===>
          binrel% Eq✝ n n
          • n = n : Prop @ ⟨3, 20⟩†-⟨3, 25⟩† @ Lean.Elab.Term.Op.elabBinRel
            • n = n : Prop @ ⟨3, 20⟩†-⟨3, 25⟩†
              • [id] Eq✝ : none @ ⟨3, 20⟩†-⟨3, 25⟩†
              • n : Nat @ ⟨3, 20⟩-⟨3, 21⟩ @ Lean.Elab.Term.elabIdent
                • [id] n : none @ ⟨3, 20⟩-⟨3, 21⟩
                • n : Nat @ ⟨3, 20⟩-⟨3, 21⟩
              • n : Nat @ ⟨3, 24⟩-⟨3, 25⟩ @ Lean.Elab.Term.elabIdent
                • [id] n : none @ ⟨3, 24⟩-⟨3, 25⟩
                • n : Nat @ ⟨3, 24⟩-⟨3, 25⟩
      • _example (isBinder := true) : ∀ (n : Nat), n = n @ ⟨3, 0⟩†-⟨3, 40⟩†
      • n (isBinder := true) : Nat @ ⟨3, 9⟩-⟨3, 10⟩
      • nomatch sorryAx ?m.13 true : n = n @ ⟨3, 29⟩-⟨3, 40⟩ @ Lean.Elab.Term.elabMatch
        • Macro expansion
          failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)
          ===>
          failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)
          • nomatch sorryAx ?m.13 true : n = n @ ⟨3, 29⟩†-⟨3, 40⟩† @ Lean.Elab.Term.elabLetMVar
            • sorryAx ?m.13 true : ?m.13 @ ⟨3, 35⟩-⟨3, 40⟩ @ Lean.Elab.Term.elabApp
              • [id] n : none @ ⟨3, 35⟩-⟨3, 36⟩
              • n : Nat @ ⟨3, 35⟩-⟨3, 36⟩
            • nomatch sorryAx ?m.13 true : n = n @ ⟨3, 29⟩-⟨3, 40⟩† @ Lean.Elab.Term.elabMatch
              • sorryAx ?m.13 true : ?m.13 @ ⟨3, 29⟩†-⟨3, 40⟩† @ Lean.Elab.Term.elabSyntheticHole
              • sorryAx ?m.13 true : ?m.13 @ ⟨3, 29⟩†-⟨3, 40⟩† @ Lean.Elab.Term.elabSyntheticHole 

In this tree, there is a completion node for n, but not wit, leading to incorrect completions after wit. Instead, this tree should contain a completion node for wit somewhere that the completion can work with.

Start by running the reported snippet with set_option trace.Elab.info true and inspect the InfoTree around Lean.Elab.Term.elabMatch and the completion nodes. Trace how the incomplete match n wit expression is elaborated and determine where the wit completion should be represented. Done means the tree includes a usable completion node for wit, producing correct completions after it.