Injective functions: right inverse and union of images

injective.lean

import data.set
import tactic

variables {α β : Type} [nonempty α] {f : α → β}

example (hf : function.injective f) :
  ∃ g, function.right_inverse f g :=
begin
  classical,
  let g := λ b,
      if h : ∃ a, f a = b
        then classical.some h
        else classical.choice (by apply_instance),
  use g,
  intro a,
  have h : ∃ a', f a' = f a, from ⟨a, rfl⟩,
  simp only [g, dif_pos h],
  apply hf,
  exact classical.some_spec h
end

example (hf : function.injective f) (s₁ s₂ : set α) :
  f '' s₁ ∩ f '' s₂ ⊆ f '' (s₁ ∩ s₂) :=
begin
  rintros b ⟨h₁, h₂⟩,
  simp only [set.mem_image, set.mem_set_of_eq] at ⊢ h₁ h₂,
  rcases h₁ with ⟨_, h₁, ⟨⟩⟩,
  rcases h₂ with ⟨a, h₂, h⟩,
  specialize hf h,
  subst hf,
  use a,
  simp [h₁, h₂]
end