chore(data/equiv/basic): Add trivial simp lemma (#5100)

With this in place, `⇑1 ∘ f` simplifies to `⇑f`

Author: eric-wieser

src/data/equiv/basic.lean

@@ -271,7 +271,7 @@ end
 theorem mul_apply {α : Type u} (f g : perm α) (x) : (f * g) x = f (g x) :=
 equiv.trans_apply _ _ _
 
-@[simp] theorem one_apply {α : Type u} (x) : (1 : perm α) x = x := rfl
+theorem one_apply {α : Type u} (x) : (1 : perm α) x = x := rfl
 
 @[simp] lemma inv_apply_self {α : Type u} (f : perm α) (x) :
   f⁻¹ (f x) = x := equiv.symm_apply_apply _ _
@@ -287,6 +287,8 @@ lemma inv_def {α : Type u} (f : perm α) : f⁻¹ = f.symm := rfl
 
 @[simp] lemma coe_mul {α : Type u} (f g : perm α) : ⇑(f * g) = f ∘ g := rfl
 
+@[simp] lemma coe_one {α : Type u} : ⇑(1 : perm α) = id := rfl
+
 end perm
 
 /-- If `α` is an empty type, then it is equivalent to the `empty` type. -/