feat(logic/equiv/basic): coe_prod_comm (#17510)

As a result of this new lemma, `prod_comm_image` and `prod_comm_preimage` are now redundant.

Author: YaelDillies

src/logic/embedding/basic.lean

@@ -57,7 +57,10 @@ example (s : finset (fin 3)) (f : equiv.perm (fin 3)) : s.map f.to_embedding = s
 example (s : finset (fin 3)) (f : equiv.perm (fin 3)) : s.map f = s.map f.to_embedding := by simp
 ```
 -/
-@[simps] protected def equiv.to_embedding : α ↪ β := ⟨f, f.injective⟩
+protected def equiv.to_embedding : α ↪ β := ⟨f, f.injective⟩
+
+@[simp] lemma equiv.coe_to_embedding : ⇑f.to_embedding = f := rfl
+lemma equiv.to_embedding_apply (a : α) : f.to_embedding a = f a := rfl
 
 instance equiv.coe_embedding : has_coe (α ≃ β) (α ↪ β) := ⟨equiv.to_embedding⟩
 

src/logic/equiv/basic.lean

@@ -89,8 +89,11 @@ rfl
 
 /-- Type product is commutative up to an equivalence: `α × β ≃ β × α`. This is `prod.swap` as an
 equivalence.-/
-@[simps apply] def prod_comm (α β : Type*) : α × β ≃ β × α :=
-⟨prod.swap, prod.swap, λ ⟨a, b⟩, rfl, λ ⟨a, b⟩, rfl⟩
+def prod_comm (α β : Type*) : α × β ≃ β × α :=
+⟨prod.swap, prod.swap, prod.swap_swap, prod.swap_swap⟩
+
+@[simp] lemma coe_prod_comm (α β : Type*) : ⇑(prod_comm α β) = prod.swap := rfl
+@[simp] lemma prod_comm_apply {α β : Type*} (x : α × β) : prod_comm α β x = x.swap := rfl
 
 @[simp] lemma prod_comm_symm (α β) : (prod_comm α β).symm = prod_comm β α := rfl
 

src/logic/equiv/set.lean

@@ -100,13 +100,6 @@ preimage_eq_iff_eq_image e.bijective
 lemma eq_preimage_iff_image_eq {α β} (e : α ≃ β) (s t) : s = e ⁻¹' t ↔ e '' s = t :=
 eq_preimage_iff_image_eq e.bijective
 
-@[simp] lemma prod_comm_preimage {α β} {s : set α} {t : set β} :
-  equiv.prod_comm α β ⁻¹' t ×ˢ s = s ×ˢ t :=
-preimage_swap_prod _ _
-
-lemma prod_comm_image {α β} {s : set α} {t : set β} : equiv.prod_comm α β '' s ×ˢ t = t ×ˢ s :=
-image_swap_prod _ _
-
 @[simp]
 lemma prod_assoc_preimage {α β γ} {s : set α} {t : set β} {u : set γ} :
   equiv.prod_assoc α β γ ⁻¹' s ×ˢ (t ×ˢ u) = (s ×ˢ t) ×ˢ u :=