subsingleton from card = 1

Stream: Is there code for X?

[Eric Wieser]

I can't seem to find these:

import data.fintype.basic

variables {n : Type*} [fintype n] (h : fintype.card n = 1)

example : unique n := by library_search
example : subsingleton n := by library_search

[Gabriel Ebner]

docs#fintype.card_le_one_iff_subsingleton

[Eric Wieser]

Thanks, that beats my

  obtain ⟨k, heq⟩ := fintype.card_eq_one_iff.mp h,
  exact subsingleton_of_forall_eq k heq,

by a line