import data.set.prod

import logic.function.conjugate

universes u v w x y

variables {α : Type u} {β : Type v} {π : α → Type v} {γ : Type w} {ι : Sort x}

open equiv equiv.perm function

namespace set

def restrict (s : set α) (f : Π a : α, π a) : Π a : s, π a := λ x, f x

lemma restrict_eq (f : α → β) (s : set α) : s.restrict f = f ∘ coe := rfl

@[simp] lemma restrict_apply (f : α → β) (s : set α) (x : s) : s.restrict f x = f x := rfl

lemma restrict_eq_iff {f : Π a, π a} {s : set α} {g : Π a : s, π a} :

restrict s f = g ↔ ∀ a (ha : a ∈ s), f a = g ⟨a, ha⟩ :=

funext_iff.trans subtype.forall

lemma eq_restrict_iff {s : set α} {f : Π a : s, π a} {g : Π a, π a} :

f = restrict s g ↔ ∀ a (ha : a ∈ s), f ⟨a, ha⟩ = g a :=

funext_iff.trans subtype.forall

@[simp] lemma range_restrict (f : α → β) (s : set α) : set.range (s.restrict f) = f '' s :=

(range_comp _ _).trans $ congr_arg (('') f) subtype.range_coe

lemma image_restrict (f : α → β) (s t : set α) : s.restrict f '' (coe ⁻¹' t) = f '' (t ∩ s) :=

by rw [restrict, image_comp, image_preimage_eq_inter_range, subtype.range_coe]

@[simp] lemma restrict_dite {s : set α} [∀ x, decidable (x ∈ s)] (f : Π a ∈ s, β) (g : Π a ∉ s, β) :

s.restrict (λ a, if h : a ∈ s then f a h else g a h) = λ a, f a a.2 :=

funext $ λ a, dif_pos a.2

@[simp] lemma restrict_dite_compl {s : set α} [∀ x, decidable (x ∈ s)] (f : Π a ∈ s, β)

(g : Π a ∉ s, β) :

sᶜ.restrict (λ a, if h : a ∈ s then f a h else g a h) = λ a, g a a.2 :=

funext $ λ a, dif_neg a.2

@[simp] lemma restrict_ite (f g : α → β) (s : set α) [∀ x, decidable (x ∈ s)] :

s.restrict (λ a, if a ∈ s then f a else g a) = s.restrict f :=

restrict_dite _ _

@[simp] lemma restrict_ite_compl (f g : α → β) (s : set α) [∀ x, decidable (x ∈ s)] :

sᶜ.restrict (λ a, if a ∈ s then f a else g a) = sᶜ.restrict g :=

restrict_dite_compl _ _

@[simp] lemma restrict_piecewise (f g : α → β) (s : set α) [∀ x, decidable (x ∈ s)] :

s.restrict (piecewise s f g) = s.restrict f :=

restrict_ite _ _ _

@[simp] lemma restrict_piecewise_compl (f g : α → β) (s : set α) [∀ x, decidable (x ∈ s)] :

sᶜ.restrict (piecewise s f g) = sᶜ.restrict g :=

restrict_ite_compl _ _ _

lemma restrict_extend_range (f : α → β) (g : α → γ) (g' : β → γ) :

(range f).restrict (extend f g g') = λ x, g x.coe_prop.some :=

by convert restrict_dite _ _

@[simp] lemma restrict_extend_compl_range (f : α → β) (g : α → γ) (g' : β → γ) :

(range f)ᶜ.restrict (extend f g g') = g' ∘ coe :=

by convert restrict_dite_compl _ _

lemma range_extend_subset (f : α → β) (g : α → γ) (g' : β → γ) :

range (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ :=

classical,

rintro _ ⟨y, rfl⟩,

rw extend_def, split_ifs,

exacts [or.inl (mem_range_self _), or.inr (mem_image_of_mem _ h)]

lemma range_extend {f : α → β} (hf : injective f) (g : α → γ) (g' : β → γ) :

range (extend f g g') = range g ∪ g' '' (range f)ᶜ :=

refine (range_extend_subset _ _ _).antisymm _,

rintro z (⟨x, rfl⟩|⟨y, hy, rfl⟩),

exacts [⟨f x, hf.extend_apply _ _ _⟩, ⟨y, extend_apply' _ _ _ hy⟩]

def cod_restrict (f : ι → α) (s : set α) (h : ∀ x, f x ∈ s) : ι → s :=

λ x, ⟨f x, h x⟩

@[simp] lemma coe_cod_restrict_apply (f : ι → α) (s : set α) (h : ∀ x, f x ∈ s) (x : ι) :

(cod_restrict f s h x : α) = f x :=

rfl

@[simp] lemma restrict_comp_cod_restrict {f : ι → α} {g : α → β} {b : set α}

(h : ∀ x, f x ∈ b) : (b.restrict g) ∘ (b.cod_restrict f h) = g ∘ f := rfl

@[simp] lemma injective_cod_restrict {f : ι → α} {s : set α} (h : ∀ x, f x ∈ s) :

injective (cod_restrict f s h) ↔ injective f :=

by simp only [injective, subtype.ext_iff, coe_cod_restrict_apply]

alias injective_cod_restrict ↔ _ _root_.function.injective.cod_restrict

variables {s s₁ s₂ : set α} {t t₁ t₂ : set β} {p : set γ} {f f₁ f₂ f₃ : α → β} {g g₁ g₂ : β → γ}

{f' f₁' f₂' : β → α} {g' : γ → β} {a : α} {b : β}

def eq_on (f₁ f₂ : α → β) (s : set α) : Prop :=

∀ ⦃x⦄, x ∈ s → f₁ x = f₂ x

@[simp] lemma eq_on_empty (f₁ f₂ : α → β) : eq_on f₁ f₂ ∅ := λ x, false.elim

@[simp] lemma eq_on_singleton : eq_on f₁ f₂ {a} ↔ f₁ a = f₂ a := by simp [set.eq_on]

@[simp] lemma restrict_eq_restrict_iff : restrict s f₁ = restrict s f₂ ↔ eq_on f₁ f₂ s :=

restrict_eq_iff

@[symm] lemma eq_on.symm (h : eq_on f₁ f₂ s) : eq_on f₂ f₁ s :=

λ x hx, (h hx).symm

lemma eq_on_comm : eq_on f₁ f₂ s ↔ eq_on f₂ f₁ s :=

⟨eq_on.symm, eq_on.symm⟩

@[refl] lemma eq_on_refl (f : α → β) (s : set α) : eq_on f f s :=

λ _ _, rfl

@[trans] lemma eq_on.trans (h₁ : eq_on f₁ f₂ s) (h₂ : eq_on f₂ f₃ s) : eq_on f₁ f₃ s :=

λ x hx, (h₁ hx).trans (h₂ hx)

theorem eq_on.image_eq (heq : eq_on f₁ f₂ s) : f₁ '' s = f₂ '' s :=

image_congr heq

theorem eq_on.inter_preimage_eq (heq : eq_on f₁ f₂ s) (t : set β) : s ∩ f₁ ⁻¹' t = s ∩ f₂ ⁻¹' t :=

ext $ λ x, and.congr_right_iff.2 $ λ hx, by rw [mem_preimage, mem_preimage, heq hx]

lemma eq_on.mono (hs : s₁ ⊆ s₂) (hf : eq_on f₁ f₂ s₂) : eq_on f₁ f₂ s₁ :=

λ x hx, hf (hs hx)

@[simp] lemma eq_on_union : eq_on f₁ f₂ (s₁ ∪ s₂) ↔ eq_on f₁ f₂ s₁ ∧ eq_on f₁ f₂ s₂ :=

ball_or_left_distrib

lemma eq_on.union (h₁ : eq_on f₁ f₂ s₁) (h₂ : eq_on f₁ f₂ s₂) : eq_on f₁ f₂ (s₁ ∪ s₂) :=

eq_on_union.2 ⟨h₁, h₂⟩

lemma eq_on.comp_left (h : s.eq_on f₁ f₂) : s.eq_on (g ∘ f₁) (g ∘ f₂) := λ a ha, congr_arg _ $ h ha

@[simp] lemma eq_on_range {ι : Sort*} {f : ι → α} {g₁ g₂ : α → β} :

eq_on g₁ g₂ (range f) ↔ g₁ ∘ f = g₂ ∘ f :=

forall_range_iff.trans $ funext_iff.symm

alias eq_on_range ↔ eq_on.comp_eq _

section order

variables [preorder α] [preorder β]

lemma _root_.monotone_on.congr (h₁ : monotone_on f₁ s) (h : s.eq_on f₁ f₂) : monotone_on f₂ s :=

intros a ha b hb hab,

rw [←h ha, ←h hb],

exact h₁ ha hb hab,

lemma _root_.antitone_on.congr (h₁ : antitone_on f₁ s) (h : s.eq_on f₁ f₂) : antitone_on f₂ s :=

h₁.dual_right.congr h

lemma _root_.strict_mono_on.congr (h₁ : strict_mono_on f₁ s) (h : s.eq_on f₁ f₂) :

strict_mono_on f₂ s :=

intros a ha b hb hab,

rw [←h ha, ←h hb],

exact h₁ ha hb hab,

lemma _root_.strict_anti_on.congr (h₁ : strict_anti_on f₁ s) (h : s.eq_on f₁ f₂) :

strict_anti_on f₂ s :=

h₁.dual_right.congr h

lemma eq_on.congr_monotone_on (h : s.eq_on f₁ f₂) : monotone_on f₁ s ↔ monotone_on f₂ s :=

⟨λ h₁, h₁.congr h, λ h₂, h₂.congr h.symm⟩

lemma eq_on.congr_antitone_on (h : s.eq_on f₁ f₂) : antitone_on f₁ s ↔ antitone_on f₂ s :=

⟨λ h₁, h₁.congr h, λ h₂, h₂.congr h.symm⟩

lemma eq_on.congr_strict_mono_on (h : s.eq_on f₁ f₂) : strict_mono_on f₁ s ↔ strict_mono_on f₂ s :=

⟨λ h₁, h₁.congr h, λ h₂, h₂.congr h.symm⟩

lemma eq_on.congr_strict_anti_on (h : s.eq_on f₁ f₂) : strict_anti_on f₁ s ↔ strict_anti_on f₂ s :=

⟨λ h₁, h₁.congr h, λ h₂, h₂.congr h.symm⟩

end order

section mono

variables [preorder α] [preorder β]

lemma _root_.monotone_on.mono (h : monotone_on f s) (h' : s₂ ⊆ s) : monotone_on f s₂ :=

λ x hx y hy, h (h' hx) (h' hy)

lemma _root_.antitone_on.mono (h : antitone_on f s) (h' : s₂ ⊆ s) : antitone_on f s₂ :=

λ x hx y hy, h (h' hx) (h' hy)

lemma _root_.strict_mono_on.mono (h : strict_mono_on f s) (h' : s₂ ⊆ s) : strict_mono_on f s₂ :=

λ x hx y hy, h (h' hx) (h' hy)

lemma _root_.strict_anti_on.mono (h : strict_anti_on f s) (h' : s₂ ⊆ s) : strict_anti_on f s₂ :=

λ x hx y hy, h (h' hx) (h' hy)

protected lemma _root_.monotone_on.monotone (h : monotone_on f s) : monotone (f ∘ coe : s → β) :=

λ x y hle, h x.coe_prop y.coe_prop hle

protected lemma _root_.antitone_on.monotone (h : antitone_on f s) : antitone (f ∘ coe : s → β) :=

λ x y hle, h x.coe_prop y.coe_prop hle

protected lemma _root_.strict_mono_on.strict_mono (h : strict_mono_on f s) :

strict_mono (f ∘ coe : s → β) :=

λ x y hlt, h x.coe_prop y.coe_prop hlt

protected lemma _root_.strict_anti_on.strict_anti (h : strict_anti_on f s) :

strict_anti (f ∘ coe : s → β) :=

λ x y hlt, h x.coe_prop y.coe_prop hlt

end mono

def maps_to (f : α → β) (s : set α) (t : set β) : Prop := ∀ ⦃x⦄, x ∈ s → f x ∈ t

def maps_to.restrict (f : α → β) (s : set α) (t : set β) (h : maps_to f s t) :

s → t :=

subtype.map f h

@[simp] lemma maps_to.coe_restrict_apply (h : maps_to f s t) (x : s) :

(h.restrict f s t x : β) = f x := rfl

@[simp] lemma cod_restrict_restrict (h : ∀ x : s, f x ∈ t) :

cod_restrict (s.restrict f) t h = maps_to.restrict f s t (λ x hx, h ⟨x, hx⟩) := rfl

lemma maps_to.restrict_eq_cod_restrict (h : maps_to f s t) :

h.restrict f s t = cod_restrict (s.restrict f) t (λ x, h x.2) := rfl

lemma maps_to.coe_restrict (h : set.maps_to f s t) :

coe ∘ h.restrict f s t = s.restrict f := rfl

lemma maps_to.range_restrict (f : α → β) (s : set α) (t : set β) (h : maps_to f s t) :

range (h.restrict f s t) = coe ⁻¹' (f '' s) :=

set.range_subtype_map f h

lemma maps_to_iff_exists_map_subtype : maps_to f s t ↔ ∃ g : s → t, ∀ x : s, f x = g x :=

⟨λ h, ⟨h.restrict f s t, λ _, rfl⟩,

λ ⟨g, hg⟩ x hx, by { erw [hg ⟨x, hx⟩], apply subtype.coe_prop }⟩

theorem maps_to' : maps_to f s t ↔ f '' s ⊆ t :=

image_subset_iff.symm

theorem maps_to_prod_map_diagonal : maps_to (prod.map f f) (diagonal α) (diagonal β) :=

diagonal_subset_iff.2 $ λ x, rfl

lemma maps_to.subset_preimage {f : α → β} {s : set α} {t : set β} (hf : maps_to f s t) :

s ⊆ f ⁻¹' t := hf

theorem maps_to_empty (f : α → β) (t : set β) : maps_to f ∅ t := empty_subset _

@[simp] lemma maps_to_singleton : maps_to f {a} t ↔ f a ∈ t := singleton_subset_iff

theorem maps_to.image_subset (h : maps_to f s t) : f '' s ⊆ t :=

maps_to'.1 h

theorem maps_to.congr (h₁ : maps_to f₁ s t) (h : eq_on f₁ f₂ s) :

maps_to f₂ s t :=

λ x hx, h hx ▸ h₁ hx

lemma eq_on.comp_right (hg : t.eq_on g₁ g₂) (hf : s.maps_to f t) : s.eq_on (g₁ ∘ f) (g₂ ∘ f) :=

λ a ha, hg $ hf ha

theorem eq_on.maps_to_iff (H : eq_on f₁ f₂ s) : maps_to f₁ s t ↔ maps_to f₂ s t :=

⟨λ h, h.congr H, λ h, h.congr H.symm⟩

theorem maps_to.comp (h₁ : maps_to g t p) (h₂ : maps_to f s t) : maps_to (g ∘ f) s p :=

λ x h, h₁ (h₂ h)

theorem maps_to_id (s : set α) : maps_to id s s := λ x, id

theorem maps_to.iterate {f : α → α} {s : set α} (h : maps_to f s s) :

∀ n, maps_to (f^[n]) s s

| 0 := λ _, id

| (n+1) := (maps_to.iterate n).comp h

theorem maps_to.iterate_restrict {f : α → α} {s : set α} (h : maps_to f s s) (n : ℕ) :

(h.restrict f s s^[n]) = (h.iterate n).restrict _ _ _ :=

funext x,

rw [subtype.ext_iff, maps_to.coe_restrict_apply],

induction n with n ihn generalizing x,

{ refl },

{ simp [nat.iterate, ihn] }

lemma maps_to_of_subsingleton' [subsingleton β] (f : α → β) (h : s.nonempty → t.nonempty) :

maps_to f s t :=

λ a ha, subsingleton.mem_iff_nonempty.2 $ h ⟨a, ha⟩

lemma maps_to_of_subsingleton [subsingleton α] (f : α → α) (s : set α) : maps_to f s s :=

maps_to_of_subsingleton' _ id

theorem maps_to.mono (hf : maps_to f s₁ t₁) (hs : s₂ ⊆ s₁) (ht : t₁ ⊆ t₂) :

maps_to f s₂ t₂ :=

λ x hx, ht (hf $ hs hx)

theorem maps_to.mono_left (hf : maps_to f s₁ t) (hs : s₂ ⊆ s₁) : maps_to f s₂ t :=

λ x hx, hf (hs hx)

theorem maps_to.mono_right (hf : maps_to f s t₁) (ht : t₁ ⊆ t₂) : maps_to f s t₂ :=

λ x hx, ht (hf hx)

theorem maps_to.union_union (h₁ : maps_to f s₁ t₁) (h₂ : maps_to f s₂ t₂) :

maps_to f (s₁ ∪ s₂) (t₁ ∪ t₂) :=

λ x hx, hx.elim (λ hx, or.inl $ h₁ hx) (λ hx, or.inr $ h₂ hx)

theorem maps_to.union (h₁ : maps_to f s₁ t) (h₂ : maps_to f s₂ t) :

maps_to f (s₁ ∪ s₂) t :=

union_self t ▸ h₁.union_union h₂

@[simp] theorem maps_to_union : maps_to f (s₁ ∪ s₂) t ↔ maps_to f s₁ t ∧ maps_to f s₂ t :=

⟨λ h, ⟨h.mono (subset_union_left s₁ s₂) (subset.refl t),

h.mono (subset_union_right s₁ s₂) (subset.refl t)⟩, λ h, h.1.union h.2⟩

theorem maps_to.inter (h₁ : maps_to f s t₁) (h₂ : maps_to f s t₂) :

maps_to f s (t₁ ∩ t₂) :=

λ x hx, ⟨h₁ hx, h₂ hx⟩

theorem maps_to.inter_inter (h₁ : maps_to f s₁ t₁) (h₂ : maps_to f s₂ t₂) :

maps_to f (s₁ ∩ s₂) (t₁ ∩ t₂) :=

λ x hx, ⟨h₁ hx.1, h₂ hx.2⟩

@[simp] theorem maps_to_inter : maps_to f s (t₁ ∩ t₂) ↔ maps_to f s t₁ ∧ maps_to f s t₂ :=

⟨λ h, ⟨h.mono (subset.refl s) (inter_subset_left t₁ t₂),

h.mono (subset.refl s) (inter_subset_right t₁ t₂)⟩, λ h, h.1.inter h.2⟩

theorem maps_to_univ (f : α → β) (s : set α) : maps_to f s univ := λ x h, trivial

theorem maps_to_image (f : α → β) (s : set α) : maps_to f s (f '' s) := by rw maps_to'

theorem maps_to_preimage (f : α → β) (t : set β) : maps_to f (f ⁻¹' t) t := subset.refl _

theorem maps_to_range (f : α → β) (s : set α) : maps_to f s (range f) :=

(maps_to_image f s).mono (subset.refl s) (image_subset_range _ _)

@[simp] lemma maps_image_to (f : α → β) (g : γ → α) (s : set γ) (t : set β) :

maps_to f (g '' s) t ↔ maps_to (f ∘ g) s t :=

⟨λ h c hc, h ⟨c, hc, rfl⟩, λ h d ⟨c, hc⟩, hc.2 ▸ h hc.1⟩

lemma maps_to.comp_left (g : β → γ) (hf : maps_to f s t) : maps_to (g ∘ f) s (g '' t) :=

λ x hx, ⟨f x, hf hx, rfl⟩

lemma maps_to.comp_right {s : set β} {t : set γ} (hg : maps_to g s t) (f : α → β) :

maps_to (g ∘ f) (f ⁻¹' s) t := λ x hx, hg hx

@[simp] lemma maps_univ_to (f : α → β) (s : set β) :

maps_to f univ s ↔ ∀ a, f a ∈ s :=

⟨λ h a, h (mem_univ _), λ h x _, h x⟩

@[simp] lemma maps_range_to (f : α → β) (g : γ → α) (s : set β) :

maps_to f (range g) s ↔ maps_to (f ∘ g) univ s :=

by rw [←image_univ, maps_image_to]

theorem surjective_maps_to_image_restrict (f : α → β) (s : set α) :

surjective ((maps_to_image f s).restrict f s (f '' s)) :=

λ ⟨y, x, hs, hxy⟩, ⟨⟨x, hs⟩, subtype.ext hxy⟩

theorem maps_to.mem_iff (h : maps_to f s t) (hc : maps_to f sᶜ tᶜ) {x} : f x ∈ t ↔ x ∈ s :=

⟨λ ht, by_contra $ λ hs, hc hs ht, λ hx, h hx⟩

variables (t f)

@[simps] def restrict_preimage : f ⁻¹' t → t :=

(set.maps_to_preimage f t).restrict _ _ _

lemma range_restrict_preimage :

range (t.restrict_preimage f) = coe ⁻¹' (range f) :=

delta set.restrict_preimage,

rw [maps_to.range_restrict, set.image_preimage_eq_inter_range,

set.preimage_inter, subtype.coe_preimage_self, set.univ_inter],

variables {f} {U : ι → set β}

lemma restrict_preimage_injective (hf : injective f) : injective (t.restrict_preimage f) :=

λ x y e, subtype.mk.inj_arrow e (λ e, subtype.coe_injective (hf e))

lemma restrict_preimage_surjective (hf : surjective f) : surjective (t.restrict_preimage f) :=

λ x, ⟨⟨_, (show f (hf x).some ∈ t, from (hf x).some_spec.symm ▸ x.2)⟩, subtype.ext (hf x).some_spec⟩

lemma restrict_preimage_bijective (hf : bijective f) : bijective (t.restrict_preimage f) :=

⟨t.restrict_preimage_injective hf.1, t.restrict_preimage_surjective hf.2⟩

alias set.restrict_preimage_injective ← _root_.function.injective.restrict_preimage

alias set.restrict_preimage_surjective ← _root_.function.surjective.restrict_preimage

alias set.restrict_preimage_bijective ← _root_.function.bijective.restrict_preimage

def inj_on (f : α → β) (s : set α) : Prop :=

∀ ⦃x₁ : α⦄, x₁ ∈ s → ∀ ⦃x₂ : α⦄, x₂ ∈ s → f x₁ = f x₂ → x₁ = x₂

theorem subsingleton.inj_on (hs : s.subsingleton) (f : α → β) : inj_on f s :=

λ x hx y hy h, hs hx hy

@[simp] theorem inj_on_empty (f : α → β) : inj_on f ∅ :=

subsingleton_empty.inj_on f

@[simp] theorem inj_on_singleton (f : α → β) (a : α) : inj_on f {a} :=

subsingleton_singleton.inj_on f

theorem inj_on.eq_iff {x y} (h : inj_on f s) (hx : x ∈ s) (hy : y ∈ s) :

f x = f y ↔ x = y :=

⟨h hx hy, λ h, h ▸ rfl⟩

lemma inj_on.ne_iff {x y} (h : inj_on f s) (hx : x ∈ s) (hy : y ∈ s) : f x ≠ f y ↔ x ≠ y :=

(h.eq_iff hx hy).not

alias inj_on.ne_iff ↔ _ inj_on.ne

theorem inj_on.congr (h₁ : inj_on f₁ s) (h : eq_on f₁ f₂ s) :

inj_on f₂ s :=

λ x hx y hy, h hx ▸ h hy ▸ h₁ hx hy

theorem eq_on.inj_on_iff (H : eq_on f₁ f₂ s) : inj_on f₁ s ↔ inj_on f₂ s :=

⟨λ h, h.congr H, λ h, h.congr H.symm⟩

theorem inj_on.mono (h : s₁ ⊆ s₂) (ht : inj_on f s₂) : inj_on f s₁ :=

λ x hx y hy H, ht (h hx) (h hy) H

theorem inj_on_union (h : disjoint s₁ s₂) :

inj_on f (s₁ ∪ s₂) ↔ inj_on f s₁ ∧ inj_on f s₂ ∧ ∀ (x ∈ s₁) (y ∈ s₂), f x ≠ f y :=

refine ⟨λ H, ⟨H.mono $ subset_union_left _ _, H.mono $ subset_union_right _ _, _⟩, _⟩,

{ intros x hx y hy hxy,

obtain rfl : x = y, from H (or.inl hx) (or.inr hy) hxy,

exact h.le_bot ⟨hx, hy⟩ },

{ rintro ⟨h₁, h₂, h₁₂⟩,

rintro x (hx|hx) y (hy|hy) hxy,

exacts [h₁ hx hy hxy, (h₁₂ _ hx _ hy hxy).elim, (h₁₂ _ hy _ hx hxy.symm).elim, h₂ hx hy hxy] }

theorem inj_on_insert {f : α → β} {s : set α} {a : α} (has : a ∉ s) :

set.inj_on f (insert a s) ↔ set.inj_on f s ∧ f a ∉ f '' s :=

have disjoint s {a}, from disjoint_iff_inf_le.mpr $ λ x ⟨hxs, (hxa : x = a)⟩, has (hxa ▸ hxs),

by { rw [← union_singleton, inj_on_union this], simp }

lemma injective_iff_inj_on_univ : injective f ↔ inj_on f univ :=

⟨λ h x hx y hy hxy, h hxy, λ h _ _ heq, h trivial trivial heq⟩

lemma inj_on_of_injective (h : injective f) (s : set α) : inj_on f s :=

λ x hx y hy hxy, h hxy

alias inj_on_of_injective ← _root_.function.injective.inj_on

lemma inj_on_id (s : set α) : inj_on id s := injective_id.inj_on _

theorem inj_on.comp (hg : inj_on g t) (hf: inj_on f s) (h : maps_to f s t) :

inj_on (g ∘ f) s :=

λ x hx y hy heq, hf hx hy $ hg (h hx) (h hy) heq

lemma inj_on.iterate {f : α → α} {s : set α} (h : inj_on f s) (hf : maps_to f s s) :

∀ n, inj_on (f^[n]) s

| 0 := inj_on_id _

| (n + 1) := (inj_on.iterate n).comp h hf

lemma inj_on_of_subsingleton [subsingleton α] (f : α → β) (s : set α) : inj_on f s :=

(injective_of_subsingleton _).inj_on _

lemma _root_.function.injective.inj_on_range (h : injective (g ∘ f)) : inj_on g (range f) :=

by { rintros _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ H, exact congr_arg f (h H) }

lemma inj_on_iff_injective : inj_on f s ↔ injective (s.restrict f) :=

⟨λ H a b h, subtype.eq $ H a.2 b.2 h,

λ H a as b bs h, congr_arg subtype.val $ @H ⟨a, as⟩ ⟨b, bs⟩ h⟩

alias inj_on_iff_injective ↔ inj_on.injective _

lemma maps_to.restrict_inj (h : maps_to f s t) : injective (h.restrict f s t) ↔ inj_on f s :=

by rw [h.restrict_eq_cod_restrict, injective_cod_restrict, inj_on_iff_injective]

lemma exists_inj_on_iff_injective [nonempty β] :

(∃ f : α → β, inj_on f s) ↔ ∃ f : s → β, injective f :=

⟨λ ⟨f, hf⟩, ⟨_, hf.injective⟩,

λ ⟨f, hf⟩, by { lift f to α → β using trivial, exact ⟨f, inj_on_iff_injective.2 hf⟩ }⟩

lemma inj_on_preimage {B : set (set β)} (hB : B ⊆ 𝒫 (range f)) :

inj_on (preimage f) B :=

λ s hs t ht hst, (preimage_eq_preimage' (hB hs) (hB ht)).1 hst

lemma inj_on.mem_of_mem_image {x} (hf : inj_on f s) (hs : s₁ ⊆ s) (h : x ∈ s) (h₁ : f x ∈ f '' s₁) :

x ∈ s₁ :=

let ⟨x', h', eq⟩ := h₁ in hf (hs h') h eq ▸ h'

lemma inj_on.mem_image_iff {x} (hf : inj_on f s) (hs : s₁ ⊆ s) (hx : x ∈ s) :

f x ∈ f '' s₁ ↔ x ∈ s₁ :=

⟨hf.mem_of_mem_image hs hx, mem_image_of_mem f⟩

lemma inj_on.preimage_image_inter (hf : inj_on f s) (hs : s₁ ⊆ s) :

f ⁻¹' (f '' s₁) ∩ s = s₁ :=

ext $ λ x, ⟨λ ⟨h₁, h₂⟩, hf.mem_of_mem_image hs h₂ h₁, λ h, ⟨mem_image_of_mem _ h, hs h⟩⟩

lemma eq_on.cancel_left (h : s.eq_on (g ∘ f₁) (g ∘ f₂)) (hg : t.inj_on g) (hf₁ : s.maps_to f₁ t)

(hf₂ : s.maps_to f₂ t) :

s.eq_on f₁ f₂ :=

λ a ha, hg (hf₁ ha) (hf₂ ha) (h ha)

lemma inj_on.cancel_left (hg : t.inj_on g) (hf₁ : s.maps_to f₁ t) (hf₂ : s.maps_to f₂ t) :

s.eq_on (g ∘ f₁) (g ∘ f₂) ↔ s.eq_on f₁ f₂ :=

⟨λ h, h.cancel_left hg hf₁ hf₂, eq_on.comp_left⟩

lemma inj_on.image_inter {s t u : set α} (hf : u.inj_on f) (hs : s ⊆ u) (ht : t ⊆ u) :

f '' (s ∩ t) = f '' s ∩ f '' t :=

apply subset.antisymm (image_inter_subset _ _ _),

rintros x ⟨⟨y, ys, hy⟩, ⟨z, zt, hz⟩⟩,

have : y = z,

{ apply hf (hs ys) (ht zt),

rwa ← hz at hy },

rw ← this at zt,

exact ⟨y, ⟨ys, zt⟩, hy⟩,

lemma _root_.disjoint.image {s t u : set α} {f : α → β} (h : disjoint s t) (hf : inj_on f u)

(hs : s ⊆ u) (ht : t ⊆ u) : disjoint (f '' s) (f '' t) :=

rw disjoint_iff_inter_eq_empty at h ⊢,

rw [← hf.image_inter hs ht, h, image_empty],

def surj_on (f : α → β) (s : set α) (t : set β) : Prop := t ⊆ f '' s

theorem surj_on.subset_range (h : surj_on f s t) : t ⊆ range f :=

subset.trans h $ image_subset_range f s

lemma surj_on_iff_exists_map_subtype :

surj_on f s t ↔ ∃ (t' : set β) (g : s → t'), t ⊆ t' ∧ surjective g ∧ ∀ x : s, f x = g x :=

⟨λ h, ⟨_, (maps_to_image f s).restrict f s _, h, surjective_maps_to_image_restrict _ _, λ _, rfl⟩,

λ ⟨t', g, htt', hg, hfg⟩ y hy, let ⟨x, hx⟩ := hg ⟨y, htt' hy⟩ in

⟨x, x.2, by rw [hfg, hx, subtype.coe_mk]⟩⟩

theorem surj_on_empty (f : α → β) (s : set α) : surj_on f s ∅ := empty_subset _

@[simp] lemma surj_on_singleton : surj_on f s {b} ↔ b ∈ f '' s := singleton_subset_iff

theorem surj_on_image (f : α → β) (s : set α) : surj_on f s (f '' s) := subset.rfl

theorem surj_on.comap_nonempty (h : surj_on f s t) (ht : t.nonempty) : s.nonempty :=

(ht.mono h).of_image

theorem surj_on.congr (h : surj_on f₁ s t) (H : eq_on f₁ f₂ s) : surj_on f₂ s t :=

by rwa [surj_on, ← H.image_eq]

theorem eq_on.surj_on_iff (h : eq_on f₁ f₂ s) : surj_on f₁ s t ↔ surj_on f₂ s t :=

⟨λ H, H.congr h, λ H, H.congr h.symm⟩

theorem surj_on.mono (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) (hf : surj_on f s₁ t₂) : surj_on f s₂ t₁ :=

subset.trans ht $ subset.trans hf $ image_subset _ hs

theorem surj_on.union (h₁ : surj_on f s t₁) (h₂ : surj_on f s t₂) : surj_on f s (t₁ ∪ t₂) :=

λ x hx, hx.elim (λ hx, h₁ hx) (λ hx, h₂ hx)

theorem surj_on.union_union (h₁ : surj_on f s₁ t₁) (h₂ : surj_on f s₂ t₂) :

surj_on f (s₁ ∪ s₂) (t₁ ∪ t₂) :=

(h₁.mono (subset_union_left _ _) (subset.refl _)).union

(h₂.mono (subset_union_right _ _) (subset.refl _))

theorem surj_on.inter_inter (h₁ : surj_on f s₁ t₁) (h₂ : surj_on f s₂ t₂) (h : inj_on f (s₁ ∪ s₂)) :

surj_on f (s₁ ∩ s₂) (t₁ ∩ t₂) :=

intros y hy,

rcases h₁ hy.1 with ⟨x₁, hx₁, rfl⟩,

rcases h₂ hy.2 with ⟨x₂, hx₂, heq⟩,

obtain rfl : x₁ = x₂ := h (or.inl hx₁) (or.inr hx₂) heq.symm,

exact mem_image_of_mem f ⟨hx₁, hx₂⟩

theorem surj_on.inter (h₁ : surj_on f s₁ t) (h₂ : surj_on f s₂ t) (h : inj_on f (s₁ ∪ s₂)) :

surj_on f (s₁ ∩ s₂) t :=

inter_self t ▸ h₁.inter_inter h₂ h

lemma surj_on_id (s : set α) : surj_on id s s := by simp [surj_on]

theorem surj_on.comp (hg : surj_on g t p) (hf : surj_on f s t) : surj_on (g ∘ f) s p :=

subset.trans hg $ subset.trans (image_subset g hf) $ (image_comp g f s) ▸ subset.refl _

lemma surj_on.iterate {f : α → α} {s : set α} (h : surj_on f s s) : ∀ n, surj_on (f^[n]) s s

| 0 := surj_on_id _

| (n + 1) := (surj_on.iterate n).comp h

lemma surj_on.comp_left (hf : surj_on f s t) (g : β → γ) : surj_on (g ∘ f) s (g '' t) :=

by { rw [surj_on, image_comp g f], exact image_subset _ hf }

lemma surj_on.comp_right {s : set β} {t : set γ} (hf : surjective f) (hg : surj_on g s t) :

surj_on (g ∘ f) (f ⁻¹' s) t :=

by rwa [surj_on, image_comp g f, image_preimage_eq _ hf]

lemma surj_on_of_subsingleton' [subsingleton β] (f : α → β) (h : t.nonempty → s.nonempty) :

surj_on f s t :=

λ a ha, subsingleton.mem_iff_nonempty.2 $ (h ⟨a, ha⟩).image _

lemma surj_on_of_subsingleton [subsingleton α] (f : α → α) (s : set α) : surj_on f s s :=

surj_on_of_subsingleton' _ id

lemma surjective_iff_surj_on_univ : surjective f ↔ surj_on f univ univ :=

by simp [surjective, surj_on, subset_def]

lemma surj_on_iff_surjective : surj_on f s univ ↔ surjective (s.restrict f) :=

⟨λ H b, let ⟨a, as, e⟩ := @H b trivial in ⟨⟨a, as⟩, e⟩,

λ H b _, let ⟨⟨a, as⟩, e⟩ := H b in ⟨a, as, e⟩⟩

lemma surj_on.image_eq_of_maps_to (h₁ : surj_on f s t) (h₂ : maps_to f s t) :

f '' s = t :=

eq_of_subset_of_subset h₂.image_subset h₁

lemma image_eq_iff_surj_on_maps_to : f '' s = t ↔ s.surj_on f t ∧ s.maps_to f t :=

refine ⟨_, λ h, h.1.image_eq_of_maps_to h.2⟩,

rintro rfl,

exact ⟨s.surj_on_image f, s.maps_to_image f⟩,

lemma surj_on.maps_to_compl (h : surj_on f s t) (h' : injective f) : maps_to f sᶜ tᶜ :=

λ x hs ht, let ⟨x', hx', heq⟩ := h ht in hs $ h' heq ▸ hx'

lemma maps_to.surj_on_compl (h : maps_to f s t) (h' : surjective f) : surj_on f sᶜ tᶜ :=

h'.forall.2 $ λ x ht, mem_image_of_mem _ $ λ hs, ht (h hs)

lemma eq_on.cancel_right (hf : s.eq_on (g₁ ∘ f) (g₂ ∘ f)) (hf' : s.surj_on f t) : t.eq_on g₁ g₂ :=

intros b hb,

obtain ⟨a, ha, rfl⟩ := hf' hb,

exact hf ha,

lemma surj_on.cancel_right (hf : s.surj_on f t) (hf' : s.maps_to f t) :

s.eq_on (g₁ ∘ f) (g₂ ∘ f) ↔ t.eq_on g₁ g₂ :=

⟨λ h, h.cancel_right hf, λ h, h.comp_right hf'⟩

lemma eq_on_comp_right_iff : s.eq_on (g₁ ∘ f) (g₂ ∘ f) ↔ (f '' s).eq_on g₁ g₂ :=

(s.surj_on_image f).cancel_right $ s.maps_to_image f

def bij_on (f : α → β) (s : set α) (t : set β) : Prop :=

maps_to f s t ∧ inj_on f s ∧ surj_on f s t

lemma bij_on.maps_to (h : bij_on f s t) : maps_to f s t := h.left

lemma bij_on.inj_on (h : bij_on f s t) : inj_on f s := h.right.left

lemma bij_on.surj_on (h : bij_on f s t) : surj_on f s t := h.right.right

lemma bij_on.mk (h₁ : maps_to f s t) (h₂ : inj_on f s) (h₃ : surj_on f s t) :

bij_on f s t :=

⟨h₁, h₂, h₃⟩

@[simp] lemma bij_on_empty (f : α → β) : bij_on f ∅ ∅ :=

⟨maps_to_empty f ∅, inj_on_empty f, surj_on_empty f ∅⟩

@[simp] lemma bij_on_singleton : bij_on f {a} {b} ↔ f a = b := by simp [bij_on, eq_comm]

lemma bij_on.inter_maps_to (h₁ : bij_on f s₁ t₁) (h₂ : maps_to f s₂ t₂) (h₃ : s₁ ∩ f ⁻¹' t₂ ⊆ s₂) :

bij_on f (s₁ ∩ s₂) (t₁ ∩ t₂) :=

⟨h₁.maps_to.inter_inter h₂, h₁.inj_on.mono $ inter_subset_left _ _,

λ y hy, let ⟨x, hx, hxy⟩ := h₁.surj_on hy.1 in ⟨x, ⟨hx, h₃ ⟨hx, hxy.symm.rec_on hy.2⟩⟩, hxy⟩⟩

lemma maps_to.inter_bij_on (h₁ : maps_to f s₁ t₁) (h₂ : bij_on f s₂ t₂)

(h₃ : s₂ ∩ f ⁻¹' t₁ ⊆ s₁) :

bij_on f (s₁ ∩ s₂) (t₁ ∩ t₂) :=

inter_comm s₂ s₁ ▸ inter_comm t₂ t₁ ▸ h₂.inter_maps_to h₁ h₃

lemma bij_on.inter (h₁ : bij_on f s₁ t₁) (h₂ : bij_on f s₂ t₂) (h : inj_on f (s₁ ∪ s₂)) :

bij_on f (s₁ ∩ s₂) (t₁ ∩ t₂) :=

⟨h₁.maps_to.inter_inter h₂.maps_to, h₁.inj_on.mono $ inter_subset_left _ _,

h₁.surj_on.inter_inter h₂.surj_on h⟩

lemma bij_on.union (h₁ : bij_on f s₁ t₁) (h₂ : bij_on f s₂ t₂) (h : inj_on f (s₁ ∪ s₂)) :

bij_on f (s₁ ∪ s₂) (t₁ ∪ t₂) :=

⟨h₁.maps_to.union_union h₂.maps_to, h, h₁.surj_on.union_union h₂.surj_on⟩

theorem bij_on.subset_range (h : bij_on f s t) : t ⊆ range f :=

h.surj_on.subset_range

lemma inj_on.bij_on_image (h : inj_on f s) : bij_on f s (f '' s) :=

bij_on.mk (maps_to_image f s) h (subset.refl _)

theorem bij_on.congr (h₁ : bij_on f₁ s t) (h : eq_on f₁ f₂ s) :

bij_on f₂ s t :=

bij_on.mk (h₁.maps_to.congr h) (h₁.inj_on.congr h) (h₁.surj_on.congr h)

theorem eq_on.bij_on_iff (H : eq_on f₁ f₂ s) : bij_on f₁ s t ↔ bij_on f₂ s t :=

⟨λ h, h.congr H, λ h, h.congr H.symm⟩

lemma bij_on.image_eq (h : bij_on f s t) :

f '' s = t :=

h.surj_on.image_eq_of_maps_to h.maps_to

lemma bij_on_id (s : set α) : bij_on id s s := ⟨s.maps_to_id, s.inj_on_id, s.surj_on_id⟩

theorem bij_on.comp (hg : bij_on g t p) (hf : bij_on f s t) : bij_on (g ∘ f) s p :=

bij_on.mk (hg.maps_to.comp hf.maps_to) (hg.inj_on.comp hf.inj_on hf.maps_to)

(hg.surj_on.comp hf.surj_on)

lemma bij_on.iterate {f : α → α} {s : set α} (h : bij_on f s s) : ∀ n, bij_on (f^[n]) s s

| 0 := s.bij_on_id

| (n + 1) := (bij_on.iterate n).comp h

lemma bij_on_of_subsingleton' [subsingleton α] [subsingleton β] (f : α → β)

(h : s.nonempty ↔ t.nonempty) : bij_on f s t :=

⟨maps_to_of_subsingleton' _ h.1, inj_on_of_subsingleton _ _, surj_on_of_subsingleton' _ h.2⟩

lemma bij_on_of_subsingleton [subsingleton α] (f : α → α) (s : set α) : bij_on f s s :=

bij_on_of_subsingleton' _ iff.rfl

theorem bij_on.bijective (h : bij_on f s t) : bijective (h.maps_to.restrict f s t) :=

⟨λ x y h', subtype.ext $ h.inj_on x.2 y.2 $ subtype.ext_iff.1 h',

λ ⟨y, hy⟩, let ⟨x, hx, hxy⟩ := h.surj_on hy in ⟨⟨x, hx⟩, subtype.eq hxy⟩⟩

lemma bijective_iff_bij_on_univ : bijective f ↔ bij_on f univ univ :=

iff.intro

(λ h, let ⟨inj, surj⟩ := h in

⟨maps_to_univ f _, inj.inj_on _, iff.mp surjective_iff_surj_on_univ surj⟩)

(λ h, let ⟨map, inj, surj⟩ := h in

⟨iff.mpr injective_iff_inj_on_univ inj, iff.mpr surjective_iff_surj_on_univ surj⟩)

alias bijective_iff_bij_on_univ ↔ _root_.function.bijective.bij_on_univ _

lemma bij_on.compl (hst : bij_on f s t) (hf : bijective f) : bij_on f sᶜ tᶜ :=

⟨hst.surj_on.maps_to_compl hf.1, hf.1.inj_on _, hst.maps_to.surj_on_compl hf.2⟩

def left_inv_on (f' : β → α) (f : α → β) (s : set α) : Prop :=

∀ ⦃x⦄, x ∈ s → f' (f x) = x

@[simp] lemma left_inv_on_empty (f' : β → α) (f : α → β) : left_inv_on f' f ∅ := empty_subset _

@[simp] lemma left_inv_on_singleton : left_inv_on f' f {a} ↔ f' (f a) = a := singleton_subset_iff

lemma left_inv_on.eq_on (h : left_inv_on f' f s) : eq_on (f' ∘ f) id s := h

lemma left_inv_on.eq (h : left_inv_on f' f s) {x} (hx : x ∈ s) : f' (f x) = x := h hx

lemma left_inv_on.congr_left (h₁ : left_inv_on f₁' f s)

{t : set β} (h₁' : maps_to f s t) (heq : eq_on f₁' f₂' t) : left_inv_on f₂' f s :=

λ x hx, heq (h₁' hx) ▸ h₁ hx

theorem left_inv_on.congr_right (h₁ : left_inv_on f₁' f₁ s) (heq : eq_on f₁ f₂ s) :

left_inv_on f₁' f₂ s :=

λ x hx, heq hx ▸ h₁ hx

theorem left_inv_on.inj_on (h : left_inv_on f₁' f s) : inj_on f s :=

λ x₁ h₁ x₂ h₂ heq,

x₁ = f₁' (f x₁) : eq.symm $ h h₁

... = f₁' (f x₂) : congr_arg f₁' heq

... = x₂ : h h₂

theorem left_inv_on.surj_on (h : left_inv_on f' f s) (hf : maps_to f s t) : surj_on f' t s :=

λ x hx, ⟨f x, hf hx, h hx⟩

theorem left_inv_on.maps_to (h : left_inv_on f' f s) (hf : surj_on f s t) : maps_to f' t s :=

λ y hy, let ⟨x, hs, hx⟩ := hf hy in by rwa [← hx, h hs]

lemma left_inv_on_id (s : set α) : left_inv_on id id s := λ a _, rfl

theorem left_inv_on.comp

(hf' : left_inv_on f' f s) (hg' : left_inv_on g' g t) (hf : maps_to f s t) :

left_inv_on (f' ∘ g') (g ∘ f) s :=

λ x h,

(f' ∘ g') ((g ∘ f) x) = f' (f x) : congr_arg f' (hg' (hf h))

... = x : hf' h

theorem left_inv_on.mono (hf : left_inv_on f' f s) (ht : s₁ ⊆ s) : left_inv_on f' f s₁ :=

λ x hx, hf (ht hx)

theorem left_inv_on.image_inter' (hf : left_inv_on f' f s) :

f '' (s₁ ∩ s) = f' ⁻¹' s₁ ∩ f '' s :=

apply subset.antisymm,

{ rintro _ ⟨x, ⟨h₁, h⟩, rfl⟩, exact ⟨by rwa [mem_preimage, hf h], mem_image_of_mem _ h⟩ },

{ rintro _ ⟨h₁, ⟨x, h, rfl⟩⟩, exact mem_image_of_mem _ ⟨by rwa ← hf h, h⟩ }

theorem left_inv_on.image_inter (hf : left_inv_on f' f s) :

f '' (s₁ ∩ s) = f' ⁻¹' (s₁ ∩ s) ∩ f '' s :=

rw hf.image_inter',

refine subset.antisymm _ (inter_subset_inter_left _ (preimage_mono $ inter_subset_left _ _)),

rintro _ ⟨h₁, x, hx, rfl⟩, exact ⟨⟨h₁, by rwa hf hx⟩, mem_image_of_mem _ hx⟩

theorem left_inv_on.image_image (hf : left_inv_on f' f s) :

f' '' (f '' s) = s :=

by rw [image_image, image_congr hf, image_id']

theorem left_inv_on.image_image' (hf : left_inv_on f' f s) (hs : s₁ ⊆ s) :

f' '' (f '' s₁) = s₁ :=

(hf.mono hs).image_image

@[reducible] def right_inv_on (f' : β → α) (f : α → β) (t : set β) : Prop :=

left_inv_on f f' t

@[simp] lemma right_inv_on_empty (f' : β → α) (f : α → β) : right_inv_on f' f ∅ := empty_subset _

@[simp] lemma right_inv_on_singleton : right_inv_on f' f {b} ↔ f (f' b) = b := singleton_subset_iff

lemma right_inv_on.eq_on (h : right_inv_on f' f t) : eq_on (f ∘ f') id t := h

lemma right_inv_on.eq (h : right_inv_on f' f t) {y} (hy : y ∈ t) : f (f' y) = y := h hy

lemma left_inv_on.right_inv_on_image (h : left_inv_on f' f s) : right_inv_on f' f (f '' s) :=

λ y ⟨x, hx, eq⟩, eq ▸ congr_arg f $ h.eq hx

theorem right_inv_on.congr_left (h₁ : right_inv_on f₁' f t) (heq : eq_on f₁' f₂' t) :

right_inv_on f₂' f t :=

h₁.congr_right heq

theorem right_inv_on.congr_right (h₁ : right_inv_on f' f₁ t) (hg : maps_to f' t s)

(heq : eq_on f₁ f₂ s) : right_inv_on f' f₂ t :=

left_inv_on.congr_left h₁ hg heq

theorem right_inv_on.surj_on (hf : right_inv_on f' f t) (hf' : maps_to f' t s) :

surj_on f s t :=

hf.surj_on hf'

theorem right_inv_on.maps_to (h : right_inv_on f' f t) (hf : surj_on f' t s) : maps_to f s t :=

h.maps_to hf

lemma right_inv_on_id (s : set α) : right_inv_on id id s := λ a _, rfl

theorem right_inv_on.comp (hf : right_inv_on f' f t) (hg : right_inv_on g' g p)

(g'pt : maps_to g' p t) : right_inv_on (f' ∘ g') (g ∘ f) p :=

hg.comp hf g'pt

theorem right_inv_on.mono (hf : right_inv_on f' f t) (ht : t₁ ⊆ t) : right_inv_on f' f t₁ :=

hf.mono ht

theorem inj_on.right_inv_on_of_left_inv_on (hf : inj_on f s) (hf' : left_inv_on f f' t)

(h₁ : maps_to f s t) (h₂ : maps_to f' t s) :

right_inv_on f f' s :=

λ x h, hf (h₂ $ h₁ h) h (hf' (h₁ h))

theorem eq_on_of_left_inv_on_of_right_inv_on (h₁ : left_inv_on f₁' f s) (h₂ : right_inv_on f₂' f t)

(h : maps_to f₂' t s) : eq_on f₁' f₂' t :=

λ y hy,

calc f₁' y = (f₁' ∘ f ∘ f₂') y : congr_arg f₁' (h₂ hy).symm

... = f₂' y : h₁ (h hy)

theorem surj_on.left_inv_on_of_right_inv_on (hf : surj_on f s t) (hf' : right_inv_on f f' s) :

left_inv_on f f' t :=

λ y hy, let ⟨x, hx, heq⟩ := hf hy in by rw [← heq, hf' hx]

def inv_on (g : β → α) (f : α → β) (s : set α) (t : set β) : Prop :=

left_inv_on g f s ∧ right_inv_on g f t

@[simp] lemma inv_on_empty (f' : β → α) (f : α → β) : inv_on f' f ∅ ∅ := by simp [inv_on]

@[simp] lemma inv_on_singleton : inv_on f' f {a} {b} ↔ f' (f a) = a ∧ f (f' b) = b :=

by simp [inv_on]

lemma inv_on.symm (h : inv_on f' f s t) : inv_on f f' t s := ⟨h.right, h.left⟩

lemma inv_on_id (s : set α) : inv_on id id s s := ⟨s.left_inv_on_id, s.right_inv_on_id⟩

lemma inv_on.comp (hf : inv_on f' f s t) (hg : inv_on g' g t p) (fst : maps_to f s t)

(g'pt : maps_to g' p t) :

inv_on (f' ∘ g') (g ∘ f) s p :=

⟨hf.1.comp hg.1 fst, hf.2.comp hg.2 g'pt⟩

lemma inv_on.mono (h : inv_on f' f s t) (hs : s₁ ⊆ s) (ht : t₁ ⊆ t) : inv_on f' f s₁ t₁ :=

⟨h.1.mono hs, h.2.mono ht⟩

theorem inv_on.bij_on (h : inv_on f' f s t) (hf : maps_to f s t) (hf' : maps_to f' t s) :

bij_on f s t :=

⟨hf, h.left.inj_on, h.right.surj_on hf'⟩

lemma bij_on.symm {g : β → α} (h : inv_on f g t s) (hf : bij_on f s t) : bij_on g t s :=

⟨h.2.maps_to hf.surj_on, h.1.inj_on, h.2.surj_on hf.maps_to⟩

lemma bij_on_comm {g : β → α} (h : inv_on f g t s) : bij_on f s t ↔ bij_on g t s :=

⟨bij_on.symm h, bij_on.symm h.symm⟩

end set

namespace function

variables [nonempty α] {s : set α} {f : α → β} {a : α} {b : β}

local attribute [instance, priority 10] classical.prop_decidable

noncomputable def inv_fun_on (f : α → β) (s : set α) (b : β) : α :=

if h : ∃a, a ∈ s ∧ f a = b then classical.some h else classical.choice ‹nonempty α›

theorem inv_fun_on_pos (h : ∃a∈s, f a = b) : inv_fun_on f s b ∈ s ∧ f (inv_fun_on f s b) = b :=

by rw [bex_def] at h; rw [inv_fun_on, dif_pos h]; exact classical.some_spec h

theorem inv_fun_on_mem (h : ∃a∈s, f a = b) : inv_fun_on f s b ∈ s := (inv_fun_on_pos h).left

theorem inv_fun_on_eq (h : ∃a∈s, f a = b) : f (inv_fun_on f s b) = b := (inv_fun_on_pos h).right

theorem inv_fun_on_neg (h : ¬ ∃a∈s, f a = b) : inv_fun_on f s b = classical.choice ‹nonempty α› :=

by rw [bex_def] at h; rw [inv_fun_on, dif_neg h]

@[simp] theorem inv_fun_on_apply_mem (h : a ∈ s) : inv_fun_on f s (f a) ∈ s :=

inv_fun_on_mem ⟨a, h, rfl⟩

theorem inv_fun_on_apply_eq (h : a ∈ s) : f (inv_fun_on f s (f a)) = f a :=

inv_fun_on_eq ⟨a, h, rfl⟩

end function

open function

namespace set

variables {s s₁ s₂ : set α} {t : set β} {f : α → β}

theorem inj_on.left_inv_on_inv_fun_on [nonempty α] (h : inj_on f s) :

left_inv_on (inv_fun_on f s) f s :=

λ a ha, h (inv_fun_on_apply_mem ha) ha (inv_fun_on_apply_eq ha)

lemma inj_on.inv_fun_on_image [nonempty α] (h : inj_on f s₂) (ht : s₁ ⊆ s₂) :

(inv_fun_on f s₂) '' (f '' s₁) = s₁ :=

h.left_inv_on_inv_fun_on.image_image' ht

theorem surj_on.right_inv_on_inv_fun_on [nonempty α] (h : surj_on f s t) :

right_inv_on (inv_fun_on f s) f t :=

λ y hy, inv_fun_on_eq $ mem_image_iff_bex.1 $ h hy

theorem bij_on.inv_on_inv_fun_on [nonempty α] (h : bij_on f s t) :

inv_on (inv_fun_on f s) f s t :=

⟨h.inj_on.left_inv_on_inv_fun_on, h.surj_on.right_inv_on_inv_fun_on⟩