How do I trace a metavar automatically resolved in a proof?

Stream: general

[nrs]

Consider the following incomplete definition and its state:

import Mathlib

def makeSuccNTimesFunc {n : Nat} (m : Nat) : Fin2 n.succ -> Fin2 (n.succ + m) := by
  have ha : Fin2 n.succ -> Fin2 (n.succ + m) := ?x ∘ (Fin2.fs .)
  swap; convert @makeSuccNTimesFunc ?nn ?mm using 1
  _
/- state:
case h'
n m : ℕ
a✝ : Fin2 (n + 1).succ
⊢ Fin2 (n.succ + m) = Fin2 ((n + 1).succ + ?mm)

case mm
n m : ℕ
⊢ ℕ

n m : ℕ
ha : Fin2 n.succ → Fin2 (n.succ + m)
⊢ Fin2 n.succ → Fin2 (n.succ + m)

it seems using convert has automatically resolved the value of ?nn. Is there a trace I could run to see what value it resolved to?

[Martin Dvořák]

Please include your imports.

[nrs]

whoops sorry, it's just Mathlib

[nrs]

it seems set_option pp.explicit true with #print makeSuccNTimesFunc._unsafe_rec contains the information, I believe it is (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) n (@OfNat.ofNat Nat 1 (instOfNatNat 1))).succ that was inferred here? This is pretty painful to read, if anyone has suggestions it would be highly appreciated

[Kyle Miller]

def makeSuccNTimesFunc {n : Nat} (m : Nat) : Fin2 n.succ -> Fin2 (n.succ + m) := by
  have ha : Fin2 n.succ -> Fin2 (n.succ + m) := ?x ∘ (Fin2.fs .)
  swap; convert @makeSuccNTimesFunc ?nn ?mm using 1
  #check ?nn -- n + 1 : ℕ

[nrs]

ahhhh so much better! thank you very much!