feat: add Function.update_eq_const and eq_const_of_subsingleton (#…

…7275)

Also golf `Function.update_apply`.

Mathlib/Logic/Function/Basic.lean

@@ -551,23 +551,27 @@ def update (f : ∀ a, β a) (a' : α) (v : β a') (a : α) : β a :=
   if h : a = a' then Eq.ndrec v h.symm else f a
 #align function.update Function.update
 
-/-- On non-dependent functions, `Function.update` can be expressed as an `ite` -/
-theorem update_apply {β : Sort*} (f : α → β) (a' : α) (b : β) (a : α) :
-    update f a' b a = if a = a' then b else f a :=
-by have h2 : (h : a = a') → Eq.rec (motive := λ _ _ => β) b h.symm = b :=
-     by intro h
-        rw [eq_rec_constant]
-   have h3 : (λ h : a = a' => Eq.rec (motive := λ _ _ => β) b h.symm) =
-             (λ _ : a = a' => b) := funext h2
-   let f := λ x => dite (a = a') x (λ (_: ¬ a = a') => (f a))
-   exact congrArg f h3
-#align function.update_apply Function.update_apply
-
 @[simp]
 theorem update_same (a : α) (v : β a) (f : ∀ a, β a) : update f a v a = v :=
   dif_pos rfl
 #align function.update_same Function.update_same
 
+@[simp]
+theorem update_noteq {a a' : α} (h : a ≠ a') (v : β a') (f : ∀ a, β a) : update f a' v a = f a :=
+  dif_neg h
+#align function.update_noteq Function.update_noteq
+
+/-- On non-dependent functions, `Function.update` can be expressed as an `ite` -/
+theorem update_apply {β : Sort*} (f : α → β) (a' : α) (b : β) (a : α) :
+    update f a' b a = if a = a' then b else f a := by
+  rcases Decidable.eq_or_ne a a' with rfl | hne <;> simp [*]
+#align function.update_apply Function.update_apply
+
+@[nontriviality]
+theorem update_eq_const_of_subsingleton [Subsingleton α] (a : α) (v : α') (f : α → α') :
+    update f a v = const α v :=
+  funext fun a' ↦ Subsingleton.elim a a' ▸ update_same _ _ _
+
 theorem surjective_eval {α : Sort u} {β : α → Sort v} [h : ∀ a, Nonempty (β a)] (a : α) :
     Surjective (eval a : (∀ a, β a) → β a) := fun b ↦
   ⟨@update _ _ (Classical.decEq α) (fun a ↦ (h a).some) a b,
@@ -579,11 +583,6 @@ theorem update_injective (f : ∀ a, β a) (a' : α) : Injective (update f a') :
   rwa [update_same, update_same] at this
 #align function.update_injective Function.update_injective
 
-@[simp]
-theorem update_noteq {a a' : α} (h : a ≠ a') (v : β a') (f : ∀ a, β a) : update f a' v a = f a :=
-  dif_neg h
-#align function.update_noteq Function.update_noteq
-
 lemma forall_update_iff (f : ∀a, β a) {a : α} {b : β a} (p : ∀a, β a → Prop) :
   (∀ x, p x (update f a b x)) ↔ p a b ∧ ∀ x, x ≠ a → p x (f x) := by
   rw [← and_forall_ne a, update_same]

Mathlib/Logic/Unique.lean

@@ -204,10 +204,12 @@ instance Pi.uniqueOfIsEmpty [IsEmpty α] (β : α → Sort v) : Unique (∀ a, 
   default := isEmptyElim
   uniq _ := funext isEmptyElim
 
-theorem eq_const_of_unique [Unique α] (f : α → β) : f = Function.const α (f default) := by
-  ext x
-  rw [Subsingleton.elim x default]
-  rfl
+theorem eq_const_of_subsingleton [Subsingleton α] (f : α → β) (a : α) :
+    f = Function.const α (f a) :=
+  funext fun x ↦ Subsingleton.elim x a ▸ rfl
+
+theorem eq_const_of_unique [Unique α] (f : α → β) : f = Function.const α (f default) :=
+  eq_const_of_subsingleton ..
 #align eq_const_of_unique eq_const_of_unique
 
 theorem heq_const_of_unique [Unique α] {β : α → Sort v} (f : ∀ a, β a) :