∀ {α : Type u} [inst : Ring α] {a : α} {num : ℤ} {denom : ℕ} {motive : Mathlib.Meta.NormNum.IsRat a num denom → Prop}
  (t : Mathlib.Meta.NormNum.IsRat a num denom),
  (∀ (inv : Invertible ↑denom) (eq : a = ↑num * ⅟↑denom), motive ⋯) → motive t