Computably extending an embedding

Stream: Is there code for X?

[Eric Wieser]

Do we have something like this?

import Mathlib

variable {m n : Type*} [DecidableEq n] [Fintype m]

def Function.Embedding.equivSumRangeCompl (f : m ↪ n) : n ≃ m ⊕ ↥(Set.range f)ᶜ where
  toFun i :=
    -- TODO: this iterates twice rather than once
    if h : i ∈ Set.range f then .inl (f.invOfMemRange ⟨i, h⟩) else .inr ⟨i, h⟩
  invFun := Sum.elim f Subtype.val
  left_inv i := by
    dsimp
    split <;> simp
  right_inv
    | .inl i => by simp
    | .inr ⟨j, h⟩ => by
      rw [Set.mem_compl_iff] at h
      simp_all

[Antoine Chambert-Loir]

(to iterate only once, can you use docs#Nat.find?)

[Eric Wieser]

How do I produce the existential though?

[Eric Wieser]

To be clear, I say the above loops twice because the first is if h : i ∈ Set.range f, and the second is invOfMemRange.

[Yakov Pechersky]

Can you think of n as (Set.range f) ⊕ ((Set.range f)ᶜ : Set n) and have the equiv be using that, and then use a nasty Eq based cast Equiv to show that's the same a n?

[Eric Wieser]

I don't see what Eq you're going to use there, the range is not Eq to the domain

[Eric Wieser]

Certainly I can build the optimal version by using the Finset recursor, but this feels close to something we may already have

[Eric Wieser]

Maybe

/-- `invOfMemRange`, but returns `None` outside of the range-/
def Function.Embedding.invOption  {m n : Type*} [DecidableEq n] [Fintype m] (f : m ↪ n) (i : n) : Option m :=
  aux
where
  aux : Option {j : m // f j = i} :=
    Finset.univ.val.rec (C := fun _ : Multiset m  => Option _) none
      (fun x xs acc => acc <|> if h : f x = i then some ⟨x, h⟩ else none)
      (fun x₁ x₂ xs acc => heq_of_eq <| by
        dsimp at *
        obtain _ | ⟨x, h⟩ := acc <;> aesop)

is the building block here

[Bhavik Mehta]

You could also do it like

def Finset.toOption {m : Type*} (s : Finset m) (h : (s : Set m).Subsingleton) : Option m :=
  if hs : ∃ x ∈ s, True then some (s.choose (fun _ ↦ True) (existsUnique_of_exists_of_unique hs (by aesop))) else none

def Function.Embedding.invOption {m n : Type*} [DecidableEq n] [Fintype m] (f : m ↪ n) (i : n) : Option m :=
  Finset.toOption {j | f j = i} <| by aesop (add simp Set.Subsingleton)

but I haven't checked if this traverses once or twice

[Eric Wieser]

That would surely also be twice

[Eric Wieser]

Oh, I guess it's once on the full list, then twice on the singleton

[Bhavik Mehta]

Right, that was my exact hope