Glue together `Equiv`s on finite set

Stream: Is there code for X?

[Aaron Liu]

I have two permutations e₁ e₂ : Equiv.Perm Nat, and two disjoint subsets s₁ : Finset Nat := Finset.Iio a and s₂ : Finset Nat := Finset.Ico a b whose images under the permutations s₁.map e₁.toEmbedding and s₂.map e₂.toEmbedding are also disjoint. I want to glue together e₁ and e₂ into e : Equiv.Perm Nat such that ∀ n ∈ s₁, e n = e₁ n and ∀ n ∈ s₂, e n = e₂ n, constructively if possible. The action of ⇑e outside s₁.disjUnion s₂ ⋯ does not matter to me.

import Mathlib

example (e₁ e₂ : Equiv.Perm Nat) (a b : Nat)
    (disj : Disjoint ((Finset.Iio a).map e₁.toEmbedding) ((Finset.Ico a b).map e₂.toEmbedding)) :
    { e : Equiv.Perm Nat // (∀ n ∈ Finset.Iio a, e n = e₁ n) ∧ (∀ n ∈ Finset.Ico a b, e n = e₂ n)} :=
  sorry

[Aaron Liu]

I just thought of an infinitely better way to do what I wanted to do

[Aaron Liu]

so I technically don't need this anymore, but I'd love to see what you come up with

[Jakub Nowak]

You could try gluing together these 3 equivalences:

Finset.Iio a ≃ (Finset.Iio a).map e₁.toEmbedding

Finset.Ico a b ≃ (Finset.Ico a b).map e₂.toEmbedding

(Finset.Iio a ∪ Finset.Ico a b).toSet.compl ≃ ((Finset.Iio a).map e₁.toEmbedding ∪ (Finset.Ico a b).map e₂.toEmbedding).toSet.compl

[Jakub Nowak]

Though, I couldn't find in mathlib theorem that would state equivalence between Finset and its image under surjection/equivalence.