feat(data/equiv/option): option_congr (#12263)

This is a universe-polymorphic version of the existing `equiv_functor.map_equiv option`.

src/combinatorics/derangements/basic.lean

@@ -141,8 +141,7 @@ begin
       simp only [perm.decompose_option_symm_apply, swap_apply_self, perm.coe_mul],
       cases x,
       { simp },
-      simp only [equiv_functor.map_equiv_apply, equiv_functor.map,
-                  option.map_eq_map, option.map_some'],
+      simp only [equiv.option_congr_apply, option.map_some'],
       by_cases x_vs_a : x = a,
       { rw [x_vs_a, swap_apply_right], apply option.some_ne_none },
       have ne_1 : some x ≠ none := option.some_ne_none _,

src/data/equiv/option.lean

@@ -9,16 +9,50 @@ import control.equiv_functor
 /-!
 # Equivalences for `option α`
 
-We define `remove_none` which acts to provide a `e : α ≃ β` if given a `f : option α ≃ option β`.
 
-To construct an `f : option α ≃ option β` from `e : α ≃ β` such that
-`f none = none` and `f (some x) = some (e x)`, use
-`f = equiv_functor.map_equiv option e`.
+We define
+* `equiv.option_congr`: the `option α ≃ option β` constructed from `e : α ≃ β` by sending `none` to
+  `none`, and applying a `e` elsewhere.
+* `equiv.remove_none`: the `α ≃ β` constructed from `option α ≃ option β` by removing `none` from
+  both sides.
 -/
 
 namespace equiv
 
-variables {α β : Type*} (e : option α ≃ option β)
+variables {α β γ : Type*}
+
+section option_congr
+
+variables
+
+/-- A universe-polymorphic version of `equiv_functor.map_equiv option e`. -/
+@[simps apply]
+def option_congr (e : α ≃ β) : option α ≃ option β :=
+{ to_fun := option.map e,
+  inv_fun := option.map e.symm,
+  left_inv := λ x, (option.map_map _ _ _).trans $
+    e.symm_comp_self.symm ▸ congr_fun option.map_id x,
+  right_inv := λ x, (option.map_map _ _ _).trans $
+    e.self_comp_symm.symm ▸ congr_fun option.map_id x }
+
+@[simp] lemma option_congr_refl : option_congr (equiv.refl α) = equiv.refl _ :=
+ext $ congr_fun option.map_id
+
+@[simp] lemma option_congr_symm (e : α ≃ β) : (option_congr e).symm = option_congr e.symm := rfl
+
+@[simp] lemma option_congr_trans (e₁ : α ≃ β) (e₂ : β ≃ γ) :
+  (option_congr e₁).trans (option_congr e₂) = option_congr (e₁.trans e₂) :=
+ext $ option.map_map _ _
+
+/-- When `α` and `β` are in the same universe, this is the same as the result of
+`equiv_functor.map_equiv`. -/
+lemma option_congr_eq_equiv_function_map_equiv {α β : Type*} (e : α ≃ β) :
+  option_congr e = equiv_functor.map_equiv option e := rfl
+
+end option_congr
+
+section remove_none
+variables (e : option α ≃ option β)
 
 private def remove_none_aux (x : α) : β :=
 if h : (e (some x)).is_some
@@ -87,8 +121,12 @@ begin
 end
 
 @[simp]
-lemma remove_none_map_equiv {α β : Type*} (e : α ≃ β) :
-  remove_none (equiv_functor.map_equiv option e) = e :=
+lemma remove_none_option_congr (e : α ≃ β) : remove_none e.option_congr = e :=
 equiv.ext $ λ x, option.some_injective _ $ remove_none_some _ ⟨e x, by simp [equiv_functor.map]⟩
 
+end remove_none
+
+lemma option_congr_injective : function.injective (option_congr : α ≃ β → option α ≃ option β) :=
+function.left_inverse.injective remove_none_option_congr
+
 end equiv

src/group_theory/perm/option.lean

@@ -11,42 +11,31 @@ import data.equiv.option
 -/
 open equiv
 
-lemma equiv_functor.map_equiv_option_injective {α β : Type*} :
-  function.injective (equiv_functor.map_equiv option : α ≃ β → option α ≃ option β) :=
-equiv_functor.map_equiv.injective option option.some_injective
+@[simp] lemma equiv.option_congr_one {α : Type*} : (1 : perm α).option_congr = 1 :=
+equiv.option_congr_refl
 
-@[simp] lemma equiv_functor.option.map_none {α β : Type*} (e : α ≃ β) :
-  equiv_functor.map e none = none :=
-by simp [equiv_functor.map]
-
-@[simp] lemma map_equiv_option_one {α : Type*} : equiv_functor.map_equiv option (1 : perm α) = 1 :=
-by {ext, simp [equiv_functor.map_equiv, equiv_functor.map] }
-
-@[simp] lemma map_equiv_option_refl {α : Type*} :
-  equiv_functor.map_equiv option (equiv.refl α) = 1 := map_equiv_option_one
-
-@[simp] lemma map_equiv_option_swap {α : Type*} [decidable_eq α] (x y : α) :
-  equiv_functor.map_equiv option (swap x y) = swap (some x) (some y) :=
+@[simp] lemma equiv.option_congr_swap {α : Type*} [decidable_eq α] (x y : α) :
+  option_congr (swap x y) = swap (some x) (some y) :=
 begin
   ext (_ | i),
   { simp [swap_apply_of_ne_of_ne] },
   { by_cases hx : i = x,
-    simp [hx, swap_apply_of_ne_of_ne, equiv_functor.map],
+    simp [hx, swap_apply_of_ne_of_ne],
     by_cases hy : i = y;
-    simp [hx, hy, swap_apply_of_ne_of_ne, equiv_functor.map], }
+    simp [hx, hy, swap_apply_of_ne_of_ne], }
 end
 
-@[simp] lemma equiv_functor.option.sign {α : Type*} [decidable_eq α] [fintype α] (e : perm α) :
-  perm.sign (equiv_functor.map_equiv option e) = perm.sign e :=
+@[simp] lemma equiv.option_congr_sign {α : Type*} [decidable_eq α] [fintype α] (e : perm α) :
+  perm.sign e.option_congr = perm.sign e :=
 begin
   apply perm.swap_induction_on e,
   { simp [perm.one_def] },
   { intros f x y hne h,
-    simp [h, hne, perm.mul_def, ←equiv_functor.map_equiv_trans] }
+    simp [h, hne, perm.mul_def, ←equiv.option_congr_trans] }
 end
 
 @[simp] lemma map_equiv_remove_none {α : Type*} [decidable_eq α] (σ : perm (option α)) :
-  equiv_functor.map_equiv option (remove_none σ) = swap none (σ none) * σ :=
+  (remove_none σ).option_congr = swap none (σ none) * σ :=
 begin
   ext1 x,
   have : option.map ⇑(remove_none σ) x = (swap none (σ none)) (σ x),
@@ -66,18 +55,18 @@ The fixed `option α` is swapped with `none`. -/
 @[simps] def equiv.perm.decompose_option {α : Type*} [decidable_eq α] :
   perm (option α) ≃ option α × perm α :=
 { to_fun := λ σ, (σ none, remove_none σ),
-  inv_fun := λ i, swap none i.1 * (equiv_functor.map_equiv option i.2),
+  inv_fun := λ i, swap none i.1 * i.2.option_congr,
   left_inv := λ σ, by simp,
   right_inv := λ ⟨x, σ⟩, begin
-    have : remove_none (swap none x * equiv_functor.map_equiv option σ) = σ :=
-      equiv_functor.map_equiv_option_injective (by simp [←mul_assoc, equiv_functor.map]),
-    simp [←perm.eq_inv_iff_eq, equiv_functor.map, this],
+    have : remove_none (swap none x * σ.option_congr) = σ :=
+      equiv.option_congr_injective (by simp [←mul_assoc]),
+    simp [←perm.eq_inv_iff_eq, this],
   end }
 
 lemma equiv.perm.decompose_option_symm_of_none_apply {α : Type*} [decidable_eq α]
   (e : perm α) (i : option α) :
   equiv.perm.decompose_option.symm (none, e) i = i.map e :=
-by simp [equiv_functor.map]
+by simp
 
 lemma equiv.perm.decompose_option_symm_sign {α : Type*} [decidable_eq α] [fintype α] (e : perm α) :
   perm.sign (equiv.perm.decompose_option.symm (none, e)) = perm.sign e :=