feat(control/equiv_functor): simp defn lemmas and injectivity (#5739)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/control/equiv_functor.lean

@@ -52,8 +52,26 @@ def map_equiv :
 @[simp] lemma map_equiv_apply (x : f α) :
   map_equiv f e x = equiv_functor.map e x := rfl
 
-@[simp] lemma map_equiv_symm_apply (y : f β) :
+lemma map_equiv_symm_apply (y : f β) :
   (map_equiv f e).symm y = equiv_functor.map e.symm y := rfl
+
+@[simp] lemma map_equiv_refl (α) :
+  map_equiv f (equiv.refl α) = equiv.refl (f α) :=
+by simpa [equiv_functor.map_equiv]
+
+@[simp] lemma map_equiv_symm :
+  (map_equiv f e).symm = map_equiv f e.symm :=
+equiv.ext $ map_equiv_symm_apply f e
+
+/--
+The composition of `map_equiv`s is carried over the `equiv_functor`.
+For plain `functor`s, this lemma is named `map_map` when applied
+or `map_comp_map` when not applied.
+-/
+@[simp] lemma map_equiv_trans {γ : Type u₀} (ab : α ≃ β) (bc : β ≃ γ) :
+  (map_equiv f ab).trans (map_equiv f bc) = map_equiv f (ab.trans bc) :=
+equiv.ext $ λ x, by simp [map_equiv, map_trans']
+
 end
 
 @[priority 100]
@@ -63,4 +81,10 @@ instance of_is_lawful_functor
   map_refl' := λ α, by { ext, apply is_lawful_functor.id_map, },
   map_trans' := λ α β γ k h, by { ext x, apply (is_lawful_functor.comp_map k h x), } }
 
+lemma map_equiv.injective
+  (f : Type u₀ → Type u₁) [applicative f] [is_lawful_applicative f] {α β : Type u₀}
+  (h : ∀ γ, function.injective (pure : γ → f γ)) :
+  function.injective (@equiv_functor.map_equiv f _ α β) :=
+λ e₁ e₂ H, equiv.ext $ λ x, h β (by simpa [equiv_functor.map] using equiv.congr_fun H (pure x))
+
 end equiv_functor