From 3b4e9d58eae1978db9bd73d4c5f9c90fd4bb65ee Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Mon, 26 Sep 2022 05:32:50 +0000
Subject: [PATCH] feat(data/option/basic): `option.map` is injective (#16626)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* prove that `option.map : (α → β) → (option α → option β)` is injective;
* add `iff` version of this lemma;
* add `option.map_comp_some` and `option.map_eq_id`;
* drop `option.map_id'`: it was the same as `option.map_id`.
---
 src/data/option/basic.lean | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/data/option/basic.lean b/src/data/option/basic.lean
index f8587890de76a..16ff17eba180f 100644
--- a/src/data/option/basic.lean
+++ b/src/data/option/basic.lean
@@ -88,6 +88,8 @@ theorem map_injective {f : α → β} (Hf : function.injective f) : function.inj
 | none      none      H := rfl
 | (some a₁) (some a₂) H := by rw Hf (option.some.inj H)
 
+@[simp] theorem map_comp_some (f : α → β) : option.map f ∘ some = some ∘ f := rfl
+
 @[ext] theorem ext : ∀ {o₁ o₂ : option α}, (∀ a, a ∈ o₁ ↔ a ∈ o₂) → o₁ = o₂
 | none     none     H := rfl
 | (some a) o        H := ((H _).1 rfl).symm
@@ -179,11 +181,20 @@ by { cases x; simp only [map_none, map_some, eq_self_iff_true] }
   x.map f = none ↔ x = none :=
 by { cases x; simp only [map_none', map_some', eq_self_iff_true] }
 
+/-- `option.map` as a function between functions is injective. -/
+theorem map_injective' : function.injective (@option.map α β) :=
+λ f g h, funext $ λ x, some_injective _ $ by simp only [← map_some', h]
+
+@[simp] theorem map_inj {f g : α → β} : option.map f = option.map g ↔ f = g :=
+map_injective'.eq_iff
+
 lemma map_congr {f g : α → β} {x : option α} (h : ∀ a ∈ x, f a = g a) :
   option.map f x = option.map g x :=
 by { cases x; simp only [map_none', map_some', h, mem_def] }
 
-@[simp] theorem map_id' : option.map (@id α) = id := map_id
+attribute [simp] map_id
+
+@[simp] theorem map_eq_id {f : α → α} : option.map f = id ↔ f = id := map_injective'.eq_iff' map_id
 
 @[simp] lemma map_map (h : β → γ) (g : α → β) (x : option α) :
   option.map h (option.map g x) = option.map (h ∘ g) x :=