Bijection A -> B from A+X -> B+X

Stream: Is there code for X?

[Timothy Mou]

Hi folks, not sure what this theorem is called, but it goes like given a bijection f : A + X -> B + X where X is finite, we can constructively obtain a bijection A -> B. The idea is you repeatedly apply f until you get something that lands in B, and you cannot get stuck in a loop in X because f is injective and X is finite (pigeonhole principle). Felt like this is something that would be in the Mathlib but could not find it or did not know how to search. Thanks!

[Chris Hughes]

I think you'd need an explicit bijectionX ≃ Fin n for this to work, I don't think either Finite, nor Fintype would be good enough. I proved a similar thing for option years ago, but never PRed it. I thought I'd generalize it today. I wouldn't be at all surprised if it wasn't in mathlib.

def option_fun_aux {α β : Type*} (h : Option α ≃ Option β) (a : α) : Option β :=
  Option.elim (h (some a)) (h none) some

def option_fun_aux_isSome {α β : Type*} (e : Option α ≃ Option β) (a : α) :
    (option_fun_aux e a).isSome := by
  rw [option_fun_aux]
  match h : e (some a) with
  | some x => simp
  | none =>
    simp only [Option.elim_none, Option.isSome_iff_ne_none]
    rw [← h]
    simp only [ne_eq, EmbeddingLike.apply_eq_iff_eq, reduceCtorEq, not_false_eq_true]

def option_fun {α β : Type*} (e : Option α ≃ Option β) (a : α) : β :=
  Option.get _ (option_fun_aux_isSome e a)

def option_fun_option_fun {α β : Type*} (e : Option α ≃ Option β) (a : α) :
    option_fun e.symm (option_fun e a) = a := by
  simp [option_fun, option_fun_aux]
  apply Option.some_injective
  simp only [Option.some_get]
  match h : e (some a) with
  | none =>
    simp only [Option.elim_none, Equiv.symm_apply_apply]
    rw [← h]
    simp
  | some x =>
    simp only [Option.elim_some]
    rw [← h]
    simp

def option_inj_aux {α β : Type*} (e : Option α ≃ Option β) : α ≃ β where
  toFun := option_fun e
  invFun := option_fun e.symm
  left_inv := option_fun_option_fun _
  right_inv := option_fun_option_fun e.symm

def optionSumEquivSumOption {α β : Type*} : (α ⊕ Option β) ≃ Option (α ⊕ β) where
  toFun := Sum.elim (some ∘ Sum.inl) (fun x => x.map Sum.inr)
  invFun := fun x => Option.elim x (Sum.inr none) (Sum.map id some)
  left_inv := by rintro (_ | _ | _) <;> simp
  right_inv := by rintro (_ | _ | _) <;> simp

def addFinEquiv {α β : Type*} : ∀ {n : ℕ}, (α ⊕ Fin n) ≃ (β ⊕ Fin n) → α ≃ β
  | 0, e => ((Equiv.sumEmpty _ _).symm.trans e).trans (Equiv.sumEmpty _ _)
  | n + 1, e =>
    have : Option (α ⊕ (Fin n)) ≃ Option (β ⊕ (Fin n)) := calc
      Option (α ⊕ (Fin n)) ≃ (α ⊕ Option (Fin n)) := optionSumEquivSumOption.symm
      _ ≃ α ⊕ Fin (n + 1) := Equiv.sumCongr (Equiv.refl _) (finSuccEquiv _).symm
      _ ≃ β ⊕ Fin (n + 1) := e
      _ ≃ (β ⊕ Option (Fin n)) := Equiv.sumCongr (Equiv.refl _) (finSuccEquiv _)
      _ ≃ Option (β ⊕ (Fin n)) := optionSumEquivSumOption
    addFinEquiv (option_inj_aux this)

[Yaël Dillies]

@Bhavik Mehta and I talked about this years ago. I don't remember if we ended up formalising anything