feat(logic/unique,data/fintype/basic): unique and fintype of subtype …

…of one element (#8491)

Additionally, a lemma proving that the cardinality of such a subtype is 1.

src/data/fintype/basic.lean

@@ -710,12 +710,36 @@ end
 @[instance, priority 10] def unique.fintype {α : Type*} [unique α] : fintype α :=
 fintype.of_subsingleton (default α)
 
+/-- Short-circuit instance to decrease search for `unique.fintype`,
+since that relies on a subsingleton elimination for `unique`. -/
+instance fintype.subtype_eq (y : α) : fintype {x // x = y} :=
+fintype.subtype {y} (by simp)
+
+/-- Short-circuit instance to decrease search for `unique.fintype`,
+since that relies on a subsingleton elimination for `unique`. -/
+instance fintype.subtype_eq' (y : α) : fintype {x // y = x} :=
+fintype.subtype {y} (by simp [eq_comm])
+
 @[simp] lemma univ_unique {α : Type*} [unique α] [f : fintype α] : @finset.univ α _ = {default α} :=
 by rw [subsingleton.elim f (@unique.fintype α _)]; refl
 
 @[simp] lemma univ_is_empty {α : Type*} [is_empty α] [fintype α] : @finset.univ α _ = ∅ :=
 finset.ext is_empty_elim
 
+@[simp] lemma fintype.card_subtype_eq (y : α)  :
+  fintype.card {x // x = y} = 1 :=
+begin
+  convert fintype.card_unique,
+  exact unique.subtype_eq _
+end
+
+@[simp] lemma fintype.card_subtype_eq' (y : α) :
+  fintype.card {x // y = x} = 1 :=
+begin
+  convert fintype.card_unique,
+  exact unique.subtype_eq' _
+end
+
 @[simp] theorem fintype.univ_empty : @univ empty _ = ∅ := rfl
 
 @[simp] theorem fintype.card_empty : fintype.card empty = 0 := rfl

src/logic/unique.lean

@@ -161,3 +161,15 @@ protected def injective.unique [inhabited α] [subsingleton β] (hf : injective
 @unique.mk' _ _ hf.subsingleton
 
 end function
+
+section subtype
+
+instance unique.subtype_eq (y : α) : unique {x // x = y} :=
+{ default := ⟨y, rfl⟩,
+  uniq := λ ⟨x, hx⟩, by simpa using hx }
+
+instance unique.subtype_eq' (y : α) : unique {x // y = x} :=
+{ default := ⟨y, rfl⟩,
+  uniq := λ ⟨x, hx⟩, by simpa using hx.symm }
+
+end subtype