feat(logic/function/basic): a lemma on symmetric operations and flip (#…

…7871)

This lemma is used to show that if multiplication is commutative, then `flip`ping the arguments returns the same function.

This is used in PR #7645 .

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

src/logic/function/basic.lean

@@ -654,3 +654,6 @@ lemma cast_inj {α β : Type*} (h : α = β) {x y : α} : cast h x = cast h y 
 if for each pair of distinct points there is a function taking different values on them. -/
 def set.separates_points {α β : Type*} (A : set (α → β)) : Prop :=
 ∀ ⦃x y : α⦄, x ≠ y → ∃ f ∈ A, (f x : β) ≠ f y
+
+lemma is_symm_op.flip_eq {α β} (op) [is_symm_op α β op] : flip op = op :=
+funext $ λ a, funext $ λ b, (is_symm_op.symm_op a b).symm