When does the cases tactic find the recursor?

Stream: lean4

[Leni Aniva]

Consider the following proof:

example : (forall p q: Prop), Or p q -> Or q p := by
  intro p q h
  cases h
  . apply Or.inr
    assumption
  . apply Or.inl
    assumption

cases h here is applied to the metavariable generated by intro p q h. Right after cases h, if I were to query the value of this metavariable, I get

?m.45 _uniq.16 (Eq.refl _uniq.16)

here we have an extra metavariable ?m.45. Why is this not Or.casesOn? I think it could fill in Or.casesOn right away, because after the proof runs to completion, the value of the aforementioned metavariable becomes

Or.casesOn (motive := fun t => _uniq.16 = t → _uniq.13 ∨ _uniq.10) _uniq.16 (fun h h_1 => Eq.symm h_1 ▸ Or.inr h)
  (fun h h_1 => Eq.symm h_1 ▸ Or.inl h) (Eq.refl _uniq.16)

so at some point?m.45 is replaced by Or.casesOn .... When does this happen?

[Kyle Miller]

I believe you're looking at a delayed assignment metavariable. You need to follow docs#Lean.getDelayedMVarAssignment? for these.

They don't get assigned until the metavariable associated to it is fully assigned with no pending metavariables.