feat(*): a few more fun_uniques (#9938)

src/data/equiv/basic.lean

@@ -519,9 +519,9 @@ def arrow_punit_equiv_punit (α : Sort*) : (α → punit.{v}) ≃ punit.{w} :=
 
 
 /-- If `α` has a unique term, then the type of function `α → β` is equivalent to `β`. -/
-@[simps] def fun_unique (α β) [unique α] : (α → β) ≃ β :=
-{ to_fun := λ f, f (default α),
-  inv_fun := λ b a, b,
+@[simps { fully_applied := ff }] def fun_unique (α β) [unique α] : (α → β) ≃ β :=
+{ to_fun := eval (default α),
+  inv_fun := const α,
   left_inv := λ f, funext $ λ a, congr_arg f $ subsingleton.elim _ _,
   right_inv := λ b, rfl }
 

src/linear_algebra/pi.lean

@@ -333,6 +333,14 @@ def sum_arrow_lequiv_prod_arrow (α β R M : Type*) [semiring R] [add_comm_monoi
 @[simp] lemma sum_arrow_lequiv_prod_arrow_symm_apply_inr {α β} (f : α → M) (g : β → M) (b : β) :
   ((sum_arrow_lequiv_prod_arrow α β R M).symm (f, g)) (sum.inr b) = g b := rfl
 
+/-- If `ι` has a unique element, then `ι → M` is linearly equivalent to `M`. -/
+@[simps { simp_rhs := tt, fully_applied := ff }]
+def fun_unique (ι R M : Type*) [unique ι] [semiring R] [add_comm_monoid M] [module R M] :
+  (ι → M) ≃ₗ[R] M :=
+{ map_add' := λ f g, rfl,
+  map_smul' := λ c f, rfl,
+  .. equiv.fun_unique ι M }
+
 end linear_equiv
 
 section extend

src/topology/algebra/module.lean

@@ -1487,6 +1487,23 @@ equiv_of_inverse (f₁.prod (f₁.proj_ker_of_right_inverse f₂ h)) (f₂.copro
 
 end ring
 
+section
+
+variables (ι R M : Type*) [unique ι] [semiring R] [add_comm_monoid M] [module R M]
+  [topological_space M]
+
+/-- If `ι` has a unique element, then `ι → M` is continuously linear equivalent to `M`. -/
+def fun_unique : (ι → M) ≃L[R] M :=
+{ to_linear_equiv := linear_equiv.fun_unique ι R M,
+  .. homeomorph.fun_unique ι M }
+
+variables {ι R M}
+
+@[simp] lemma coe_fun_unique : ⇑(fun_unique ι R M) = function.eval (default ι) := rfl
+@[simp] lemma coe_fun_unique_symm : ⇑(fun_unique ι R M).symm = function.const ι := rfl
+
+end
+
 end continuous_linear_equiv
 
 namespace continuous_linear_map

src/topology/homeomorph.lean

@@ -392,6 +392,13 @@ homeomorph_of_continuous_open (equiv.sigma_prod_distrib σ β).symm
 
 end distrib
 
+/-- If `ι` has a unique element, then `ι → α` is homeomorphic to `α`. -/
+@[simps { fully_applied := ff }]
+def fun_unique (ι α : Type*) [unique ι] [topological_space α] : (ι → α) ≃ₜ α :=
+{ to_equiv := equiv.fun_unique ι α,
+  continuous_to_fun := continuous_apply _,
+  continuous_inv_fun := continuous_pi (λ _, continuous_id) }
+
 /--
 A subset of a topological space is homeomorphic to its image under a homeomorphism.
 -/