lean can't synth argument for instance

Stream: lean4

[Nir Paz]

I can't get typeclasses with an IsLimit assumption to synthesize properly:

import Mathlib

open Set

instance instNoMaxOrderIio {o : Ordinal} {h : o.IsLimit} : NoMaxOrder (Iio o) :=
  sorry

example {o : Ordinal} {h : o.IsLimit} : NoMaxOrder (Iio o) := instNoMaxOrderIio -- can't synth argument h

The problem is really that by infer_instance doesn't work, so I have to start some proofs with explicitly proving a few instances similar to this one (Nonempty (Iio o) is another common one). Is there a better way to deal with this?

[Daniel Weber]

You can use docs#Fact

[Nir Paz]

That's cool! I'll give it a try