nontriviality leaves metavars

Stream: mathlib4

[Yury G. Kudryashov]

Hi, the following code in Data.Set.Finite leaves metavariables:

example : Finite α := by
  show_term { nontriviality α; sorry }

[Yury G. Kudryashov]

In Lean 3, I get

Try this: refine (subsingleton_or_nontrivial α).dcases_on (λ (_inst : subsingleton α), finite.of_subsingleton)
  (λ (_inst : nontrivial α),
     _[subsingleton_or_nontrivial α, subsingleton_or_nontrivial α, subsingleton_or_nontrivial α, _inst])

[Yury G. Kudryashov]

BTW, why are there 3 subsingleton_or_nontrivial α in the output?

[Yury G. Kudryashov]

@Sebastien Gouezel @Mario Carneiro You're the authors of nontriviality in Mathlib 4 :up:

[Mario Carneiro]

The core issue is lean4#2054, I posted a workaround in mathlib4#1769

[Yury G. Kudryashov]

Could you add a test, please?