feat(data/equiv/basic): subsingleton equiv and perm (#5736)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/category_theory/simple.lean

@@ -29,9 +29,6 @@ class simple (X : C) : Type (max u v) :=
 begin
   casesI a, casesI b,
   congr,
-  funext Y f m,
-  ext,
-  refl,
 end
 
 instance subsingleton_simple (X : C) : subsingleton (simple X) :=

src/data/equiv/basic.lean

@@ -155,6 +155,23 @@ set.eq_univ_of_forall e.surjective
 protected theorem subsingleton (e : α ≃ β) [subsingleton β] : subsingleton α :=
 e.injective.subsingleton
 
+protected theorem subsingleton.symm (e : α ≃ β) [subsingleton α] : subsingleton β :=
+e.symm.injective.subsingleton
+
+instance equiv_subsingleton_cod [subsingleton β] :
+  subsingleton (α ≃ β) :=
+⟨λ f g, equiv.ext $ λ x, subsingleton.elim _ _⟩
+
+instance equiv_subsingleton_dom [subsingleton α] :
+  subsingleton (α ≃ β) :=
+⟨λ f g, equiv.ext $ λ x, @subsingleton.elim _ (equiv.subsingleton.symm f) _ _⟩
+
+instance perm_subsingleton [subsingleton α] : subsingleton (perm α) :=
+equiv.equiv_subsingleton_cod
+
+lemma perm.subsingleton_eq_refl [subsingleton α] (e : perm α) :
+  e = equiv.refl α := subsingleton.elim _ _
+
 /-- Transfer `decidable_eq` across an equivalence. -/
 protected def decidable_eq (e : α ≃ β) [decidable_eq β] : decidable_eq α :=
 e.injective.decidable_eq
@@ -179,6 +196,9 @@ rfl
 
 @[simp] theorem coe_refl : ⇑(equiv.refl α) = id := rfl
 
+@[simp] theorem perm.coe_subsingleton {α : Type*} [subsingleton α] (e : perm α) : ⇑(e) = id :=
+by rw [perm.subsingleton_eq_refl e, coe_refl]
+
 theorem refl_apply (x : α) : equiv.refl α x = x := rfl
 
 @[simp] theorem coe_trans (f : α ≃ β) (g : β ≃ γ) : ⇑(f.trans g) = g ∘ f := rfl