feat(data/fintype/basic): inv of inj on deceq (#5872)

Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>

src/data/fintype/basic.lean

@@ -248,6 +248,95 @@ def of_surjective [decidable_eq β] [fintype α] (f : α → β) (H : function.s
   fintype β :=
 ⟨univ.image f, λ b, let ⟨a, e⟩ := H b in e ▸ mem_image_of_mem _ (mem_univ _)⟩
 
+end fintype
+
+section inv
+
+namespace function
+
+variables [fintype α] [decidable_eq β]
+
+namespace injective
+
+variables {f : α → β} (hf : function.injective f)
+
+/--
+The inverse of an `hf : injective` function `f : α → β`, of the type `↥(set.range f) → α`.
+This is the computable version of `function.inv_fun` that requires `fintype α` and `decidable_eq β`,
+or the function version of applying `(equiv.set.range f hf).symm`.
+This function should not usually be used for actual computation because for most cases,
+an explicit inverse can be stated that has better computational properties.
+This function computes by checking all terms `a : α` to find the `f a = b`, so it is O(N) where
+`N = fintype.card α`.
+-/
+def inv_of_mem_range : set.range f → α :=
+λ b, finset.choose (λ a, f a = b) finset.univ ((exists_unique_congr (by simp)).mp
+  (hf.exists_unique_of_mem_range b.property))
+
+lemma left_inv_of_inv_of_mem_range (b : set.range f) :
+  f (hf.inv_of_mem_range b) = b :=
+(finset.choose_spec (λ a, f a = b) _ _).right
+
+@[simp] lemma right_inv_of_inv_of_mem_range (a : α) :
+  hf.inv_of_mem_range (⟨f a, set.mem_range_self a⟩) = a :=
+hf (finset.choose_spec (λ a', f a' = f a) _ _).right
+
+lemma inv_fun_restrict [nonempty α] :
+  (set.range f).restrict (inv_fun f) = hf.inv_of_mem_range :=
+begin
+  ext ⟨b, h⟩,
+  apply hf,
+  simp [hf.left_inv_of_inv_of_mem_range, @inv_fun_eq _ _ _ f b (set.mem_range.mp h)]
+end
+
+lemma inv_of_mem_range_surjective : function.surjective hf.inv_of_mem_range :=
+λ a, ⟨⟨f a, set.mem_range_self a⟩, by simp⟩
+
+end injective
+
+namespace embedding
+
+variables (f : α ↪ β) (b : set.range f)
+
+/--
+The inverse of an embedding `f : α ↪ β`, of the type `↥(set.range f) → α`.
+This is the computable version of `function.inv_fun` that requires `fintype α` and `decidable_eq β`,
+or the function version of applying `(equiv.set.range f f.injective).symm`.
+This function should not usually be used for actual computation because for most cases,
+an explicit inverse can be stated that has better computational properties.
+This function computes by checking all terms `a : α` to find the `f a = b`, so it is O(N) where
+`N = fintype.card α`.
+-/
+def inv_of_mem_range : α :=
+f.injective.inv_of_mem_range b
+
+@[simp] lemma left_inv_of_inv_of_mem_range :
+  f (f.inv_of_mem_range b) = b :=
+f.injective.left_inv_of_inv_of_mem_range b
+
+@[simp] lemma right_inv_of_inv_of_mem_range (a : α) :
+  f.inv_of_mem_range ⟨f a, set.mem_range_self a⟩ = a :=
+f.injective.right_inv_of_inv_of_mem_range a
+
+lemma inv_fun_restrict [nonempty α] :
+  (set.range f).restrict (inv_fun f) = f.inv_of_mem_range :=
+begin
+  ext ⟨b, h⟩,
+  apply f.injective,
+  simp [f.left_inv_of_inv_of_mem_range, @inv_fun_eq _ _ _ f b (set.mem_range.mp h)]
+end
+
+lemma inv_of_mem_range_surjective : function.surjective f.inv_of_mem_range :=
+λ a, ⟨⟨f a, set.mem_range_self a⟩, by simp⟩
+
+end embedding
+
+end function
+
+end inv
+
+namespace fintype
+
 /-- Given an injective function to a fintype, the domain is also a
 fintype. This is noncomputable because injectivity alone cannot be
 used to construct preimages. -/

src/data/set/basic.lean

@@ -1698,6 +1698,14 @@ lemma injective.nonempty_apply_iff {f : set α → set β} (hf : injective f)
   (h2 : f ∅ = ∅) {s : set α} : (f s).nonempty ↔ s.nonempty :=
 by rw [← ne_empty_iff_nonempty, ← h2, ← ne_empty_iff_nonempty, hf.ne_iff]
 
+lemma injective.mem_range_iff_exists_unique (hf : injective f) {b : β} :
+  b ∈ range f ↔ ∃! a, f a = b :=
+⟨λ ⟨a, h⟩, ⟨a, h, λ a' ha, hf (ha.trans h.symm)⟩, exists_unique.exists⟩
+
+lemma injective.exists_unique_of_mem_range (hf : injective f) {b : β} (hb : b ∈ range f) :
+  ∃! a, f a = b :=
+hf.mem_range_iff_exists_unique.mp hb
+
 end function
 open function
 

src/logic/function/basic.lean

@@ -220,7 +220,7 @@ include n
 local attribute [instance, priority 10] classical.prop_decidable
 
 /-- Construct the inverse for a function `f` on domain `s`. This function is a right inverse of `f`
-on `f '' s`. -/
+on `f '' s`. For a computable version, see `function.injective.inv_of_mem_range`. -/
 noncomputable def inv_fun_on (f : α → β) (s : set α) (b : β) : α :=
 if h : ∃a, a ∈ s ∧ f a = b then classical.some h else classical.choice n