chore(logic/function/basic): remove classical decidable instance from…

… a lemma statement (#6488)

Found using #6485

This means that this lemma can be use in reverse against any `ite`, not just one that uses `classical.decidable`.

src/logic/function/basic.lean

@@ -463,8 +463,9 @@ Mostly useful when `f` is injective. -/
 def extend (f : α → β) (g : α → γ) (e' : β → γ) : β → γ :=
 λ b, if h : ∃ a, f a = b then g (classical.some h) else e' b
 
-lemma extend_def (f : α → β) (g : α → γ) (e' : β → γ) (b : β) :
-  extend f g e' b = if h : ∃ a, f a = b then g (classical.some h) else e' b := rfl
+lemma extend_def (f : α → β) (g : α → γ) (e' : β → γ) (b : β) [decidable (∃ a, f a = b)] :
+  extend f g e' b = if h : ∃ a, f a = b then g (classical.some h) else e' b :=
+by { unfold extend, congr }
 
 @[simp] lemma extend_apply (hf : injective f) (g : α → γ) (e' : β → γ) (a : α) :
   extend f g e' (f a) = g a :=