feat(data/set/basic): add set.subsingleton_range (#17248)

Also use it to golf a proof.

src/analysis/normed_space/add_torsor_bases.lean

@@ -60,10 +60,9 @@ lemma interior_convex_hull_aff_basis {ι E : Type*} [finite ι] [normed_add_comm
 begin
   casesI subsingleton_or_nontrivial ι,
   { -- The zero-dimensional case.
-    suffices : range (b.points) = univ, { simp [this], },
-    refine affine_subspace.eq_univ_of_subsingleton_span_eq_top _ b.tot,
-    rw ← image_univ,
-    exact subsingleton.image subsingleton_of_subsingleton b.points, },
+    have : range (b.points) = univ,
+      from affine_subspace.eq_univ_of_subsingleton_span_eq_top (subsingleton_range _) b.tot,
+    simp [this] },
   { -- The positive-dimensional case.
     haveI : finite_dimensional ℝ E := b.finite_dimensional,
     have : convex_hull ℝ (range b.points) = ⋂ i, (b.coord i)⁻¹' Ici 0,

src/data/set/basic.lean

@@ -2076,6 +2076,9 @@ theorem forall_subtype_range_iff {p : range f → Prop} :
   (∀ a : range f, p a) ↔ ∀ i, p ⟨f i, mem_range_self _⟩ :=
 ⟨λ H i, H _, λ H ⟨y, i, hi⟩, by { subst hi, apply H }⟩
 
+lemma subsingleton_range {α : Sort*} [subsingleton α] (f : α → β) : (range f).subsingleton :=
+forall_range_iff.2 $ λ x, forall_range_iff.2 $ λ y, congr_arg f (subsingleton.elim x y)
+
 theorem exists_range_iff {p : α → Prop} : (∃ a ∈ range f, p a) ↔ (∃ i, p (f i)) :=
 by simp