exact? returns long proof term which doesn't work

Stream: lean4

[Ted Hwa]

import Std.Data.List.Lemmas

-- the following works as expected
example {α: Type} (xs: List α) (h1: xs ≠ []) (h2: xs.length > 0):
    xs[0] = xs.head h1 := by
  simp
  exact?  -- exact List.get_mk_zero h2

-- now combine h1 and h2 into one hypothesis
example {α: Type} (xs: List α) (h: xs ≠ [] ∧ xs.length > 0):
    xs[0] = xs.head h.1 := by
  simp
  exact?  -- very long proof involving Lean.Omega which doesn't work when copied in

[Kim Morrison]

Note that the suggestion can be successfully replaced with exact List.get_mk_zero (by omega).

[Kim Morrison]

I think this is "not really exact?'s fault". An argument gets filled in by an autoparam, and there's no mechanism available to pretty-print the tactic invocation, rather than the proof the tactic produced.

[Kim Morrison]

The fact that the proof produced by omega doesn't round trip is sad, but not hugely surprising.