fresh metavars

Stream: mathlib4

[Johan Commelin]

I just had to resort to the following hack

  have ih : ?_ := ?_ -- Porting note: this is an ugly hack, but `?ih` on the next line fails
  obtain ⟨a, a₀, ba, h⟩ := zorn_nonempty_partialOrder₀ (Set.Iio k) ih b (lt_of_le_of_ne hbk H)

whereas I expected that I could just write

  obtain ⟨a, a₀, ba, h⟩ := zorn_nonempty_partialOrder₀ (Set.Iio k) ?ih b (lt_of_le_of_ne hbk H)

[Johan Commelin]

Is this to be expected?

[Johan Commelin]

For the record, this is in https://github.com/leanprover-community/mathlib4/pull/1976, around L480