feat(data/equiv/{basic,mul_equiv)}: add Pi_subsingleton (#12040)

src/data/equiv/basic.lean

@@ -512,13 +512,18 @@ def arrow_punit_equiv_punit (α : Sort*) : (α → punit.{v}) ≃ punit.{w} :=
 ⟨λ f, punit.star, λ u f, punit.star,
   λ f, by { funext x, cases f x, refl }, λ u, by { cases u, reflexivity }⟩
 
+/-- If `α` is `subsingleton` and `a : α`, then the type of dependent functions `Π (i : α), β
+i` is equivalent to `β i`. -/
+@[simps]
+def Pi_subsingleton {α} (β : α → Sort*) [subsingleton α] (a : α) : (Π a', β a') ≃ β a :=
+{ to_fun := eval a,
+  inv_fun := λ x b, cast (congr_arg β $ subsingleton.elim a b) x,
+  left_inv := λ f, funext $ λ b, by { rw subsingleton.elim b a, reflexivity },
+  right_inv := λ b, rfl }
 
 /-- If `α` has a unique term, then the type of function `α → β` is equivalent to `β`. -/
 @[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 }
+Pi_subsingleton _ default
 
 /-- The sort of maps from `punit` is equivalent to the codomain. -/
 def punit_arrow_equiv (α : Sort*) : (punit.{u} → α) ≃ α :=

src/data/equiv/mul_add.lean

@@ -418,6 +418,15 @@ lemma Pi_congr_right_trans {η : Type*}
   (es : ∀ j, Ms j ≃* Ns j) (fs : ∀ j, Ns j ≃* Ps j) :
   (Pi_congr_right es).trans (Pi_congr_right fs) = (Pi_congr_right $ λ i, (es i).trans (fs i)) := rfl
 
+/-- A family indexed by a nonempty subsingleton type is equivalent to the element at the single
+index. -/
+@[to_additive add_equiv.Pi_subsingleton "A family indexed by a nonempty subsingleton type is
+equivalent to the element at the single index.", simps]
+def Pi_subsingleton
+  {ι : Type*} (M : ι → Type*) [Π j, has_mul (M j)] [subsingleton ι] (i : ι) :
+  (Π j, M j) ≃* M i :=
+{ map_mul' := λ f1 f2, pi.mul_apply _ _ _, ..equiv.Pi_subsingleton M i }
+
 /-!
 # Groups
 -/